matlogta

Ÿ 2.1. Формулы сигнатуры Σ. Истинность формулы на алгебраической системе

Зафиксируем некоторую сигнатуру Σ и счетное множество V =

fvi j i 2 !g, элементы которого будем называть переменными и обозначать буквами x, y è z, возможно, с индексами. Алфавит исчис- ления предикатов сигнатуры Σ (ÈÏΣ) состоит из следующих групп

символов:

1. Предикатные и функциональные символы, образующие сигнатуру Σ.

2. Символы переменных, составляющих множество V .

3. Символ равенства: ¼.

4. Логические связки: :, ^, _, !.

5. Кванторы: 8, 9.

6. Вспомогательные символы: левая скобка (, правая скобка ), запятая ,.

Обозначим через T (Σ) множество всех термов сигнатуры Σ, â îïðå-

делении которых используются лишь переменные из V . Очевидно, лю- áîé òåðì èç T (Σ) является словом алфавита ИПΣ.

Введем понятие атомарной формулы сигнатуры Σ:

1) åñëè t1, t2 2 T (Σ), òî (t1 ¼ t2) атомарная формула;

2) åñëè P (n) 2 Σ предикатный символ, t1, t2, : : :, tn 2 T (Σ), òî

P (t1; t2; : : : ; tn) атомарная формула;

3) никаких атомарных формул, кроме построенных по пп. 1, 2, нет. Формула сигнатуры Σ определяется следующим образом:

1)атомарная формула есть формула;

2)åñëè ', Ã формулы и x 2 V , òî :', (' ^ Ã), (' _ Ã), (' ! Ã),

8x ', 9x ' формулы;

3) никаких формул, кроме построенных по пп. 1, 2, нет.

Символы 8, 9, использованные в определении, называются соответ-

ственно квантором всеобщности и квантором существования. Запись 8x (соответственно 9x) читается для всех x ( существует x ).

Все соглашения относительно расстановок скобок, принятые для формул исчисления высказываний, остаются в силе и для формул логики предикатов. Кроме того, вместо записей 8x1 : : : 8xn ' è 9x1 : : : 9xn '

будем использовать записи 8x1; : : : ; xn ' è 9x1; : : : ; xn '. Формула ' сигнатуры Σ называется бескванторной, если она не содержит кванторов.

31

Ï ð è ì å ð	2.1.1. 1. Рассмотрим предикатную сигнатуру
Σ = fQ(1); R(1)	; P (1); меньше(2)g со следующими интерпретациями:
Q(x) , x рациональное число,
R(x) , x вещественное число,
P (x) , x простое число,
меньше(x; y) , x < y.

Формула 8x (Q(x) ! R(x)) означает, что любое рациональное число является вещественным, а формула 8x9y (меньше(x; y) ^ P (y)) для любого элемента x найдется больший элемент y, являющийся про-

стым числом. (1) (1) Сократ(0)

2. Рассмотрим сигнатуру Σ = fA ; B ; g со следующими

интерпретациями: A(x) , x человек, B(x) , x смертен, констант-

ный символ Сократ известный древнегреческий философ. Формула 8x (A(x) ! B(x)) читается как Каждый человек смертен , а

формула A(Сократ) ! B(Сократ) означает, что Сократ смертен, если

он является человеком.

3. Любая бескванторная формула сигнатуры нульместных предикатов может рассматриваться как формула исчисления высказываний. Например, таковой является формула A _ B ! :C сигнатуры

Σ = fA(0); B(0); C(0)g. ¤

Определим множество SF(') подформул формулы ' сигнатуры Σ:

1)åñëè ' атомарная формула, то ' ее единственная подформула и SF(') = f'g;

2)åñëè ' имеет вид :'1, èëè 8x '1, èëè 9x '1, то подформула формулы ' ýòî ëèáî ', либо подформула формулы '1 è SF(') =

SF('1) [ f'g;

3) åñëè ' имеет вид '1 ^ '2, èëè '1 _ '2, èëè '1 ! '2, то подфор- мула формулы ' ýòî ëèáî ', либо подформула формулы '1, ëèáî подформула формулы '2 è SF(') = SF('1) [ SF('2) [ f'g.

П р и м е р 2.1.2. Пусть ' - 8x (9y (x ¼ F (z; y)) _ :P (z)) формула сигнатуры Σ = fF (2); P (1)g. Тогда 8x (9y (x ¼ F (z; y)) _ :P (z)),

9y (x ¼ F (z; y)) _ :P (z), 9y (x ¼ F (z; y)), (x ¼ F (z; y)), :P (z), P (z)

все подформулы формулы '. ¤

Каждое вхождение квантора 8 (9) в данную формулу ' однознач-

но определяет некоторое вхождение 8x à (9x Ã) подформулы из SF('),

первым символом которого является рассматриваемое вхождение соответствующего квантора. Формула 8x à (9x Ã), связанная с вхожде-

нием квантора 8 (9), называется областью действия этого вхождения квантора 8 (квантора 9).

32

'(x1;

находится одновременно под кванторами

Заметим, что в записи формулы возможно наложение области действия вхождения одного квантора с данной переменной на область действия другого квантора с той же самой переменной. Например, в формуле 8x (P2(x; y) ! 9x P1(x)) вхождение переменной x â P1(x)

8x è 9x. Поскольку чис-

ло переменных, образующих множество V , бесконечно, мы будем из-

бегать подобных коллизий введением новых переменных для меньших областей действия вхождений кванторов. Так, вместо формулы 8x (P2(x; y) ! 9x P1(x)) будет рассматриваться, например, формула

8x (P2(x; y) ! 9z P1(z)).

Говорят, что вхождение переменной x в формулу ' связано в ',

если оно находится в области действия некоторого вхождения квантора в формулу ', имеющую вид 8x à èëè 9x Ã; в противном случае

это вхождение называется свободным в '. Переменная x называется

свободной (связанной), если некоторое вхождение x â ' свободно (связано).

П р и м е р 2.1.3. Рассмотрим следующие формулы сигнатуры S =

fP1(1); P2(2)g:

:P1(x);

P2(x; y) ! 8x P1(x);

8x (P2(x; y) ! P1(x)).

Переменная x в первой формуле является свободной, во второй и свободной, и связанной, в третьей связанной; переменная y во всех формулах свободна. ¤

Предложением или замкнутой формулой сигнатуры Σ называется формула сигнатуры Σ, не имеющая свободных переменных.

П р и м е р 2.1.4. Формула 8x; y (x+y ¼ y +x) является предложе-

нием сигнатуры f+g,	формула			ïðåä-
	(1)	(2)9z8x (9y P2(x; y) ! :P1(x))
ложением сигнатуры	fP1	; P2	g, а формула 8x (P2(x; y) ! P1(x))

предложением не является. ¤

Запись '(x1; : : : ; xn) будет означать, что все свободные переменные формулы ' содержатся в множестве fx1; : : : ; xng.

Дадим индуктивное определение истинности формулы

: : : ; xn) сигнатуры Σ на элементах a1; : : : ; an 2 A в алгебраической системе A = hA; Σi (запись A j= '(a1; : : : ; an) будет означать, что формула ' истинна на элементах a1; : : :, an 2 A в системе A):

1) åñëè t1; t2 2 T (Σ), òî A j= (t1(a1; : : : ; an) ¼ t2(a1; : : : ; an)) , çíà-

чения термов t1, t2 в системе A на элементах a1; : : : ; an 2 A совпадают;

33

h!; +; ¢i

'(x), истинную в

2) åñëè P (k) предикатный символ сигнатуры Σ, t1, : : :, tk 2 T (Σ),

òî A j= P (t1(a1; : : : ; an); : : : ; tk(a1; : : : ; an)) , ht1(a1; : : : ; an), : : : ; tk(a1; : : : ; an)i 2 PA;

3) A j= (Ã(a1; : : : ; an) ^ Â(a1; : : : ; an)) , A j= Ã(a1; : : : ; an) è A j= Â(a1; : : : ; an);

4) A j= (Ã(a1; : : : ; an) _ Â(a1; : : : ; an)) , A j= Ã(a1; : : : ; an) èëè A j= Â(a1; : : : ; an);

5) A j= (Ã(a1; : : : ; an) ! Â(a1; : : : ; an)) , åñëè A j= Ã(a1; : : :, an), òî

Aj= Â(a1; : : : ; an);

6)A j= :Ã(a1; : : : ; an) , неверно, что A j= Ã(a1; : : : ; an);

7)A j= 8x Ã(x; a1; : : : ; an) , A j= Ã(a; a1; : : : ; an) для любого a 2 A;

8) A j= 9x Ã(x; a1; : : : ; an) , A j= Ã(a; a1; : : : ; an) для некоторого a 2 A.

Если не выполняется A j= '(a1; : : : ; an), то будем говорить, что формула ' ложна на элементах a1; : : : ; an в системе A, и писать A 6j=

'(a1; : : : ; an).

П р и м е р 2.1.5. Рассмотрим формулу '(x; y) функциональной сигнатуры f+(2); 0(0)g, имеющую вид (x + y ¼ 0). Для алгебраической системы A = hZ; +; 0i тогда и только тогда имеет место A j= '(m; n), когда m = ¡n. Для формулы Ã(x) - 9y (x + y ¼ 0) справедливо

A j= Ã(n) для любого целого числа n, поскольку у любого целого

числа имеется к нему противоположное и так же целое число. Следовательно, A j= 8x9y (x + y ¼ 0). Отметим, что A 6j= 9y8x (x + y ¼ 0),

так как нет единого целого числа, противоположного ко всем целым числам.

П р и м е р 2.1.6. 1. Записать формулу тогда и только тогда, когда x четно.

Искомая формула '(x) имеет, например, вид 9y (x ¼ y + y).

2. Записать формулу '0(x; y; z), истинную в h!; +; ¢i тогда и только

тогда, когда z наименьшее общее кратное чисел x è y.

Положим '0(x; y; z) - Ã(x; y; z) ^ Â(x; y; z), где формула Ã говорит о том, что z делится на x è íà y, а формула Â говорит о том,

÷òî z делит все общие кратные x è y, т. е. является наименьшим из всех общих кратных:

Ã- 9u; v ((z ¼ u ¢ x) ^ (z ¼ v ¢ y));

Â- 8w (9u; v ((w ¼ u ¢ x) ^ (w ¼ v ¢ y)) ! 9w1 (w ¼ w1 ¢ z)):

Èòàê, '0(x; y; z) имеет вид 9u; v ((z ¼ u¢x)^(z ¼ v¢y))^8w (9u; v ((w ¼ u ¢ x) ^ (w ¼ v ¢ y)) ! 9w1 (w ¼ w1 ¢ z)). ¤

34

Формула '(x1; : : : ; xn) сигнатуры Σ называется тождественно истинной или общезначимой (тождественно ложной или противоре- чивой), если для любой алгебраической системы A = hA; Σi è ëþáî-

го кортежа элементов (a1; : : : ; an) 2 An выполнено A j= '(a1; : : : ; an) (A 6j= '(a1; : : : ; an)). Åñëè ' тождественно истинное предложение, то пишем j= '.

Формула '(x1; : : : ; xn) называется выполнимой в системе A, åñëè

Aj= '(a1; : : : ; an) для некоторых a1; : : : ; an 2 A.

Ïр и м е р 2.1.7. 1. Формула (x ¼ x) общезначима, поскольку A j=

(a ¼ a) для любой системы A = hA; Σi и любого элемента a 2 A. По этой же причине формула :(x ¼ x) тождественно ложна.

2.Формула ' - 8x9y (x + y ¼ 0) выполнима, но не общезначима,

поскольку hZ; +; 0i j= 8x9y (x + y ¼ 0) è hN; +; 0i 6j= 8x9y (x + y ¼ 0).

Тем самым предложение ' описывает одно из характерных свойств, отличающих систему hZ; +; 0i от системы hN; +; 0i.

3.Формула ' - 8x; y (x ¢ y ¼ y ¢ x) выполнима, но не тождественно

истинна, так как hZ; ¢i j= ', à hM2(Z); ¢i 6j= ', ãäå M2(Z) множество матриц порядка 2 с элементами из Z.

4.Определим выполнимость формулы '(y) - :9x (P (x) ^ Q(x; y))

âсистеме A = hf1; 2g; P; Qi, ãäå P = f1g, Q = f(1; 1); (1; 2)g. Составим таблицу истинности предикатов P è Q:

P (1)		P (2)		Q(1; 1)		Q(1; 2)		Q(2; 1)		Q(2; 2)	,
1		0		1		1		0		0

ãäå P (a) = 1 , A j= P (a), Q(a; b) = 1 , A j= Q(a; b). По таблице истинности предикатов P è Q составляем таблицу истинности формулы

P (x) ^ Q(x; y):

x		y		P (x) ^ Q(x; y)
1		1		1
1		2		1
2		1		0
2		2		0

из которой следует, что A j= 9x (P (x)^Q(x; 1)), поскольку A j= P (1)^

Q(1; 1), а также A j= 9x (P (x) ^ Q(x; 2)), òàê êàê A j= P (1) ^ Q(1; 2).

Таким образом, A j= :'(1) è A j= :'(2), ò. å. A 6j= '(1) è A 6j= '(2). Следовательно, формула ' не выполнима в системе A.

5. Докажем выполнимость формулы 9x; y; u; v (P (x; y)^ :P (u; v))

предикатной сигнатуры Σ = fP (2)g.

Действительно, рассмотрим двухэлементную алгебраическую систему A = hfa; bg; P i c интерпретацией P = f(a; b)g. Тогда по опреде-

35

лению выполняется A j= P (a; b) è A 6j= P (b; a), ò.å. A j= P (a; b) ^ :P (b; a). Тем самым в системе A истинна формула '(x; y; u; v) - P (x; y) ^:P (u; v) на наборе элементов (a; b; b; a). Тогда A j= 9x; y; u; v (P (x; y) ^ :P (u; v)), т.е. данная формула выполнима. ¤

Как и раньше, для формул ' è Ã через (' $ Ã) будем обозначать формулу (' ! Ã) ^ (Ã ! ').

Предложение 2.1.1. 1. Для любой формулы ' сигнатуры Σ ñëå-

дующие формулы общезначимы:

(à) 8x :' $ :9x ';

(á) 9x :' $ :8x ';

(â) 8x; y ' $ 8y; x ';

(ã) 9x; y ' $ 9y; x ';

(ä) 9x8y ' ! 8y9x '.

2. Для любой формулы ' сигнатуры Σ формула 8x ' ^ 9x :' противоречива. ¤

Заметим, что на основании примера 2.1.5 общезначимость формулы 8y9x ' ! 9x8y ' в общем случае утверждать нельзя. В следующем

примере также иллюстрируется отсутствие общезначимости указан-
ной формулы для случая ' = P (x; y).
	П р и м е р 2.1.8. В графе A = hA; P i = hf1; 2; 3g;			-
			1 ²I@	¡²2
f	(1; 2), (2; 3), (3; 1)	(рис. 2.1) выполнимо A =
	gi	j	@	¡
8y 9x P (x; y), íî A 6j= 9x 8y P (x; y).				@²ª¡
	Следующая теорема позволяет создавать общезна-			3
чимые и противоречивые формулы на основе фор-			Ðèñ. 2.1
ìóë ÈÂ.

Теорема 2.1.2. Пусть '(A1; : : : ; An) общезначимая (противоречивая) формула ИВ, '1; : : : ; 'n формулы сигнатуры Σ. Тогда в результате подстановки формул '1; : : : ; 'n вместо всех соответ- ствующих вхождений пропозициональных переменных A1; : : : ; An îá- разуется общезначимая (противоречивая) формула '('1; : : : ; 'n) сигнатуры Σ.

Теорема 2.1.3. Åñëè f изоморфизм системы A на систему B,

'(x1; : : : ; xn) формула сигнатуры системы A, то для любых a1; : : : ; an 2 A свойство A j= '(a1; : : : ; an) эквивалентно свойству

B j= '(f(a1); : : : ; f(an)).

Множество формул сигнатуры Σ с множеством свободных переменных X называется выполнимым, если существует система M =

hM; Σi, элементы ax 2 M для каждого x 2 X такие, что для любой формулы '(x1; : : : ; xn) 2 выполнимо M j= '(ax1; : : : ; axn). Система

36

Σ и определим (ИПСΣ).

M называется моделью множества формул , и этот факт обознача-

ется через M j= .

П р и м е р 2.1.9. Рассмотрим следующее множество формул сигнатуры f·g, описывающих линейные порядки: lo = f8x (x · x);

8x; y; z (((x · y) ^ (y · z)) ! (x · z)); 8x; y (((x · y) ^ (y · x)) !

(x ¼ y)); 8x; y ((x · y)_(y · x))g. Очевидно, что множество lo имеет как конечные, так и бесконечные модели. Например, hf0g; ·i j= lo, ãäå · = f(0; 0)g, hN; ·i j= lo. Добавив к множеству lo две формулы

9x; y :(x ¼ y) è 8x; y((x · y) ^ :(x ¼ y) ! 9z ((x · z) ^ :(x ¼

z) ^ (z · y) ^ :(z ¼ y))), получаем множество dlo, описывающее бес-

конечные плотные линейные порядки. Моделями множества dlo ÿâ- ляются в точности бесконечные линейно упорядоченные множества, у которых между любыми двумя различными элементами имеется некоторый промежуточный. Примерами таких моделей служат hQ; ·i è

hR; ·i. ¤

Ÿ 2.2. Секвенциальное исчисление предикатов

Зафиксируем некоторую произвольную сигнатуру

секвенциальное исчисление предикатов сигнатуры Σ

Алфавит ИПСΣ получается из алфавита ИПΣ добавлением символа

следования `, ò.å. A(ÈÏÑΣ) = Σ [ V [ f¼; :; ^; _; !; 8; 9; (; ); ; ; `g.

Формулами ИПСΣ будут формулы сигнатуры Σ.

Секвенциями ИПСΣ называются конечные последовательности следующих двух видов, где '1; : : : ; 'n; Ã формулы ИПСΣ:

'1; : : : ; 'n ` Ã; '1; : : : ; 'n ` :

Примем следующие соглашения. Пусть x1; : : : ; xn переменные,

t1; : : : ; tn термы сигнатуры Σ è ' формула сигнатуры Σ. Запись
x1;:::;xn
(')t1;:::;tn будет обозначать результат подстановки термов t1; : : : ; tn âìå-
сто всех свободных вхождений в ' переменных x1; : : : ; xn соответствен-
но, причем, если в тексте встречается запись (')x1;:::;xn
гается, что для всех						t1;:::;tn , то предпола-
			i = 1; : : : ; n ни одно свободное вхождение в '
переменной	xi	не входит в подформулу		'	âèäà	y '	èëè	9	y '	, ãäå y
						x81;:::;xn1			1
переменная, входящая в ti. Вместо записи (')t1;:::;tn							мы будем иногда

писать '(t1; : : : ; tn). При этом, наряду с тем, что переменные x1; : : : ; xn в записи '(x1; : : : ; xn) будут всегда предполагаться попарно различными, среди t1; : : : ; tn могут быть равные термы.

П р и м е р 2.2.1. 1. Обозначим через ' формулу 9x R(x; y; z), через t1 òåðì F1(y; z; u), через t2 òåðì F2(F3(z); w). Результат подста-

37

запись (')yt

новки (')y;zt1;t2 равен 9x R(x; F1(y; z; u); F2(F3(z); w)), а результат подстановки (')y;zt1;t1 равен 9x R(x; F1(y; z; u); F1(y; z; u)). Заметим, что результат последовательной подстановки может не совпадать с результатом одновременной подстановки. Например, формула ((')y )z

t1 t2 равна 9x R(x; F1(y; F2(F3(z); w); u); F2(F3(z); w)) и не совпадает с формулой

(')y;zt1;t2.

2. Для формулы ' = 9x R(x; y; z) и терма t = F (y; x; u) недопустима, поскольку после подстановки терма t вместо свободной переменной y в формуле 9x R(x; F (y; x; u); z) вхождение переменной x

â òåðì t становится связанным. ¤

Аксиомами ИПСΣ являются следующие секвенции: 1) ' ` ', ãäå ' формула сигнатуры Σ;

2) ` (x ¼ x), ãäå x		переменная;
		x1;:::;xn	x1;:::;xn	; : : :, tn; q1; : : : ; qn
3) (t1 ¼ q1); : : : ; (tn ¼ qn); (')t1;:::;tn			` (')q1;:::;qn , ãäå t1
термы сигнатуры Σ, ' формула, удовлетворяющая условиям на
записи (')x1;:::;xn	(')x1	;:::;xn
t1;:::;tn è	q1;:::;qn .

Правила вывода ИПСΣ задаются следующими записями, где ; 1 произвольные (возможно пустые) конечные последовательности формул ИПСΣ, ', Ã, Â произвольные формулы ИПСΣ.

` '; ` Ã

1.` (' ^ Ã) (введение ^).

` (' ^ Ã)

2.` ' (удаление ^).

` (' ^ Ã)

3.` Ã (удаление ^).

` '

4.` (' _ Ã) (введение _).

` Ã

5.` (' _ Ã) (введение _).

6.

; ' ` Ã; ; Â ` Ã; ` (' _ Â)

(удаление _

, или правило разбора

`

Ã

двух случаев).

7.

; ' ` Ã

(введение !

).

` (' ! Ã)

8.

` '; ` (' ! Ã)

!

).

`

Ã

(удаление

38

9.

; :' `

(удаление :

, или доказательство от противного).

`

'

10.

` '; ` :'

(выведение противоречия).

`

11.

; '; Ã; 1 ` Â

; Ã; '; 1 ` Â (перестановка посылок).

12.

` '

; Ã ` ' (утончение, или правило лишней посылки).

13.

` '

x не входит свободно в формулы из

` 8x ', где переменная

(введение 8 справа).

14.

; (')tx ` Ã

слева).

;

8

x '

`

à (введение 8

` (')x

15.` 9x 't (введение 9 справа).

; ' ` Ã

16. ; 9x ' ` Ã, где переменная x не входит свободно в Ã è â ôîð- мулы из (введение 9 слева).

Понятия линейного доказательства в ИПСΣ, доказательства в виде дерева в ИПСΣ, доказуемой в ИПСΣ секвенции (теоремы ИПСΣ) и доказуемой в ИПСΣ формулы определяются аналогично соответству-

ющим понятиям ИС на основе аксиом 1 3 и правил вывода 1 16. Также аналогично предложению 1.2.1 устанавливается

Предложение 2.2.1. Секвенция S имеет доказательство в ИПСΣ в виде дерева тогда и только тогда, когда S теорема ИПСΣ.

П р и м е р 2.2.2. Приведем доказательство в виде дерева секвенции

9x8y '(x; y) ` 8y9x '(x; y)

для любой формулы '(x; y):

'(x; y) ` '(x; y) '(x; y) ` 9x '(x; y)15 8y '(x; y) ` 9x '(x; y)14

8y '(x; y) ` 8y9x '(x; y)13 9x8y '(x; y) ` 8y9x '(x; y)16: ¤

39

Следующая теорема является синтаксическим аналогом теоремы 2.1.2 и позволяет преобразовывать доказуемые формулы ИС в доказуемые формулы ИПСΣ.

Теорема 2.2.2. Пусть '(A1; : : : ; An) доказуемая формула ИС, '1; : : : ; 'n формулы сигнатуры Σ. Тогда в результате подстановки

формул '1; : : : ; 'n вместо всех соответствующих вхождений пропозициональных переменных A1; : : : ; An образуется доказуемая в ИПСΣ

формула '('1; : : : ; 'n).

Предложение 2.2.3. Для любой формулы ', удовлетворяющей

условиям на запись (')x1;:::;xn		Σ доказуемы следующие секвен-
öèè:	t1;:::;tn , â ÈÏÑ
	x1;:::;xn
(à) 8x1x;1:;:::;x: : ;nxn ' ` (')t1;:::;tn ;
(á) (')t1;:::;tn	` 9x1; : : : ; xn '.

Определение допустимого правила в ИПСΣ совпадает с соответ-

ствующим определением допустимого правила в ИС с заменой ИС на ИПСΣ.

В следующем предложении расширяется список допустимых правил, составленный для ИС.

Предложение 2.2.4. Â ÈÏÑΣ допустимы правила (а) (о) из пред-

ложения 1:2:2, а также правила

(ï)			'1; : : : ; 'k ` Ã		(подстановка термов);
	x1;:::;xn		x1;:::;xn	x1;:::;xn
	('1)t1;:::;tn		; : : : ; ('k)t1;:::;tn	` (Ã)t1;:::;tn
(ð)	` 8x '	(удаление ).
	` (')tx		8	допустимости правил (а) (о) в ИПСΣ
Ä î ê à ç à ò å ë ü ñ ò â î

совпадает с доказательством допустимости соответствующих правил в ИС.

Для доказательства допустимости правила (п) применим k ðàç ïðà-

вило 7, начиная с секвенции '1; : : : ; 'k ` Ã, и получим доказуемость в ИПСΣ секвенции

` '1 ! ('2 ! : : : ('k ! Ã) : : :):

Затем, применяя k раз правило 13, получаем доказуемость секвенции

` 8x1; : : : ; xn ('1 ! ('2 ! : : : ('k ! Ã) : : :)):

Из доказуемости последней секвенции и секвенции (а) предложения 2.2.3 по правилу сечения выводим секвенцию

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

40