Формулировка исчисления высказываний с единственным правилом вывода - правилом заключения

Построим исчисление высказываний ИВ1 без правила подстановки, более удобное для исследования. Формальные символы и формулы ИВ1 совпадают с аналогичными понятиями в ИВ. Пусть А,В,С - произвольные формулы в ИВ. Введем следующие схемы аксиом.

Al) A ® (В ® А).

А2) (А ® (В ® С)) ® ((А ® В) ® (А ® С)).

A3) А & В ® А.

А4) А & В ® В.

А5) (А ® В) ® ((А ® С) ® (А ® В & С)).

А6) А ® А V В.

А7) В ® А V В.

А8) (А ® С) ® ((В ® С) ® (А V В ® С)).

А9) (А ® В) ® (ù В ® ù А).

А10) А ® ù ù А.

А11) ù ù А ® А.

Единственным правилом вывода является правило заключения.

Теорема. Классы формул, доказуемых в ИВ и в ИВ1, совпадают.

Доказательство. Покажем, что класс формул, доказуемых в ИВ1, содержится в классе формул, доказуемых в ИВ. В самом деле, пусть ├ ₁ А (т.е. формула А доказуема в ИВ1) и A₁,A₂,...,A_k (=A) есть доказательство формулы А в ИВ1. Так как все А_i тождественно ис­тинны, то ├ А_i. Каждое вхождение формулы А_i в доказательстве фор­мулы А в ИВ1 заменим на доказательство формулы А_i в ИВ. Полу­ченная последовательность формул будет доказательством формулы А в ИВ.

Покажем теперь индукцией по длине k доказательства формулы в ИВ, что класс формул, доказуемых в ИВ, содержится в классе фор­мул, доказуемых в ИВ1.

БАЗИС. k = 1. Всякая аксиома в ИВ (только аксиомы имеют длину доказательства 1) доказуема в ИВ1, ибо всякая аксиома в ИВ является аксиомой и в ИВ1.

ПРЕДПОЛОЖЕНИЕ ИНДУКЦИИ. Пусть все доказуемые в ИВ формулы с длиной доказательства меньше k доказуемы в ИВ1.

ШАГ ИНДУКЦИИ. Покажем, что все доказуемые в ИВ формулы с длиной доказательства k доказуемы в ИВ1. Пусть ├ А и А₁, А₂,..., А_k (=А) есть доказательство длины k формулы А в ИВ. Возможны следую­щие случаи.

1. А_k есть аксиома в ИВ. Тогда А_k - аксиома в ИВ1 и потому ├ ₁ А_k.

2. А_k получена подстановкой формулы С в формулу А_i(р) в дока­зательстве A₁,А₂,...,А_i(р),...,А_k, т.е. А_k = А_i(С). Так как длина доказательства формулы А_i(р) в ИВ меньше k, то по предположению индукции формула ├ ₁ А_i(р). В доказа-тельстве B₁, В₂,...,В_m(р) (=А_i(р)) формулы А_i(р) в ИВ1 заменим все вхождения р на формулу С. Полученная последовательность будет доказательством формулы А в ИВ1.

3. Формула А_k получена из формул А_i и А_i ® А_k в доказательстве A₁,...,А_i,...,А_i ® А_k,..., А_k с помощью правила заключения. Так как длины доказательств A₁,...,A_i и A₁,..., А_i,...,А_i ® А_k формул А_i и А_i ® А_kв ИВ меньше k, то по предположению индукции ├ ₁ А_i и ├ ₁ А_i ® А_k; откуда по правилу заключения ├ ₁ А_k.

Теорема доказана.