Студопедия.Орг Главная | Случайная страница | Контакты | Мы поможем в написании вашей работы!  
 

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



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

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

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

(1) А(х1,...,хn);

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

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

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

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

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

(1) ("х1)...("хn)А(х1,...,хn);

(2) ├ ("х1)...("xn)A ® ("x2)...("xn)A, АБ1;

(3) ("x2)...("xn)A(х1,...,хn), ПЗ(1,2).

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

(4) A1,...,хn ), т.е. С ├ В.

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

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

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

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

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

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

Доказательство. Пусть B1,B2,... - пересчет всех замкнутых формул УИП. Определим последовательность К01,...,Кn,... классов замкнутых формул следующим образом:


K 0 = K; K n+1=

Ясно, что К 0 Í K 1 Í …Í K n Í K n+1 Í …

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

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

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

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

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

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

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

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


Пусть K L = K 0 K 1 … =

Утверждение 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 ├ù А, и тогда ввиду Kj Í K L будет K L ├ ù А, либо неверно, что Kj ├ ù B j+1, и тогда Kj+l = { Kj,B j+1 } = {Kj, A }, отку­да Kj+1 ├ А, а так как Kj+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,P1,Q1,R1,… - символы предикатных переменных.

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

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

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

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

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

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

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

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; n1,n2,...,nr - все сим­волы натуральных чисел, встречающиеся в выводах формул В и ù В; y1,y2,…,yr - попарно различные пред-метные переменные, отличные от всех переменных, встречающихся в доказательствах формул В и ù В. Заменим в этих доказательствах каждое ni на уi. При этом вст­речающиеся в доказательствах формул В и ù В аксиомы
(" x)A(x) ® А(ni) и А(ni) ® ($х)А(х) из G перейдут в аксиомы ("x)A(x) ® А(уi) и А(уi) ® ($х)А(х) из УИП. Формулы В и ù В перейдут в формулы С и ù C в УИП. Доказательства для В и ù В в G перейдут в доказательства С и ù C в УИП, что противоречит непротиворечивости УИП. Следовате­льно, формализм G непротиворечив. Утверждение доказано.

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

($x1)B1(x1), ($x2)B2(x2),…,($xk)Bk(xk),…

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

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

k = 1. Пусть p l - наименьшее натуральное число, превосходящее все натуральные числа, встречающиеся в формуле ($x1)B1(x1), и фо­рмула E1 = ($x1)B1(x1) ® В1(p1). Пусть A1 = А0 {E1} есть систе­ма аксиом для G1.

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

ШАГ ИНДУКЦИИ. Построим формализм Gk и его систему аксиом Ak. Пусть pk есть наименьшее натуральное число, превосходящее p 1 ,p2,…,p k-1 и все натуральные числа, встречающиеся в формуле ($xk)Bk(xk); формула Ek= ($xk)Bk(xk) ® Bk(p k); Ak= Ak-1 {Ek} есть система аксиом для исчисления Gk, т.е. Gkполучается добавлением к Gk-1формулы Ek в качестве аксиомы.

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

A0 Ì A1 Ì …Ì Ak Ì Ak+1 Ì …, то

T0 Í T1 Í …Í Tk Í Tk+1 Í …,

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

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

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

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

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

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

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

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

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

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

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

(7) Еk ├ ù Ek, откуда

(8) ├ Ek ® ù Еk, ТД(7);

(9) ├ (Еk ® ù Ek) ® ù Еk, ((х ® ù х) ® х);

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

(11) ├ ù (($хkkk) ® Вk(pk)); откуда имеем

(12) ├ ($хkkk) & ù Вk(pk);

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

(14) ├ ù Вk(pk), ПВ1(12).

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

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

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

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

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

(19) ├("xk) ù Bk(xk), П3(16,18);

(20) ├("хk) ù Вkk) ® ù ($хkkk), Т14;

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

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

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

Ax = A0 A1 Ak … = Ak

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

Tr = T0 T1 Tk … = Tk

доказуемых в формализме Н формул состоит из всех формул, доказуемых в формализмах Gk, 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),...).





Дата публикования: 2015-01-23; Прочитано: 198 | Нарушение авторского права страницы | Мы поможем в написании вашей работы!



studopedia.org - Студопедия.Орг - 2014-2024 год. Студопедия не является автором материалов, которые размещены. Но предоставляет возможность бесплатного использования (0.015 с)...