Эквивалентность формул в
Формулы φ и ψ сигнатуры Σ называются эквивалентными в (и пишут ψ ), если секвенции φ├ и ψ ├ φ доказуемы в ИПС.
Аналогично лемме 1.3.3 доказывается, что отношение является эквивалентностью на множестве формул сигнатуры Σ. При этом отношение φ не зависит от выбора сигнатуры, содержащей все сигнатурные символы формул ψ и . Поэтому в дальнейшем мы будем часто говорить о доказуемости в ИПС без упоминания конкретной сигнатуры Σ.
Формулы ψ и сигнатуры Σ называются пропозиционалъно эквивалентными (и пишут φ p ), если секвенции φ├ и ψ ├ φ доказуемы в ИПС с использованием лишь правил 1-12.
Предложение 1. Пусть φ = φ(Α1,..., Αn), =( Α1,..., Αn) — формулы ИС, построенные из пропозициональных переменных, χ1,..., χn - формулы сигнатуры Σ, '=( χ1,..., χn ), '= ψ(χ1,..., χn) — формулы сигнатуры Σ, получающиеся из φ и соответственно подстановкой формул χi вместо пропозициональных переменных. Если имеет место ψ в ИС, то φ' p'.
Таким образом, для любых формул φ, и χ сигнатуры Σ справедливы все утверждения лемм 1.3.4 и 1.4.1 с заменой на p. Например, выполняется φ ( χ)p (φ ) ( χ).
Предложение 2. В ИПС выполнимы все следующие эквивалентности, в которых предполагается, что переменная х не входит свободно в формулу φ:
(а) x x; (б) xx;
(в) x()x; (г) x()x;
(д) x()x; (е) x()x;
(ж)
xy
; (з)
xy
;
Доказательство.
Приведем
деревья, обосновывающие
эквивалентности (а), (в) и (ж), оставляя
проверку остальных
на самостоятельную работу. При этом в
пункте (а) мы будем использовать допустимое
правило
,
которое легко выводится с помощью
закона двойного отрицания, а в пункте
(ж) — равенство
.
(а)
Теорема 3. (теорема о замене). Пусть φ — формула сигнатуры , — ее подформула, а формула ' получается из φ заменой некоторого вхождения на формулу ' сигнатуры Σ. Тогда если ', то φ'.
Нормальные формы
В этом параграфе мы определим аналоги ДНФ и КНФ, имеющие место в исчислении предикатов, и укажем алгоритмы приведения произвольных формул ИПС к соответствующим формам.
Будем говорить, что бескванторная формула φ сигнатуры Σ находится в дизъюнктивной (конъюнктивной) нормальной форме (сокращенно ДНФ и КНФ соответственно), если φ получается из формулы ИС, находящейся в ДНФ (КНФ), подстановкой вместо пропозициональных переменных некоторых атомарных формул сигнатуры Σ.
Будем говорить, что формула φ сигнатуры Σ находится в пренексной (предклазуальной) нормальной форме (сокращенно ПНФ и ПКНФ соответственно), если φ имеет вид
=Q1x1,..., Qnxn
где Q1,..., Qn — кванторы, а находится в ДНФ (КНФ). При этом формула называется дизъюнктивным (конъюнктивным) ядром, а слово Q1x1,..., Qnxn - кванторной приставкой формулы φ.
Теорема 1. Для любой формулы φ сигнатуры Σ существует формула сигнатуры Σ, находящаяся в ПНФ (ПКНФ) и эквивалентная формуле φ.
Доказательство. Для приведения формулы φ к ПНФ (ПКНФ) на основании теоремы о замене используются эквивалентности, описанные в предложении 2.3.3, а также эквивалентность (φ ) (). Сначала формула φ преобразуется в эквивалентную ей формулу φ', не содержащую символа импликации. Затем формула φ' последовательным вынесением кванторов (при этом, если необходимо, переименовываются связанные переменные) приводится к виду Q1x1,..., Qnxn φ", где Qi € {,}, 1<=i<=n , φ" — бескванторная формула. Наконец, формула φ" приводится к ДНФ (КНФ), как показано в 1.4.
Пример 1. Считая формулы φ и атомарными, привести к пренексной и предклазуальной нормальным формам формулу
χ = xу(x,у) ху(х,у).
Избавясь от импликации, получаем
χ = x у φ(x, у) х у (х, у).,
Используя пп. (а, б) предложения 2.3.3 и теорему о замене, получаем
= ху(х,у)х у (х, у).,
Так как в формуле х у (х, у), переменные х, у являются связанными, то по пп. (в, г) предложения 2.3.3. имеем
χ = х у (φ(x, у) х у (х, у)).
Пусть и, ν — некоторые новые переменные. Тогда по пунктам (ж, з) предложения 2.3.3 получаем
χ = ху (φ(x, у) иv(и,v)),
откуда
χ =xyuv (φ(x, у) (и,v)).
Формула φ(x, у) (и,v) находится в ДНФ и в КНФ одновременно, а значит, формула
xyuv (φ(x, у) (и,v)).находится и в ПНФ, и в ПКНФ.