Полнота УИП относительно класса общезначимых формул

Теорема. Всякая доказуемая в УИП формула общезначима.

Доказательство. Индукция по длине k доказательства формулы.

БАЗИС. k = 1. Возможны следующие случаи.

1. ├ А и А есть аксиома, полученная по одной из схем аксиом А1 – А11. Тогда А общезначима как формула, полученная подстановкой в тождественно истинную формулу алгебры логики.

2. ├ В и В есть аксиома ("x)A(x) ® А(у). Покажем, что формула В общезначима. Пусть М есть множество, на котором определены свободные переменные формулы В. Возможны следующие подслучаи:

при выбранных значениях переменных высказывание (" х)А(х) лож­но. Тогда высказывание (" х)А(х) ® А(у) истинно;

высказывание ("х)A(х) истинно. Тогда высказывание А(х) истинно при любых х из М, в том числе и при х = у, т.е. А(у) истинно. Поэтому высказывание (" х)А(х) ® А(у) истинно.

2. ├ В и В есть аксиома А(у) ® ($х)А(х). Покажем, что формула В общезначима. Пусть М есть множество, на котором определены сво­бодные переменные формулы В. Возможны следующие подслучаи:

при выбранных значениях переменных высказывание А(у) ложно. Тогда высказывание А(у) ® ($х)А(х) истинно;

высказывание А(у) истинно. Тогда высказывание ($ х)А(х) истинно (при х = у) и потому (" х)А(х) ® А(у) истинно.

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

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

1. ├ А и А есть аксиома. А общезначима по случаю базиса.

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

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

Допустим, что это не так и формула А_k общезначимой не является, т.е. существует множество М, переменные формулы А_k, определенные на М, для которых получившееся высказывание С ® (" х)В(х) ложно. Тогда высказывание С истинно, а высказывание (" х)В(х) ложно, от­куда ($x)ù B(x) истинно, т.е. су-ществует предмет х = x₀ Î М, для которого ù В(х₀) истинно, а потому В(х₀) ложно. Тогда С ® В(х₀) ложно. Противоречие с общезначимостью формулы
А_i = С ® В(х). Следовательно, формула А_k общезначима.

3. ├ А в УИП и А₁,А₂,...,А_i,...,А_k (=А) есть доказательство формулы А в УИП длины k, причем формула А_k, равная ($х)В(х) ® С, получена из формулы А_i = В(х) ® С с помощью $-правила. Общезна­чимость формулы А доказывает-ся аналогично предыдущему случаю.

Приступим теперь к доказательству основной теоремы о совпаде­нии класса формул, доказуемых в УИП, и класса формул, общезначи­мых в логике предикатов. Общезначимость доказуемых формул уже ус­тановлена. Покажем теперь, что всякая общезначимая формула дока­зуема в УИП.