Непротиворечивые расширения УИП

Определение. Два класса К и К' формул в УИП дедуктивно эквивалентны, если К ├ К' и К' ├ К в УИП.

Пример. Формулы

В = А(х₁,...,х_n) и С = ("х₁)...("х_n)А(х₁,...,х_n) дедуктивно эквивалентны. В самом деле, покажем, что В ├ С:

(1) А(х₁,...,х_n);

(2)├ D, где D - произвольная доказуемая в УИП формула, не содержащая переменных х₁,...,х_n;

(3) D ® А(х₁,...,х_n), ПВЗ(1);

(4) D ® ("x₁)...("х_n)А(х₁,...,х_n), последовательное применение " -правила
к (3);

(5) (" х₁)...("х_n)А(х₁,...,х_n), ПЗ(2,4), т.е. В ├ С.

Покажем теперь, что С ├ В:

(1) ("х₁)...("х_n)А(х₁,...,х_n);

(2) ├ ("х₁)...("x_n)A ® ("x₂)...("x_n)A, АБ1;

(3) ("x₂)...("x_n)A(х₁,...,х_n), ПЗ(1,2).

После конечного числа подобных шагов получим

(4) A (х₁,...,х_n ), т.е. С ├ В.

Будем в дальнейшем рассматривать УИП, в котором аксиомы А1 – А11 замкнуты квантором общности. По предыдущему замечанию полученная система аксиом дедуктивно эквивалентна ранее рас­смотренной.

Определение. Класс К замкнутых формул УИП непротиворечив, если из К в УИП нельзя вывести А и ù А одновременно ни для какой формулы А.

Лемма. Если замкнутая формула ù А невыводима из непротиворечи­вого класса К замкнутых формул, то класс К' = { К,А}непротиво­речив.

Доказательство. Допустим, что в УИП существует формула В, для которой К' ├ В и К' ├ ù В. Тогда по правилу ПВ18 приведения к абсурду получим К ├ ù А. Противоречие с условием. Следовательно, класс { К,А}непротиворечив.

Определение. Класс К замкнутых формул полон, если для любой замкнутой формулы А либо К ├ А, либо К ├ ù А.

Лемма. Если класс К замкнутых формул непротиворечив, то его можно расширить до непротиворечивого полного класса K _L замкнутых формул.

Доказательство. Пусть B₁,B₂,... - пересчет всех замкнутых формул УИП. Определим последовательность К₀,К₁,...,К_n,... классов замкнутых формул следующим образом:

K ₀ = K; K _n+1=

Ясно, что К ₀ Í K ₁ Í …Í K _n Í K _n+1 Í …

Утверждение 1. Все классы К _nнепротиворечивы.

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

БАЗИС. п = 0. Класс К₀ непротиворечив по условию.

ПРЕДПОЛОЖЕНИЕ ИНДУКЦИИ. Допустим, что класс K _nнепротиворечив.

ШАГ ИНДУКЦИИ. Покажем, что класс К _n+1 непротиворечив. Возможны следующие случаи.

1. К_п+1 = К_n. Тогда класс К_п+1 непротиворечив по предположению индукции.

2. K_n+1 = {К_n, B_n+1 }; тогда класс К_n не выводит ù В_n+1 и потому класс К_п+1 непротиворечив по предыдущей лемме.

Утверждение 1 доказано. Продолжим доказательство леммы.

Пусть K _L = K ₀ K ₁ … =

Утверждение 2. Класс K _L непротиворечив.

Доказательство. Допустим противное: класс K _L противоречив, т.е. существует формула А, для которой K _L ├ А и K _L ├ù А. Оба вывода имеют конечную длину. Пусть К_r есть класс, который содержит все формулы из K _L, встречающиеся в этих выводах. Тогда К_r ├А и К_r ├ ù А. Противоречие с непротиворечивостью класса К_r. Следовательно, класс K _L непротиворечив.

Утверждение 3. Класс K _L полон.

Доказательство. Пусть А - произвольная замкнутая формула в УИП. Тогда А есть В _j+1 при некотором j. Одно из двух: либо К_j ├ ù В _j+1, т.е. К_j ├ù А, и тогда ввиду K_j Í K _L будет K _L ├ ù А, либо неверно, что K_j ├ ù B _j+1, и тогда K_j+l = { K_j,B _j+1 } = {K_j, A }, отку­да K_j+1 ├ А, а так как K_j+1 Í K _L,то K _L ├ A.

Итак, для любой замкнутой формулы А либо K _L ├ А, либо K _L ├ ù A. Утверж-дение 3 доказано.

Получили, что класс формул K _L непротиворечив и полон. Лемма доказана.

Формализмы F и G.Пусть К - непротиворечивый класс замкнутых формул, F - формализм, полученный из УИП добавлением к нему формул класса К в качестве аксиом. Формализм F непротиворечив. Построим формализм G, расширив формализм F натуральными числами. Опишем формализм G подробнее.

Формальные символы формализма G.

1. x,y,z,... - символы предметных переменных.

2. 0,1,2,... - символы натуральных чисел.

3. P,Q,R,P₁,Q₁,R₁,… - символы предикатных переменных.

4. &,V, ®, ù, $, "- логические символы (связки).

5. (,) - скобки и запятая.

Термы формализма G.

1. Всякая предметная переменная и предметная константа есть терм.

2. Всякое натуральное число есть терм.

Формулы формализма G.

1. Если t₁,...,t_k - термы и Р - предикатная переменная, то P(t₁,...,t_k) - элементарная формула.

2. Все другие формулы получаются из элементарных с помощью булевых операций и операций навешивания кванторов.

Аксиомы исчисления G состоят из трех следующих групп..

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

Аксиомы Бернайса составляют вторую группу аксиом для G:

АБ1. ("x)A(x) ®A(t). АБ2. A(t) ® ($х)А(х),
где А(х) - формула в G со свободной переменной х, t - терм.

Формулы класса К составляют третью группу аксиом для G.

Правила вывода для G совпадают с правилами вывода для УИП.

Утверждение. Формализм G непротиворечив.

Доказательство. Допустим, что формализм G противоречив. Пусть формула В из G такова, что ├_G В и ├_G ù B; n₁,n₂,...,n_r - все сим­волы натуральных чисел, встречающиеся в выводах формул В и ù В; y₁,y₂,…,y_r - попарно различные пред-метные переменные, отличные от всех переменных, встречающихся в доказательствах формул В и ù В. Заменим в этих доказательствах каждое n_i на у_i. При этом вст­речающиеся в доказательствах формул В и ù В аксиомы
(" x)A(x) ® А(n_i) и А(n_i) ® ($х)А(х) из G перейдут в аксиомы ("x)A(x) ® А(у_i) и А(у_i) ® ($х)А(х) из УИП. Формулы В и ù В перейдут в формулы С и ù C в УИП. Доказательства для В и ù В в G перейдут в доказательства С и ù C в УИП, что противоречит непротиворечивости УИП. Следовате­льно, формализм G непротиворечив. Утверждение доказано.

Формализмы G_n. Пусть

($x₁)B₁(x₁), ($x₂)B₂(x₂),…,($x_k)B_k(x_k),…

есть пересчет всех замкнутых формул из G вида ($ х)В(х), где В(х) - формула из G, с единственной свободной переменной х. Индукцией по k зададим последовательность формализмов G _k, k = 0,1,2,...

БАЗИС. k = 0. G₀ = G. Пусть A₀ - система аксиом для G₀.

k = 1. Пусть p _l - наименьшее натуральное число, превосходящее все натуральные числа, встречающиеся в формуле ($x₁)B₁(x₁), и фо­рмула E₁ = ($x₁)B₁(x₁) ® В₁(p₁). Пусть A₁ = А₀ {E₁} есть систе­ма аксиом для G₁.

ПРЕДПОЛОЖЕНИЕ ИНДУКЦИИ. Пусть формализм G_k-1 и система аксиом A_k-1 для него уже построены.

ШАГ ИНДУКЦИИ. Построим формализм G_k и его систему аксиом A_k. Пусть p_k есть наименьшее натуральное число, превосходящее p ₁ ,p₂,…,p _k-1 и все натуральные числа, встречающиеся в формуле ($x_k)B_k(x_k); формула E_k= ($x_k)B_k(x_k) ® B_k(p _k); A_k= A_k-1 {E_k} есть система аксиом для исчисления G_k, т.е. G_kполучается добавлением к G_k-1формулы E_k в качестве аксиомы.

Формализмы G_k, k = 0,1,2,..., построены. Обозначим через Т_k множество доказуемых в G_k формул. Так как

A₀ Ì A₁ Ì …Ì A_k Ì A_k+1 Ì …, то

T₀ Í T₁ Í …Í T_k Í T_k+1 Í …,

т.е. всякая формула, доказуемая в G_k, доказуема и во всяком последующем исчислении.

Утверждение. Формализмы G_k непротиворечивы.

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

БАЗИС. k = 0. Так как G₀ = F и формализм F непротиворечив, то формализм G₀ непротиворечив.

ПРЕДПОЛОЖЕНИЕ ИНДУКЦИИ. Допустим, что формализм G_k-1 непротиворечив.

ШАГ ИНДУКЦИИ. Покажем, что формализм G_kнепротиворечив. Допустим противное: формализм G_kпротиворечив, тогда в G_kсущест­вует формула А, для которой

(1) ├ А; (2) ├ù A. Далее

(3) ├А & ù А, ПВ2(1,2);

(4) ├А & ù А ® В, (x & ù х ® y);

(5) ├ B, П3(3,4); возьмем В = ù E_k. Тогда

(6) ├ ù E_k. Так как А_k = А_k-1 {Е_k}, то А_k-1,Е_k ├ ù Е_k, а потому

(7) Е_k ├ ù E_k, откуда

(8) ├ E_k ® ù Е_k, ТД(7);

(9) ├ (Е_k ® ù E_k) ® ù Е_k, ((х ® ù х) ® х);

(10) ├ ù E_k, П3(8,9); т.е.

(11) ├ ù (($х_k)В_k(х_k) ® В_k(p_k)); откуда имеем

(12) ├ ($х_k)В_k(х_k) & ù В_k(p_k);

(13) ├ ($х_k)В_k(х_k), ПВ1(12);

(14) ├ ù В_k(p_k), ПВ1(12).

Заменим в доказательстве формулы ù В_k(p_k) в G_k-1 натуральное число p_k на переменную х_k, не встречающуюся среди других перемен­ных в доказательстве формулы ù В_k(p_k). Тогда последовательность формул (l) - (14) преобразуется в доказательство в формализме G_k-1 формулы ù В_k(х_k), а именно,

(15) ├ ù B_k(x_k). Далее справедливо

(16) ├ С, где С есть произвольная замкнутая доказуемая в УИП формула;

(17) ├ С ®ù В_k(х_k), ПВЗ(15);

(18) ├ С ® ("х_k) ù В_k(х_k), "-ПР(17);

(19) ├("x_k) ù B_k(x_k), П3(16,18);

(20) ├("х_k) ù В_k(х_k) ® ù ($х_k)В_k(х_k), Т14;

(21) ├ ù ($х_k)В_k(х_k), П3(19,20).

Получили, что в G_k-1 доказуемы формула ($х_k)В_k(х_k) и ее отри­цание. Противоречие с непротиворечивостью G_k-1. Следовательно, формализм G_k непротиворечив. Утверждение доказано.

Формализмы Н и L. Пусть

Ax = A₀ A₁ … A_k … = A_k

есть система аксиом для формализма Н. Множество

Tr = T₀ T₁ … T_k … = T_k

доказуемых в формализме Н формул состоит из всех формул, доказуемых в формализмах G_k, k = 0,1,2,....

Утверждение. Формализм Н непротиворечив.

Доказательство. Допустим противное: формализм Н противоречив, т.е. в Н существует формула А, доказуемая в Н одновременно с ù А. Оба доказательства содержат конечное число формул, каждая из которых доказуема в Н. Так как Tr = Т_k, то найдется номер r, для которого все формулы в обоих доказате-льствах содержатся в Т _r. Тогда ├ А и ├ ù A. Противоречие с непротиворе-чивостью G. Утвер­ждение доказано.

Пусть L есть непротиворечивое полное расширение формализма H.

Лемма. Если A(x) - формула с единственной свободной переменной х, то
├ _L ("x)A(x) «(├ _L A(0), ├ _L A(l),...,├ _L A(k),...).