3. Эквивалентность формул

Пусть V ― {Р_i | i ω} ― множество всех пропозициональных переменных ИС, F ― множество всех формул ИС. Любая функция s : V → F называется подстановкой пропозициональных переменных. Для любой формулы φF обозначим через s(φ) формулу, получающуюся из φ заменой всех пропозициональных переменных Р, входящих в φ, на формулы s(P), при этом справедливы следующие свойства:

1. s(φ)=s(φ)

2. s(φψ)=s(φ)s(ψ)

3. s(φψ)=s(φ)s(ψ)

4. s(φ→ψ)=s(φ)→s(ψ)

Пример. Если s(P₀) = P₁Р₂, s(P₁) = P₂→Рз, φ = P₀P₁, то s(φ) = ( P₁Р₂)( P₂→Рз).

Для любой секвенции (последовательности формул) R обозначим через s(R) секвенцию (последовательность формул), получающуюся из R заменой всех пропозициональных переменных Р, входящих в R, на формулы s(P), т.е. s(φ₁,…,φ_n├ψ)=s(φ₁),…,s(φ_n)├s(ψ).

Таким образом, отображение s естественным образом расширяется на множество всех выражений исчисления ИС.

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

Теорема (теорема о подстановке). Если s ― подстановка, R ― доказуемая секвенция, то - допустимое правило.

Доказательство. Предположим, что секвенция R доказуема. Индукцией по длине доказательства R покажем, что секвенция s(R) также доказуема. Если R ― аксиома, равная φ├φ, то секвенция s(R) имеет вид s(R)├ s(R) и, значит, является аксиомой. Предполагая, что R не является аксиомой, рассмотрим дерево D доказательства секвенции R. Так как заключительный переход в дереве D к секвенции R осуществляется по одному из двенадцати правил вывода, в силу индукционного предположения достаточно установить, что переход по каждому из двенадцати правил вывода с заключением R преобразуется подстановкой s к соответствующему правилу вывода с заключением s(R). Покажем, как осуществляется такое преобразование на примере правила 1. Пусть секвенция R равна Г├φψ и заключительный переход имеет вид. . Тогда подстановка s преобразует данный заключительный переход к переходу , где s(R) равно s(Г)├(s()s()) _.

В ИС обозначим через (φ ψ) формулу ИС ((φ→ψ )  (ψ→φ)). Напомним, что таблица истинности последней формулы совпадает с таблицей истинности формулы алгебры логики (φ ψ).

Лемма 1 Секвенция Г├(φψ) доказуема тогда и только тогда, когда доказуемы секвенции Г,φ├ψ иГ, ψ├ φ.

Доказательство. Предположим, что секвенция Г├ (φψ) доказуема. Тогда доказуемость секвенции Г, φ ├ψ устанавливается следующим деревом:

Доказуемость секвенции Г,ψ├ φ показывается аналогично.

Установим теперь доказуемость секвенции Г├ (φ ψ), предполагая, что секвенции Г,φ├ψ и Г,ψ├ φ доказуемы:

Формулы φ и ψ называются эквивалентными (обозначается φ  ψ), если в ИС доказуемы секвенции φ ├ ψ и ψ├ φ.

В силу леммы 1.3.2 условие φ  ψ равносильно доказуемости секвенции ├(φψ). Покажем, что отношение  образует отношение эквивалентности на множестве формул.

Лемма 2. Для любых формул φ, ψ и χ исчисления ИС справедливы следующие утверждения:

(а) φ  φ;

(б) если φ  ψ, то ψ  φ;

(в) если φψ и ψ χ, то φ χ.

Доказательство. В пункте (а) доказывать нечего, поскольку φ ├ φ ― аксиома. Пункт (б) следует из симметричности в определении отношения . Пункт (в) вытекает из правила сечения (предложение 1.2.2, в) .

Установим, что эквивалентность формул сохраняется под действием операций , ,  и →.

Лемма 3. Если φ₁ψ_1, и φ₂ψ₂, то φ₁ ψ₁, (φ₁  φ₂)  (ψ₁ψ₂), (φ₁φ₂)  (ψ₁ψ₂) и (φ₁→φ₂)(ψ₁→ψ₂).

Доказательство. В силу симметричности отношения  достаточно доказать секвенции φ₁├ψ₁, (φ₁  φ₂) ├ (ψ₁ψ₂), (φ₁φ₂) ├ (ψ₁ψ₂) и (φ₁→φ₂)├(ψ₁→ψ₂), а доказуемость этих секвенций (на примере с ) устанавливается следующими деревьями:

.

Формула ψ исчисления ИС называется подформулой формулы φ исчисления ИС, если ψ является подсловом слова φ. Место, которое занимает подформула ψ в формуле φ, называется вхождением ψ в формулу φ.

Теорема(теорема о замене). Пусть φ — формула исчисления ИС, ψ — ее подформула, а формула φ' получается из φ заменой некоторого вхождения ψ на формулу ψ'. Тогда если ψψ', то φ  φ'.

Доказательство. Если φ=ψ, то доказывать нечего. Если φ ψ, то используем индукцию по числу шагов построения формулы φ. Предполагая, что φ — пропозициональная переменная, снова получаем φ = ψ. Индукционный переход осуществляется рассмотрением четырех случаев: φ = φ₁, φ =φ₁φ₂,, φ = φ₁φ₂, φ= φ₁→φ₂- В каждом из этих случаев формула ψ входит в φ₁ или φ_2. Поэтому эквивалентность φ  φ' вытекает из индукционного предположения и леммы 1.3.3