HOME

TheInfoList



OR:

In
Mathematical logic Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
(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 science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
), two formulae 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 both are not. 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 on ...
, as two equivalent formulae always have the same models. Whereas within equisatisfiable formulae, only the primitive proposition the formula imposes is valued. 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 involving this concept are
Skolemization In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers. Every first-order formula may be converted into Skolem normal form while not changing it ...
and some translations into
conjunctive normal form In Boolean logic, 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. As a can ...
.


Examples

A translation from propositional logic into propositional logic in which every binary disjunction a \vee b is replaced by ((a \vee n) \wedge (\neg n \vee b)), where n is a new variable (one for each replaced disjunction) is a transformation in which satisfiability is preserved: the original and resulting formulae are equisatisfiable. Note that these two formulae are not equivalent: the first formula has the model in which b is true while a and n are false (the model's truth value for n being irrelevant to the truth value of the formula), but this is not a model of the second formula, in which n has to be true in this case.


References

Metalogic Model theory Concepts in logic {{mathlogic-stub