Равновыполнимость

В математической логике (подтема в области формальной логики ) две формулы являются равновыполнимыми , если первая формула выполнима всякий раз, когда выполнима вторая, и наоборот; другими словами, либо обе формулы выполнимы, либо обе нет. Однако эквивалентные формулы могут не совпадать при определенном выборе переменных. В результате эквивыполнимость отличается от логической эквивалентности , поскольку две эквивалентные формулы всегда имеют одни и те же модели. В то время как внутри равновыполнимых формул ценится только примитивное предложение, которое формула навязывает.

Эквивыполнимость обычно используется в контексте перевода формул, так что можно определить перевод как правильный, если исходная и результирующая формулы эквивыполнимы. Примерами переводов, сохраняющих эквивыполнимость, являются сколемизация и некоторые переводы в конъюнктивную нормальную форму, такие как преобразование Цейтина .

Примеры

Перевод из логики высказываний в логику высказываний, в котором каждая бинарная дизъюнкция $a\vee b$ заменяется на $((a\vee n)\wedge (\neg n\vee b))$, где $n$ — новая переменная (по одной для каждой замененной дизъюнкции) — преобразование, при котором сохраняется выполнимость: исходная и результирующая формулы эквивыполнимы. Обратите внимание, что эти две формулы не эквивалентны: первая формула имеет модель, в которой $b$ это правда, пока $a$ и $n$ ложны (значение истинности модели для $n$ не имеет отношения к истинностному значению формулы), но это не модель второй формулы, в которой $n$ должно быть правдой в этом случае.