Jämliktillfredsställelse

Inom matematisk logik (ett underämne inom området formell logik ) är två formler likvärdiga om den första formeln är tillfredsställbar närhelst den andra är det och vice versa; med andra ord, antingen är båda formlerna tillfredsställbara eller så är båda inte det. Liktillfredsställande formler kan dock inte överensstämma för ett visst val av variabler. Som ett resultat av detta skiljer sig likvärdighet från logisk likvärdighet , eftersom två ekvivalenta formler alltid har samma modeller. Medan inom ekvisatisfiable formler, värderas endast den primitiva propositionen formeln ger.

Liktillfredsställelse används vanligtvis i samband med att översätta formler, så att man kan definiera en översättning som korrekt om de ursprungliga och resulterande formlerna är likvärdiga. Exempel på översättningar som involverar detta koncept är Skolemization och några översättningar till konjunktiv normal form .

Exempel

En översättning från propositionslogik till propositionslogik där varje binär disjunktion $a\vee b$ ersätts med $((a\vee n) )\wedge (\neg n\vee b))$ , där $n$ är en ny variabel (en för varje ersatt disjunktion) är en transformation där tillfredsställbarheten bevaras: de ursprungliga och resulterande formlerna är equisatisfiable. Observera att dessa två formler inte är ekvivalenta: den första formeln har modellen där $b$ är sann medan $a$ och $n$ är falska (modellens sanningsvärde för ${\ displaystyle n}$ är irrelevant för formelns sanningsvärde), men detta är inte en modell av den andra formeln, där $n$ måste vara sann i detta fall.