Equisatisfacibilidad

En lógica matemática (un subtema dentro del campo de la lógica formal ), dos fórmulas son equisatisfacibles si la primera fórmula es satisfacible siempre que la segunda lo sea y viceversa; en otras palabras, o ambas fórmulas son satisfacibles o ninguna lo es. ^{[ 1 ]} Sin embargo, los valores de verdad de dos fórmulas equisatisfacibles pueden no ser distintos para una asignación particular de variables. Como resultado, la equisatisfacibilidad difiere de la equivalencia lógica , ya que dos fórmulas equivalentes siempre tienen los mismos modelos, mientras que las equisatisfacibles solo necesitan compartir el estado de satisfacibilidad. Más formalmente, la metafórmula de equisatisfacibilidad${\displaystyle f}$es verdadero si ambas subfórmulas son satisfacibles o si ambas no lo son: ^{[ 2 ]}

${\displaystyle f\;\equiv \;(\operatorname {Sat} (\phi )\land \operatorname {Sat} (\psi ))\lor (\lnot \operatorname {Sat} (\phi )\land \lnot \operatorname {Sat} (\psi ))\;\equiv \;\operatorname {Sat} (\phi )\leftrightarrow \operatorname {Sat} (\psi )}$

La equisatisfacibilidad se utiliza generalmente en el contexto de la traducción de fórmulas, de modo que se puede definir una traducción como correcta si la fórmula original y la resultante son equisatisfacibles. Ejemplos de traducciones que conservan la equisatisfacibilidad son la skolemización y algunas traducciones a la forma normal conjuntiva, como la transformación de Tseytin .

Una traducción de lógica proposicional a lógica proposicional en la que cada disyunción binaria${\displaystyle a\vee b}$es reemplazado por${\displaystyle (a\vee n)\wedge (\neg n\vee b)}$, dónde${\displaystyle n}$es una variable nueva (una por cada disyunción reemplazada) es una transformación en la que se conserva la satisfacibilidad: las fórmulas original y resultante son equisatisfacibles. Estas dos fórmulas no son equivalentes: la primera fórmula tiene el modelo en el que${\displaystyle b}$es cierto mientras${\displaystyle a}$y${\displaystyle n}$son falsos (el valor de verdad del modelo para${\displaystyle n}$siendo irrelevante para el valor de verdad de la fórmula), pero este no es un modelo de la segunda fórmula, en la que${\displaystyle n}$tiene que ser cierto cuando${\displaystyle a}$es falso.