Спец_главы_математики

Из последней секвенции и аксиомы ('1)xt11;:::;t;:::;xnn ` ('1)xt11;:::;t;:::;xnn по правилам 8 и 12 получаем секвенцию

('1)xt11;:::;t;:::;xnn ` ('2(! : : : ('k ! Ã) : : :))xt11;:::;t;:::;xnn :

Аналогично применяя еще k ¡ 1 раз правило 8, выводим требуемую

секвенцию

('1)xt11;:::;t;:::;xnn; : : : ; ('k)xt11;:::;t;:::;xnn ` (Ã)xt11;:::;t;:::;xnn:

Следующее дерево устанавливает допустимость правила (р):

			(')tx ` (')tx		11;12;14
¡	` 8	x ';	¡; 8x ' ` (')tx
					(')x) 7
			¡	( x '
				` 8 x !	t	8: ¤
			¡ ` (')t

Покажем, что для отношения ¼ на множестве термов доказуемы обычные свойства равенства (рефлексивности, симметричности и транзитивности), т.е. доказуемо в ИПС§, что ¼ отношение эквивалентности.

Предложение 2.2.5. Для любых термов t; q; r 2 T (§) следующие секвенции доказуемы в ИПС§:

(а) ` (t ¼ t);

(б) (t ¼ q) ` (q ¼ t);

(в) (t ¼ q); (q ¼ r) ` (t ¼ r).

Д о к а з а т е л ь с т в о. Доказуемость секвенции ` (t ¼ t) устанавливается применением допустимого правила (п) из предложения 2.2.4:

`(x ¼ x):

`(t ¼ t)

Для доказательства секвенции (б) рассмотрим аксиому (t ¼ q); (z ¼

t)zt ` (z ¼ t)zq, которая равна секвенции (t ¼ q); (t ¼ t) ` (q ¼ t). Выпишем дерево, которое с участием этой аксиомы представляет до-

казательство свойства симметричности:

	`	(t	¼	t);	(t ¼ q); (t ¼ t) ` (q ¼ t)
					(t ¼ q) ` ((t ¼ t) ! (q ¼ t))7	8:
					(t ¼ q) ` (q ¼ t)

Доказуемость секвенции (в) устанавливает следующее дерево:

(t ¼ q) ` (q ¼ t);

(q ¼ t); (z ¼ r)qz ` (z ¼ r)tz

(q

¼

r)

`

((q

¼

t)

!

(t

¼

r))

11;7

8;11;12: ¤

(t ¼ q); (q ¼ r) ` (t ¼ r)

41

Пусть A = hA; §i алгебраическая система, S = S(x1; : : : ; xn) секвенция ИПС§, все свободные переменные формул которой содержатся среди x1; : : : ; xn. Будем говорить, что секвенция S истинна на элементах a1; : : : ; an 2 A в алгебраической системе A и писать

Aj= S(a1; : : : ; an), если выполняется одно из следующих условий:

1)S равна '1; : : : ; 'n ` Ã и из A j= 'i(a1; : : : ; an) для всех i = 1; : : : n

следует A j= Ã(a1; : : : ; an);

2)S равна '1; : : : ; 'n ` и хотя бы одна из формул '1; : : : ; 'n ложна на элементах a1; : : : ; an 2 A в алгебраической системе A.

Если секвенция S не истинна на элементах a1; : : : ; an 2 A в алгебраической системе A, то будем говорить, что S ложна на элементах a1; : : : ; an 2 A в A. В частности, секвенция ` ложна на любой алгебраической системе.

Секвенция S = S(x1; : : : ; xn) в ИПС§ называется тождественно истинной, если S истинна на любых элементах a1; : : : ; an 2 A в любой алгебраической системе A = hA; §i.

В дальнейшем нам предстоит доказать теорему о полноте для исчисления предикатов, установленную К. Г¨еделем и утверждающую, что класс доказуемых в ИПС§ секвенций совпадает с классом тождественно истинных секвенций ИПС§. Одна часть этого утверждения это

Теорема 2.2.6. (теорема о непротиворечивости ИПС§). Если секвенция S доказуема в ИПС§, то S тождественно истинна. В частности, не все формулы ИПС§ доказуемы в ИПС§.

Д о к а з а т е л ь с т в о проводится индукцией по высоте дерева доказательства секвенции S. Тождественная истинность аксиом ИПС§ очевидна. Проверку сохранения тождественной истинности при переходе по правилам 1–16 мы проведем на примере правила 14

¡; (')xt ` Ã ; ¡; 8x ' ` Ã

оставив рассмотрения остальных правил читателю в качестве упражнения. Итак, пусть секвенция ¡; (')xt ` Ã тождественно истинна, т.е. в предположении истинности в системе A = hA; §i на каких-то элементах a1; : : : ; an 2 A всех формул из ¡ и формулы (')xt мы имеем A j=

Ã(a1; : : : ; an). Если в системе A на каких-то элементах a1; : : : ; an 2 A истинны все формулы из ¡ и формула 8x ', то, в частности, будет

справедливо A j= (')xt (a1; : : : ; an). Значит, по условию будет верно

A j= Ã(a1; : : : ; an). Следовательно, секвенция ¡; 8x ' ` Ã тождественно истинна. ¤

42

§ 2.3. Эквивалентность формул в ИПC§

Формулы ' и Ã сигнатуры § называются эквивалентными в ИПС§ (и пишут ' ´ Ã), если секвенции ' ` Ã и Ã ` ' доказуемы в ИПС§.

В силу леммы 1.3.2 условие ' ´ Ã равносильно доказуемости секвенции ` (' $ Ã). Аналогично лемме 1.3.3 доказывается, что отношение ´ является эквивалентностью на множестве формул сигнатуры §. При этом отношение ' ´ Ã не зависит от выбора сигнатуры, содержащей все сигнатурные символы формул ' и Ã. Поэтому в дальнейшем мы будем часто говорить о доказуемости в ИПС без упоминания конкретной сигнатуры §.

Формулы ' и Ã сигнатуры § называются пропозиционально эквивалентными (и пишут ' ´P Ã), если секвенции ' ` Ã и Ã ` ' доказуемы в ИПС с использованием лишь правил 1–12.

Предложение 2.3.1. Пусть ' - '(A1; : : : ; An), Ã - Ã(A1; : : : ; An) формулы ИС, построенные из пропозициональных переменных, Â1; : : : ; Ân формулы сигнатуры §, '0 - '(Â1; : : : ; Ân), Ã0 - Ã(Â1; : : : ; Ân) формулы сигнатуры §, получающиеся из ' и Ã со-

ответственно подстановкой формул Âi вместо пропозициональных переменных. Если имеет место ' ´ Ã в ИС, то '0 ´P Ã0.

Таким образом, для любых формул ', Ã и Â сигнатуры § справедливы все утверждения лемм 1.3.4 и 1.4.1 с заменой ´ на ´P . Например, выполняется ' ^ (Ã _ Â) ´P (' ^ Ã) _ (' ^ Â).

Замечание 2.3.2. В ИП§ справедливо утверждение, аналогичное замечанию 1.5.5. Если © множество всех формул сигнатуры § с переменными из множества J, то фактор-алгебра F= ´ алгебры F = h©; ^; _; :; :(x ¼ x); (x ¼ x)i является булевой алгеброй.

Предложение 2.3.3. В ИПС выполнимы все следующие эквивалентности, в которых предполагается, что переменная x не входит свободно в формулу Ã:

(а) :9x ' ´ 8x :';

(б) :8x ' ´ 9x :';

(в) 9x (' _ Ã) ´ 9x ' _ Ã;

(г) 8x (' _ Ã) ´ 8x ' _ Ã;

(д) x ('

^

Ã)

x '

^

Ã;

(е)

8

x ('

^

Ã)

´ 8

x '

^

Ã;

9

´ 9x

(ж) 8x ' ´ 8y (')y ;

x

(з) 9x ' ´ 9y (')y .

Д о к а з а т е л ь с т в о. Приведем деревья, обосновывающие эквивалентности (а), (в) и (ж), оставляя проверку остальных читателю. При этом в пункте (а) мы будем использовать допустимое правило

' ` :Ã, которое легко выводится с помощью закона двойного отрица-

à ` :'

43

ния, а в пункте (ж) равенство ((')xy )yx = '.

(а)

' ` '

:' ` :'

'

14

x

'

15

8

:

` :

' ` 9x '

л

' ` :8x :'

16

:9x ' ` :'

13;

9x ' ` :8x :'

;

(в)

:9x ' ` 8x :'

8x :' ` :9x '

' ` '

15

à ` Ã

'

' ` 9x '

Ã;

4

Ã

Ã;

5 '

_

Ã

`

'

_

Ã

` 9

x '

_

` 9

x '

_

6;

' _ Ã ` 9x ' _ Ã

16

9x (' _ Ã) ` 9x ' _ Ã

' ` '

4

à ` Ã

' ` ' _ Ã

15

5

' ` 9x (' _ Ã)

16

Ã

à ` ' _ Ã

Ã);

15

x '

_

Ã

` 9

x '

_

Ã

x '

x ('

Ã);

x ('

9

9

` 9

_

` 9

_

6;

(ж)

9x ' _ Ã ` 9x (' _ Ã)

(')yx ` (')yx

((')yx)xy ` '

8x ' ` (')yx

14

13;

8y (')yx ` '

14

13: ¤

x

x

8x ' ` 8y (')y

8y (')y ` 8x '

Теорема 2.3.4. (теорема о замене). Пусть ' формула сигнатуры §, Ã ее подформула, а формула '0 получается из ' заменой некоторого вхождения Ã на формулу Ã0 сигнатуры §. Тогда если

ô Ã0, то ' ´ '0.

До к а з а т е л ь с т в о. Если ' = Ã, утверждение тривиально. Если ' 6= Ã, воспользуемся индукцией по числу шагов построения формулы '. Предполагая, что ' атомарная формула, снова получаем ' = Ã. Индукционный переход осуществляется рассмотрением

шести случаев: ' = :'1, ' = '1 ^ '2, ' = '1 _ '2, ' = '1 ! '2, ' = 8x '1, ' = 9x '1. В каждом из этих случаев формула Ã вхо-

дит в '1 или '2. Поэтому в первых четырех случаях эквивалентность

44

' ´ '0 вытекает из индукционного предположения и аналога леммы 1.3.3. Тогда в силу индукционного предположения остается рассмотреть случаи, когда формула ' имеет вид 8x à или 9x Ã, а секвенции à ` Ã0 и Ã0 ` à доказуемы. По симметричности à и Ã0 достаточно вывести секвенции 8x à ` 8x Ã0 и 9x à ` 9x Ã0. Доказательство этих секвенций устанавливается следующими деревьями:

à ` Ã0

14

à ` Ã0

15

8x à ` Ã0

13;

à ` 9x Ã0

16:

¤

8

x Ã

` 8

x Ã0

x Ã

` 9

x Ã0

9

§2.4. Нормальные формы

Вэтом параграфе мы определим аналоги ДНФ и КНФ, имеющие место в исчислении предикатов, и укажем алгоритмы приведения произвольных формул ИПС к соответствующим формам.

Будем говорить, что бескванторная формула ' сигнатуры § находится в дизъюнктивной (конъюнктивной) нормальной форме (сокращенно ДНФ и КНФ соответственно), если ' получается из формулы ИС, находящейся в ДНФ (КНФ), подстановкой вместо пропозициональных переменных некоторых атомарных формул сигнатуры §.

Будем говорить, что формула ' сигнатуры § находится в пренексной (предклазуальной) нормальной форме (сокращенно ПНФ и ПКНФ соответственно), если ' имеет вид

Q1x1 : : : Qnxn Ã;

где Q1; : : : ; Qn кванторы, а Ã находится в ДНФ (КНФ). При этом формула Ã называется дизъюнктивным (конъюнктивным) ядром, а слово Q1x1 : : : Qnxn кванторной приставкой формулы '.

Теорема 2.4.1. Для любой формулы ' сигнатуры § существует формула Ã сигнатуры §, находящаяся в ПНФ (ПКНФ) и эквивалентная формуле '.

Д о к а з а т е л ь с т в о. Для приведения формулы ' к ПНФ (ПКНФ) на основании теоремы о замене используются эквивалентности, описанные в предложении 2.3.3, а также эквивалентность (' ! Ã) ´ (:' _ Ã). Сначала формула ' преобразуется в эквивалентную ей формулу '0, не содержащую символа импликации. Затем формула '0 последовательным вынесением кванторов (при этом, если необхо-

димо, переименовываются связанные переменные) приводится к виду Q1x1 : : : Qnxn '00, где Qi 2 f9; 8g, 1 6 i 6 n, '00 бескванторная фор-

45

мула. Наконец, формула '00 приводится к ДНФ (КНФ), как показано в § 6:4¤ и в § 1.4. ¤

П р и м е р 2.4.1. Считая формулы ' и Ã атомарными, привести к пренексной и предклазуальной нормальным формам формулу Â -

9x 8y '(x; y) ! 9x 8y Ã(x; y):

Избавясь от импликации, получаем

 ´ :9x 8y '(x; y) _ 9x 8y Ã(x; y):

Используя пп. (а, б) предложения 2.3.3 и теорему о замене, получаем

 ´ 8x 9y :'(x; y) _ 9x 8y Ã(x; y):

Так как в формуле 9x 8y Ã(x; y) переменные x, y являются связанными, то по пп. (в, г) предложения 2.3.3. имеем

 ´ 8x 9y (:'(x; y) _ 9x 8y Ã(x; y)):

Пусть u, v некоторые новые переменные. Тогда по пунктам (ж, з) предложения 2.3.3 получаем

 ´ 8x 9y (:'(x; y) _ 9u 8v Ã(u; v));

откуда

 ´ 8x 9y 9u 8v (:'(x; y) _ Ã(u; v)):

Формула :'(x; y) _ Ã(u; v) находится в ДНФ и в КНФ одновременно, а значит, формула

8x 9y 9u 8v (:'(x; y) _ Ã(u; v))

находится и в ПНФ, и в ПКНФ. ¤

§2.5. Теорема о существовании модели

Вэтом параграфе мы сформулируем основные теоремы исчисления предикатов: теорему Мальцева Г¨еделя о существовании модели для любого непротиворечивого множества формул, теорему Г¨еделя о полноте и теорему Мальцева о компактности.

Множество ¡ формул сигнатуры § называется противоречивым

или несовместным, если для некоторых формул '1; : : : ; 'n 2 ¡ в ИПС§ доказуема секвенция '1; : : : ; 'n `. Множество формул сигнатуры §, не являющееся противоречивым, называется непротиворечивым или совместным.

46

Формула Ã сигнатуры § называется логическим следствием множества ¡ формул сигнатуры §, если в ИПС§ доказуема секвенция

'1; : : : ; 'n ` Ã для некоторых формул '1; : : : ; 'n из ¡.

Из допустимого правила (з) (правила выведения из противоречия) вытекает, что любая формула Ã сигнатуры § (и, в частности, тождественно ложная формула :(x ¼ x)) является логическим следствием противоречивого множества формул сигнатуры §. С другой стороны, любая модель множества формул ¡ является моделью для любого его логического следствия. Таким образом, противоречивое множество формул ¡ не может иметь модели. Верно и обратное утверждение:

Теорема 2.5.1. (теорема о существовании модели). Если ¡ совместное множество формул сигнатуры §, то ¡ имеет модель мощности, не превосходящей maxf!; j¡jg.

Следствие 2.5.2. (теорема Г¨еделя о полноте). Любая тождественно истинная секвенция ИПС доказуема в ИПС.

Д о к а з а т е л ь с т в о. Аналогично доказательству теоремы о полноте для ИС (теорема 1.5.5) утверждение для секвенций сводится к проверке доказуемости тождественно истинных формул. Итак, пусть ' - '(x1; : : : ; xn) произвольная тождественно истинная формула, все свободные переменные которой содержатся среди переменных

x1; : : : ; xn.

Предположим, что формула ' не доказуема. Установим тогда непротиворечивость множества, состоящего из предложения 9x1; : : : ; xn :'. Действительно, предполагая его несовместность, получаем доказуемость секвенции 9x1; : : : ; xn :' `, из которой по правилу контрапозиции выводим ` :9x1; : : : ; xn :'. Тогда в силу предложения 2.3.3 доказуема секвенция ` 8x1; : : : ; xn ', откуда по предложению 2.2.4 (пункт (p)) выводится секвенция ` ', что противоречит предположению о недоказуемости формулы '.

Из совместности множества f9x1; : : : ; xn :'g в силу теоремы о существовании модели найдется алгебраическая система A, для которой A j= 9x1; : : : ; xn :'. Последнее соотношение означает, что найдутся элементы a1; : : : ; an 2 A, опровергающие предположение о тождественной истинности формулы '. ¤

Таким образом, по теореме Г¨еделя проверка доказуемости формулы ' сводится к проверке ее тождественной истинности. Однако в отличие от ИВ в общем случае не существует алгоритма распознавания доказуемости формул ИПС§, т. е. ИПС§ неразрешимо. Тем не менее если в формуле ' “записать”, что каждая переменная может принимать конечное число значений, то перебором всех возможных систем

47

можно установить, является ли формула тождественно истинной или нет. В § 2.8 будет описан метод резолюций в исчислении предикатов, который, как и метод резолюций в ИВ, позволяет определять невыполнимость формул.

Множество формул ¡ называется локально выполнимым, если любое конечное подмножество ¡0 множества ¡ выполнимо.

Следствие 2.5.3. (теорема Мальцева о компактности). Каждое локально выполнимое множество ¡ формул сигнатуры § выполнимо.

Д о к а з а т е л ь с т в о. Допустим, что выполнимо любое конечное подмножество формул множества ¡, а само ¡ невыполнимо. Тогда по теореме о существовании модели оно противоречиво, т. е. найдутся такие формулы '1; : : : ; 'n 2 ¡, что доказуема секвенция '1; : : : ; 'n `. Следовательно, нашлось несовместное, а значит, невыполнимое конечное множество формул из ¡. Полученное противоречие доказывает теорему компактности. ¤

Следствие 2.5.4. Если для любого n 2 ! множество формул ¡ сигнатуры § имеет модель мощности > n, то ¡ имеет бесконечную модель.

Д о к а з а т е л ь с т в о. Рассмотрим множество ¡0 = ¡[f9x1; : : : ; xn (:(x1 ¼ x2) ^ :(x1 ¼ x3) ^ : : : ^ :(xn¡1 ¼ xn)) j n 2 !g. По предположению для любого n 2 ! множество ¡ [ f9x1; : : : ; xn (:(x1 ¼

x2) ^ :(x1 ¼ x3) ^ : : : ^ :(xn¡1 ¼ xn))g выполнимо. Значит, множество ¡0 локально выполнимо. По теореме компактности получаем выполни-

мость множества ¡0. Но ¡0 может иметь только бесконечные модели. Следовательно, найдется бесконечная модель M множества ¡0, которая, в частности, является моделью для ¡. ¤

§ 2.6. Исчисление предикатов гильбертовского типа

Зафиксируем произвольную сигнатуру § и определим исчисление предикатов гильбертовского типа, относящееся к сигнатуре § (ИП§). Затем мы установим эквивалентность исчислений ИП§ и ИПС§ подобно тому, как была показана эквивалентность исчислений ИС и ИВ.

Формулами ИП§ будут формулы сигнатуры §. Секвенций в ИП§ нет.

Аксиомами ИП§ являются следующие формулы для любых формул ', Ã, Â сигнатуры §, переменных x; y; z и термов t 2 T (§), удовлетворяющих условиям на записи (')xt , (')zx, (')zy:

48

1)' ! (Ã ! ');

2)(' ! Ã) ! ((' ! (Ã ! Â)) ! (' ! Â));

3)(' ^ Ã) ! ';

4)(' ^ Ã) ! Ã;

5)(' ! Ã) ! ((' ! Â) ! (' ! (Ã ^ Â)));

6)' ! (' _ Ã);

7)' ! (Ã _ ');

8)(' ! Â) ! ((Ã ! Â) ! ((' _ Ã) ! Â));

9)(' ! Ã) ! ((' ! :Ã) ! :');

10)::' ! ';

11)8x ' ! (')xt ;

12)(')xt ! 9x ';

13)	(x ¼ x);	z	z
14)	(x ¼ y) ! (')x ! (')y .
Формулы 1–14¡называются ¢схемами аксиом ИП§.
Правила вывода ИП§:
	1)	'; ' ! Ã	; 2)	Ã ! '	; 3)	' ! Ã	;
		Ã				9x ' ! Ã
				Ã ! 8x '

где в правилах 2 и 3 переменная x не входит свободно в Ã.

Понятия доказательства формулы ' (` ') и вывода формулы ' из множества гипотез ¡ (¡ ` ') в ИП§ определяются аналогично соответствующим понятиям в ИВ.

Предложение 2.6.1. Для любых формул ' и Ã сигнатуры § в ИП§ справедливы следующие соотношения:

(а) ' ` 8x ';

(б) ((')xt ! Ã) ` (8x ' ! Ã);

(в) (Ã ! (')xt ) ` (Ã ! 9x ');

(г) (')xt ` 9x '.

Д о к а з а т е л ь с т в о. Для доказательства соотношения (а) рассмотрим некоторое доказуемое предложение Ã, например, Â ! Â для произвольного предложения Â сигнатуры § (доказательство формулы Â ! Â повторяет с заменой ' на Â доказательство из примера 1.6.1). Применяя правило 1 к гипотезе ' и аксиоме ' ! (Ã ! '), выводим формулу Ã ! '. Поскольку переменная x не входит свободно в Ã, по правилу 2 из Ã ! ' выводим Ã ! 8x '. Поскольку предложение Ã доказуемо, по правилу 1 выводим формулу 8x '.

Доказательство соотношения (б) состоит в выводе формулы (8x ' ! Ã) из аксиомы 8x ' ! (')xt и гипотезы ((')xt ! Ã) по правилу 1 с помощью аксиом 1 и 2.

49

Доказательство соотношения (в) заключается в выводе формулы

à ! 9x ' из гипотезы à ! (')xt и аксиомы (')xt ! 9x ' также по правилу 1 с помощью аксиом 1 и 2.

Соотношение (г) получается применением правила 1 к гипотезе (')xt и аксиоме (')xt ! 9x '. ¤

Теорема 2.6.2. (теорема о дедукции). Если ¡ [ f'; Ãg множе-

ство формул сигнатуры §, то в ИП§ из ¡; ' ` Ã следует ¡ ` ' ! Ã.

Д о к а з а т е л ь с т в о. Рассмотрим минимальный вывод Ã1; : : : ; Ãk формулы Ã = Ãk из ¡ [ f'g. Если k = 1 или Ãk получается по правилу 1, то повторяем доказательство теоремы 1.6.1. В силу минимальности вывода формулы Ã остается рассмотреть случай, когда Ã получается из Ãk¡1 по правилам 2 или 3. При этом по индукционному предположению установлено соотношение ¡ ` ' ! Ãk¡1.

Пусть формула Ã = (Â1 ! 8x Â2) получается из формулы Ãk¡1 = (Â1 ! Â2) по правилу 2, где по определению вывода переменная x не входит свободно в формулы из ¡ [ f'; Â1g. Так как ' ! (µ1 ! µ2) `

(' ^ µ1) ! µ2 и (' ^ µ1) ! µ2 ` ' ! (µ1 ! µ2) для любых формул µ1; µ2, следующая последовательность формул дополняется до вывода

формулы ' ! Ã из ¡:

' ! Ãk¡1, (' ^ Â1) ! Â2, (' ^ Â1) ! 8x Â2, ' ! (Â1 ! 8x Â2). Пусть теперь формула Ã получается по правилу 3, т.е. Ãk¡1 = (Â1 !

Â2) и Ã = (9x Â1 ! Â2), где переменная x не входит свободно в фор-

мулы из ¡ [ f'; Â2g. Так как ' ! (Â1 ! Â2) ` Â1 ! (' ! Â2) и 9x Â1 ! (' ! Â2) ` ' ! (9x Â1 ! Â2), следующая последовательность формул дополняется до вывода формулы ' ! Ã из ¡:

' ! Ãk¡1, Â1 ! (' ! Â2), 9x Â1 ! (' ! Â2), ' ! (9x Â1 ! Â2). ¤ Таким образом, как и в исчислении высказываний, в силу теоремы

о дедукции проверка выводимости '1; : : : ; 'n ` ' в ИП§ равносильна проверке доказуемости в ИП§ формулы ('1 ! (' ! : : : ! ('n !

') : : :)).

П р и м е р 2.6.1. Из соотношения ' ` 8x ', установленного в предложении 2.6.1., по теореме о дедукции в ИП§ доказуема формула ' ! 8x ' для любой формулы ' сигнатуры §.

Теорема 2.6.3. (теорема об эквивалентности ИПC§ и ИП§). 1.

Секвенция '1; : : : ; 'n ` Ã доказуема в ИПC§ тогда и только тогда, когда формула Ã выводима в ИП§ из формул '1; : : : ; 'n.

2. Секвенция '1; : : : ; 'n ` доказуема в ИПC§ тогда и только тогда, когда формула :(x ¼ x) выводима в ИП§ из формул '1; : : : ; 'n.

Из теоремы 2.6.3 вытекает непротиворечивость ИП§. Непосредственно проверяется независимость схем аксиом ИП§.

50