In
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
(a subtopic within the field of
formal logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the study of deductively valid inferences or logical truths. It examines how conclusions follow from premises based on the structure o ...
), two
formulae
In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwe ...
are equisatisfiable if the first formula is
satisfiable
In mathematical logic, a formula is ''satisfiable'' if it is true under some assignment of values to its variables. For example, the formula x+3=y is satisfiable because it is true when x=3 and y=6, while the formula x+1=x is not satisfiable over ...
whenever the second is and vice versa; in other words, either both formulae are satisfiable or none of them is.
The truth values of two equisatisfiable formulae may disagree, however, for a particular choice of variables. As a result, equisatisfiability is different from
logical equivalence
In logic and mathematics, statements p and q are said to be logically equivalent if they have the same truth value in every model. The logical equivalence of p and q is sometimes expressed as p \equiv q, p :: q, \textsfpq, or p \iff q, depending ...
, as two equivalent formulae always have the same models. Whereas within equisatisfiable formulae, {{clarify span, only the primitive proposition the formula imposes is valued, What is this supposed to mean?, date=May 2025.
Equisatisfiability is generally used in the context of translating formulae, so that one can define a translation to be correct if the original and resulting formulae are equisatisfiable. Examples of translations that preserve equisatisfiability are
Skolemization
In mathematical logic, a Well-formed_formula, formula of first-order logic is in Skolem normal form if it is in prenex normal form with only Universal quantification, universal first-order quantifiers.
Every first-order Well-formed formula, formu ...
and some translations into
conjunctive normal form
In Boolean algebra, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs.
In au ...
such as the
Tseytin transformation
The Tseytin transformation, alternatively written Tseitin transformation, takes as input an arbitrary combinatorial logic circuit and produces an equisatisfiable boolean formula in conjunctive normal form (CNF). The length of the formula is line ...
.
Examples
A translation from
propositional logic
The propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. Sometimes, it is called ''first-order'' propositional logic to contra ...
into propositional logic in which every binary disjunction
is replaced by
, where
is a
fresh variable (one for each replaced disjunction) is a transformation in which satisfiability is preserved: the original and resulting formulae are equisatisfiable. These two formulae are not equivalent: the first formula has the model in which
is true while
and
are false (the model's truth value for
being irrelevant to the truth value of the formula), but this is not a model of the second formula, in which
has to be true when
is false.
References
Metalogic
Model theory
Concepts in logic