ИПОВС - 6 семестр / Пособие / G1

														E
										,						I
																	I
	Сравните со следующим неформальным рассуждением: «Предположим, что верно
	. Тогда, если верно , то имеет место противоречие. Поэтому верно . Мы
	доказали, что из гипотезы следует , а это значит, что верно . »
			,	I
2.						I
		( )
					E						E
3.												I
			,
				, ,									I
4.			,													I
			( ) ( )
5.	Снова разберем построение вывода. Нам необходимо построить вывод вида

( )

Заключение строится двукратным введением импликации

, ,

, I

( ) I

Но вполне очевидно, как можно получить из гипотез , , :

I,

, ,

E

,

I

( )

I

			( ) ( )					( ) ( )
		( ),			RAA		( ),		E
6.		( )					( )
				( )

RAA

1.5.2.Допустимые правила

Чтобы облегчить и ускорить поиск доказательств, сформулируем ещё несколько правил, каждое из которых является комбинацией правил вывода НД. Будем называть такие правила допустимыми.

1		2
						MT				TND
,		2
1
					I					E

15

1	2
			DS1
1, 2

Правила TND и I были доказаны в Лемме 1. Покажем правило DS1 и оставим ос-

тальные читателю в качестве упражнения.

2

2 ,

1	2 ,		E
	1, 2

Опять же, этот список ни в коем случае не нужно считать исчерпывающим!

1.5.3.Задачи для самостоятельного решения.

1.Доказать в исчислении НД:

1)( );

2)( ) ( );

3)( ( )) ;

4);

5);

6)( ) ( );

7)( ) ( ).

1.6. Корректность и полнота исчисления НД

Пора установить связь между нашими семантическим и синтаксическим подходами. У нас есть два понятия следования: отношения и ND . Оказывается, что они совпадают.

Лемма 1 (о корректности НД). ND . То есть, всякая секвенция, доказуе-

мая в НД, тождественно истинна.

Доказательство. Проведем доказательство индукцией по построению вывода в

НД.

1.Если вывод состоит только из аксиомы , , то очевидно, что , .

2.Нужно показать, что применение правил вывода НД к тождественно истинным секвенциям дает тождественно истинную секвенцию. В качестве примера докажем это для правил I и E , а для остальных оставим читателю в качестве упражне-

		ния.					1 |						2			|
		Правило I :															.
										2		|
							1
		Для любой оценки имеем																	( 1	)						( 2 ) 1.
		Если		( 1 ) 0 или								( 2 ) 0, то									( 1, 2 ) 0 и										( 1, 2	) 1.
		Если же							( 1 )					( 2 ) 1,						то				( )					( ) 1,			а значит,		( ) 1	и
		( 1, 2 ) 1.
		Правило E :						1,								2 ,					3						.
													1			2 3
		Положим 1, 2 , 3.														Тогда , , , , и для любой оценки
		( , )				( , )									( ) 1.

Если ( ) 0, то ( ) 1. Если же ( ) 1, то ( ) 1, а значит, ( ) 1 или

( ) 1. В первом случае ( , ) 1 и получается ( ) 1 и ( ) 1.

16

Множество формул называется противоречивым, если ND .

Лемма 2. Следующие утверждения эквивалентны:

1.противоречиво;

2.существует формула такая, что ND и ND ;

3.для всех формул ND .

Доказательство.

1 3) Применить правило вывода . 3 2)

Очевидно.

2 1)

Применить правило вывода E .

Лемма 3. Если выполнимо, то непротиворечиво.

Доказательство. Предположим,

что противоречиво. По лемме 1 .

Но по-

скольку выполнимо, то существует оценка , для которой

( ) 1.

Тогда

( ) 1, что

невозможно.

Лемма 4. Если , противоречиво, то ND .

Доказательство. Достаточно применить правило RAA к выводу , .

Лемма 5. Любое непротиворечивое является подмножеством некоторого макси-

мального по включению непротиворечивого множества формул .

Доказательство. Пусть 1, 2 , – все формулы ИВ. Зададим множества n индук-

тивно:

1.

0 ;

2.

{

}, если это множество непротиворечиво;

n 1

n

n

n

в противном случае;

Легко убедиться по индукции в том, что множества n непротиворечивы для всех n.

Положим теперь

n . Если

противоречиво,

то по лемме 2

существует вывод

n:

.

Он использует конечное количество гипотез 1, 2 , , m . Каждое i принадле-

жит некоторому n . Пусть n max{ni}. Тогда все i принадлежат n

и n

ND , то есть

i

n

противоречиво. А это невозможно.

Пусть теперь

– непротиворечивое множество формул и .

Тогда n

для некоторого

n.

n , n и,

следовательно,

непротиворечиво.

Но

тогда

n 1 n , n и n . Таким образом, .

Умаксимальных непротиворечивых множеств есть полезные свойства замкнутости: Лемма 6. Пусть – максимальное непротиворечивое множество. Тогда:

1.Если ND , то .

2..

3.Для всех либо , либо .

4.тогда и только тогда, когда или .

5.тогда и только тогда, когда и .

6.тогда и только тогда, когда или .

Доказательство.

1.Если , то , противоречиво. По лемме 4 ND и значит, противоре-

чиво. Пришли к противоречию.

2.Очевидно.

3.Аналогично пункту 1 (детали оставлены читателю).

4.Слева направо: предположим, что и . Тогда ND и по пункту 1

. Справа налево: если , то ND по лемме 1.5.1(2) и .

17

Если , то . Поскольку ND (задача для самостоятельного решения 1.5.3, упражнение 1(1)), .

Пункты 5 и 6 оставлены на рассмотрение читателю. Лемма 7. Если непротиворечиво, то выполнимо.

Доказательство. По лемме 5 существует максимальное непротиворечивое .

Рассмотрим следующую оценку : ( p ) 1 p . С помощью предыдущей леммы

i

i

индукцией по построению формулы легко

показать, что

( ) 1 . Отсюда

( ) 1 для всех .

Следствие. Если ND , то .

Доказательство. По лемме 4

, непротиворечиво. По лемме 7 существует оценка

такая, что

( ) 1 и

( ) 1.

Но тогда

( ) 0 и .

Это следствие и лемма о корректности в сумме дают теорему о полноте: Теорема 8 (о полноте НД). ND тогда и только тогда, когда .

Теорема 9 (о компактности ИВ). Если , то существует конечное подмножество

0 такое, что 0 .

Доказательство. По теореме о полноте, существует вывод из в исчислении НД.

Этот вывод использует конечное множество гипотез, которое и будет 0 .

1.7.Деревья выполнимости.

Уисчисления натуральной дедукции, в свою очередь, есть недостатки по сравнению с таблицами истинности:

1. Построение вывода в НД – это творческий процесс, который трудно автоматизировать. В частности, в доказательстве могут присутствовать промежуточные формулы, более сложные, чем искомый результат.

2. Сколько бы мы не строили выводы, мы никогда не убедимся в том, что какая-то секвенция невыводима (без помощи теоремы о полноте).

Есть исчисления, лишенные этих недостатков: исчисление секвенций Генцена, семантические таблицы (или деревья выполнимости) Смальяна, метод резолюций Робинсона. В этом параграфе мы рассмотрим деревья выполнимости.

Идея дерева выполнимости состоит в том, чтобы перевернуть построение таблиц истинности. Вместо того, чтобы проверять все оценки одновременно и двигаться от простых формул к сложным, мы движемся от сложных формул к простым в поисках оценки, которая сделает исходное множество формул истинным.

Начнём с простого примера. Предположим, что мы хотим найти оценку , при кото-

рой формула ( ( )) ( ) будет ложной (т.е. ( ( )) ( )). Для этого необходимо, чтобы ( ) и . Из имеем и. ( ) требует разбора вариантов – либо , либо . Первый вариант невозможен – должно быть одновременно и . Но во втором варианте получаем , что также ведет к противоречию. Таким образом, оценки , удовлетворяющей исходному условию, не существует и формула ( ( )) ( ) общезначима. Это рассуждение записывается в виде дерева следующим образом (цифры справа показывают, откуда следуют утверждения; оценка опущена, поскольку во всех строках она не меняется):

18

	1. ( ( )) ( )
	2. ( ) (1)
	3. (1)
	4. (3)
	5. (3)
6. (2)	7. (2)
	9. (7)
(4,6)	10. (7)
	(9,5)

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

, если ;

Логическим отрицанием формулы называется формула ~ иначе.

Легко видеть, что ~ для всякой формулы . Кроме того, ~ . Поэтому в вышеприведенном дереве можно заменить все вхождения на ~ и опустить знак .

Литеральными формулами называются атомарные формулы и их отрицания.

p, если 1, Для них используется обозначение p

p,если 0.

Дизъюнкция различных литералов называется элементарной дизъюнкцией. В частности, пустая дизъюнкция (т.е. 0) – также элементарная дизъюнкция.

Все нелитеральные формулы ИВ делятся на два типа: конъюнктивные (тип ) и дизъюнктивные (тип ). Они приведены в следующей таблице:

	1	2
( )
( )	~	~
( )		~

	1	2
( B)	~	~
( B)
( B)	~

В силу известных эквивалентностей 1 2 и 1 2 для всех и .

Правила построения дерева без знаков по Смальяну выглядят так:

1 1 2

2

Ккаждой нелитеральной формуле правило применяется не более одного раза.

ДВ для конечного множества исходных формул – это конечное бинарное дерево, которое изображается с корнем вверху. Из корня выходит одна ветвь, вершины которой содержат формулы из в произвольном порядке.

Ветвь дерева называется закрытой, если в ней присутствуют одновременно формулы и для какой-то формулы или формула . Если все ветви дерева закрыты, то дерево тоже называется закрытым. Незакрытые ветви и деревья называются откры-

тыми.

Формула типа рассмотрена в ветви , если 1 и 2 лежат в . Формула типа

рассмотрена в ветви , если 1 или 2 лежит в . Ветвь полна, если все нелитераль-

ные формулы в ней рассмотрены.

Открытые неполные ветви ДВ можно продолжать с помощью указанных выше правил. Легко заметить, что формула, к которой применено правило, становится рассмотрен-

19

ной Если формула, к которой применяется правило, не рассмотрена в нескольких открытых ветвях одновременно (то есть под ней лежит точка ветвления), то заключение правил пишется во всех этих ветвях.

Наконец, ДВ полно, если либо оно содержит полную открытую ветвь, либо оно закрыто.

1.7.1. Корректность и полнота исчисления ДВ

Лемма 1. Существует алгоритм, позволяющий построить полное ДВ для любого конечного множества .

Доказательство. Каноническое построение полного ДВ для производится следующим образом:

1)Выписываем одну под другой все формулы . Это исходная ветвь дерева.

2)Если есть открытые ветви и все они неполны, то выберем одну из них. В ней есть

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

Заметим, что на каждом шаге суммарная сложность еще не рассмотренных формул в ветви уменьшается, а значит, в конце концов ветвь станет полной.

Заметим, что размер построенного полного дерева зависит от того, в каком порядке мы рассматриваем формулы.

Теорема 2 (о корректности ДВ). Пусть – выполнимое конечное множество формул. Тогда всякое ДВ для открыто.

Доказательство. Индукцией по построению ДВ. Пусть – интерпретация, при которой истинно. Докажем, что у каждого ДВ для существует ветвь, множество формул которой истинно при интерпретации . Назовем такую ветвь искомой и обозначим .

База индукции очевидна: у минимального ДВ существует единственная ветвь, содер-

жащая только формулы из и потому истинная при интерпретации .

Шаг индукции: если мы продолжаем любую ветвь,

кроме , то остается искомой

ветвью. Если мы продолжаем

по

правилу EB, то

содержит 1 2

и

потому

( 1 2 ) 1. Значит, либо

( 1 ) 1,

либо

( 2 ) 1. В первом случае

( , 1) 1,

а во вто-

ром

( , 2 ) 1.

В

случае

правила

EA

имеем

( ) 1

( 1 2 ) 1

( 1)

( 2 ) 1

( , 1, 2 ) 1.

Лемма 3. Пусть – конечное множество формул,

и некоторое ДВ для содержит

открытую полную ветвь . Тогда выполнимо.

Доказательство. Пусть

p1, , pn

все переменные, входящие в . Легко видеть, что

содержит формулы вида

p1 1 , ,

pn n

для некоторых

1, , n . Поскольку открыта,

каждое i

единственно. Рассмотрим оценку такую, что

( pi ) i для всех i

от 1 до n.

Предположив, что содержит формулу , для которой ( ) 0, придем к противоречию. Соединив эти три результата, получаем следующую теорему:

Теорема 4 (о полноте ДВ). Конечное множество формул выполнимо тогда и только тогда, когда для него существует открытое полное ДВ.

Наконец, положим ST тогда и только тогда, когда все полные деревья для ,

замкнуты.

Следствие. ST тогда и только тогда, когда .

Доказательство. ST ДВ для , замкнуто , не выполнимо ,

противоречиво .

20

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

Доказательство. Немедленно следует из предыдущего следствия и алгоритма, данного в лемме 1.

1.7.2. Дизъюнктивная нормальная форма

Теорема 5 (о дизъюнктивной нормальной форме).					Существует алгоритм, позво-
ляющий для всякой формулы ,
			найти формулу	(дизъюнктивную нормальную форму
формулы ), такую, что и – конъюнкция элементарных дизъюнкций.
Доказательство.	Для		произвольного	ДВ		рассмотрим	формулу
ST ( ) { { :нерассмотренная формула в }| :открытая ветвь в }.
Легко увидеть,	что	если	дерево 1 получено расширением дерева				2 , то
ST ( 1) ST ( 2 ). Пусть теперь 2			– исходное дерево для ,		а 1	– полное. Тогда все нерас-
смотренные формулы в 1
		– литералы. Очевидно, можем взять ST ( 2 ).

1.7.3.Варианты ДВ

Вдеревьях Смальяна часто возникает избыточность за счёт того, что в случае ветвления 1 и 2 могут быть не взаимно исключающими. Это легко увидеть, построив полное

ДВ для множества p q, p q, p q, p q.

ДВЛ (деревья выполнимости с леммами) отличаются от деревьев Смальяна тем, что

правило EB заменяется на правила EBL					и EBL :
				1	2
				EB1					EB2
	1		2			1		2

~ 1 ~ 2

ДВ-KE (деревья выполнимости KE) имеют E -правила

	EA	~ 1	EBC	~ 2	EBC
1		1		1
		2		1
2

Или подробнее:

21

( )

E

~

E

~

E

~

~

( )

( )

E

E

E

~

~

( )

E

E

~

E

~

E

Кроме них, в исчислении ДВ-KE имеется правило двузначности:

BR

Для применения правила двузначности на любой ветви формула должна быть подформулой одной из нерассмотренных формул на этой ветви.

Пример 1. ДВЛ для множества p q, p q, p q, p q

		1. p q
		2. p q
		3. p q
		4. p q
	5. p (1, EB1 )	6. p (1, EB1 )
		7.q (1, EB1 )

8. p (3, EB1 )		9.q (3, EB1 )	14. p (2, EB1 )
(5,8)		10. p (3, EB1 )	(6,14)

	11. p (4, EB1	)	12. q (4, EB1 )
			13. p (4, EB1	)
	(5,8)
			(9,12)

15. q (4, EB1 )

16. p (4, EB1 )(7,15)

Цифры справа указывают, из каких формул и по каким правилам получены формулы. Пример 2. ДВ-KE для формулы (( p q) (( p q) p))

22

1. (( p q) (( p q) p)) 2. p q (1, EA)

3. (( p q) p) (1, EA) 4. p q (3, EA)

5. p (3, EA)

6.p (5, E )

7.q (2,6, EB1C )

8.q (4,6, EB1C )

(7,8)

Пример 3. ДВ-KE для множества p q, p q, p q, p q

	1. p q
	2. p q
	3. p q
	4. p q
5. p (BR)	6. p (BR)
7. q (3,5, EBC )	9.q (1,6, EBC )
1	1
8.q (4,5, EBC )	10. q (2,6, EBC )
1	1
(7,8)	(9,10)

Все результаты, доказанные выше для ДВ, переносятся также на ДВЛ и ДВ-KE.

1.8. Интуиционистская логика

Обнаружившиеся в математике к началу ХХ века противоречия (см. раздел 2.4: антиномии теории множеств) вызвали естественное желание разобраться в причинах этих противоречий и устранить их. Голландский математик Брауэр решил, что причина проблемы в слишком абстрактном подходе к математике и отходе логических связок от их интуитивного понимания. В частности, он считал, что утверждать, что формула истинна, можно только предъявив ее доказательство; причем доказательства неатомарных формул строят-

ся из доказательств подформул следующим образом:
( )	Чтобы доказать , необходимо доказать и .
( )	Чтобы доказать , необходимо либо доказать , либо доказать .
( )	Чтобы доказать , необходимо найти способ превратить любое доказатель-
ство в доказательство .
( )	Доказательства не существует.
( )	понимается как ;	то есть, чтобы доказать ,	необходимо доказать,
что у формулы нет доказательства.
Введем обозначение Pr( ) для		множества доказательств .	Тогда вышесказанное
можем перефразировать так:
( )	Pr( ) Pr( ) Pr( ).
( )	Pr( ) {0} Pr( ) {1} Pr( ).
( )	Pr( ) Pr( ) Pr( )	(множество конструктивных функций, то есть
	C
функций, заданных некоторым алгоритмом, из Pr( ) в Pr( )).
( )	Pr( ) .
( )	Pr( ) Pr( ) .
	C
Теперь мы можем писать t:Pr( )		вместо «t – доказательство ».

Примеры. Теперь мы можем рассмотреть несколько формул с интуиционистской

точки зрения:	Пусть t:Pr( ), s:Pr( ). Тогда	t, s :Pr( ). Определим следующую
1. :
функцию	fst : fst( , ) . В частности,		fst( t, s ) t Pr( ). Тогда легко ви-
	23

деть, что fst:Pr( ) Pr( ) Pr( ), то есть fst – доказательство искомой

формулы.	t:Pr( ( ))). По
2. ( ( )) ( ) : Пусть		определению это
функция, преобразующая любое доказательство s формулы		в доказательство

t(s) формулы . То есть, s:Pr( ), r:Pr( ) t(s)(r) Pr( ). Нам нужно построить доказательство формулы , то есть функцию u из Pr( ) Pr( ) в Pr( ). Но такую функцию можно определить как u( s, r ) t(s)(r). Поэтому формула ( ( )) ( ) доказуема.

3.p p : А вот этого доказать нельзя. Чтобы доказать p p, нужно доказать одну из формул p или p. Таким образом, чтобы убедить интуициониста в доказуемости p p, нужно найти единый способ, позволяющий за конечное время решить

любую математическую задачу! Очевидно, такого способа не существует.

Для формализации интуиционистского исчисления высказываний воспользуемся натуральной дедукцией. Из рассуждений, подобных вышеприведённым, мы можем убедиться, что почти все правила НД корректны с интуиционистской точки зрения. Например, рассмотрим правило E . Если у нас есть доказательство s посылки и доказательство t посылки , то s(t) является доказательством заключения .

Единственное правило НД, недопустимое с точки зрения интуиционизма, это RAA. В самом деле, посылку RAA следует понимать так: «нельзя доказать, что нельзя доказать». Но это никак не позволяет нам найти доказательство формулы .

Многие теоремы классической логики верны и в интуиционистской логике. Кроме уже вышеприведённых это, например:

1.;

2.;

3.;

4..

5.( ) ;

6.( );

7.( );

8.;

9.( );

10.( ) ( );

11..

Выводы для них всех без применения RAA легко построить. Примеры теорем классической логики, невыводимых в ИИВ:

1.p p;

2.p p;

3.p p;

4.( p q) p q;

5.q p p q;

6.( p q) p q;

7.( p q) (q p).

Разумеется, при подстановке вместо переменных неатомарных формул может получиться выводимый результат, например, ( p p) ( p p).

Итак, в интуиционистской логике двойное отрицание неэквивалентно отсутствию отрицания. Однако тройное отрицание эквивалентно однократному. Действительно,

24