145

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

С проблемой формализации неразрывно связано создание различных научных или формализованных языков. Основная цель, которая при этом преследуется, состоит в том, чтобы построить язык, свободный от недостатков обычного языка. Благодаря точности и однозначности формализованные языки находят применение там, где предъявляются повышенные требования к строгости.

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

§ 17. Теория естественного вывода

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

(!) можно получить теоремы.

Рассмотрим задание исчисления высказываний в виде теории естественного вывода.

Пусть символами являются ,&, , ,(,), A1, A2,..., а формулами - пропозициональные формы, образованные из A1, A2,... с помощью ,&, , .

Пусть А, В, С - произвольные формулы. Правила вывода задаются следующим образом. В каждом правиле вывода справа стоит символ в качестве имени этого правила. Например, одно из правил записывается в виде:

	A,B	&
	A & B

Это правило называется правилом введения конъюнкции и означает, что из А и В можно вывести А&B. Правило введения дизъюнкции

	A
	A B

означает, что из А можно вывести A B, где В - произвольная формула. Точно так же в каждом правиле вывода в "числителе" записываются гипотезы (посылки) а в "знаменателе" то, что выводится из этих гипотез.

Все правила вывода подразделяются на правила введения и правила исключения.

Правилами введения являются:

	A,B	& ;	A,B		& ;	A	;	A		.
	A & B		B & A			A B		B A

146

A├ B ;

A├ B, B .

A B

A

Правилами исключения (удаления) являются:

A & B

& ;

A & B

& ;

A

B

A,A B

A├ C, B ├ C, A B ; A ;

B

С

А

Так как в естественном выводе нет аксиом, то доказательство должно основываться на правиле введения импликации, которое говорит, что если В может быть выведено из А по правилам вывода, то A B доказано. В формальной аксиоматической теории всякая формула вывода является либо аксиомой, либо непосредственным следствием по правилам вывода из предыдущих формул этого вывода. В доказательстве естественного вывода начинаем с гипотез (т.е. с недоказанных предложений), исследуем следствия, получающиеся по правилам вывода, и затем используем информацию вида А├ В для того, чтобы заключить о доказуемости предложения A B.

Например, докажем, что для любой формулы А формула А A является теоремой. Это моментально следует, если применить правило исключения отрицания

A ,

A

т.е. А├ А, а затем правило введения импликации дает ├ А A, что и требовалось. Заметим, что при формальном аксиоматическом подходе (в теории L) доказательство того, что ├ А A было получено, не столь просто.

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

├ (A (B&C)) (A B)&(A C) (1)

Вид самой формулы для нас является подсказкой, как получить ее вывод (если он существует). Нам известно, что вводится с помощью правила введения импликации. Следовательно, прежде чем получить (1), нужно доказать, что

			C)	(2)
(A	(B&C)) ├ (A	B)&(A

Выражение (2) получим по правилу исключения дизъюнкции, если будет до-

казано		C)	(3)
A ├ (A	B)&(A
и			(4)
B&C├ (A B)&(A C)

Высказывание (3) будет доказано правилом введения конъюнкции, если будет

доказано, что		(5)
A ├ (A B) и A ├ (A C),

а (4) получим правилом введения конъюнкции из

		147
		(6)
B&C ├ (A B) и B&C├ (A C)

Ясно, что оба предложения в (5) доказуемы по правилу введения дизъюнкции.

Предложения (6) можно получить введением дизъюнкции из предложений (B&C) ├ B и (B&C) ├ C, а последнее по правилу исключения конъюнкции.

Описанную выше процедуру можно свести в следующую схему:

├(A (B&C)) (A B)&(A C)

↑введение

(A (B&C)) ├ (A B)&(A B)&(A C)

			удаление
A ├ (A B)&(A C)			B&C ├ (A B)&(A C)
	введение &			введение &
A ├ A B		A ├ A C	B&C ├ A B		B&C ├ A C
	↑	↑	↑		↑
введение введение			введение		введение
			B&C ├ B		B&C ├ C
				↑
			удаление &		↑
					удаление &

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

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

Для того, чтобы задать исчисление предикатов в виде естественного вывода, на заданные выше правила вывода накладывают некоторые ограничения

идобавляют еще примерно столько же новых правил вывода.

§18. Вопросы и темы для самопроверки

1.Эффективные и полуэффективные методы.

2.Дедуктивные теории, их классификация.

148

3.Свойства дедуктивных теорий: непротиворечивость, полнота, независимость аксиом, разрешимость.

4.Полуформальные аксиоматические теории. Пример такой теории - геометрия. В чем отличие геометрии Евклида от геометрии Лобачевского- Бойяи-Гауса?

5.Формальные аксиоматические теории. Их задание, понятие вывода, теоремы, следствия.

6.Какие вы знаете свойства выводимости?

7.Исчисление высказываний. Задание. Конечно или бесконечно множество аксиом этой теории?

8.Является ли формула А А теоремой исчисления высказываний?

9.Укажите, какие из следующих формул являются теоремами исчисления высказываний:

а) B B;	б) B B;
в) A ( A B);	г) B B;
д) A (A B);	е) ( В A) (A B);
ж) (A B) ( B A);	з) A ( B (A B));
и) (A B) (( A B) B);	к) (A B) B.

10.Производные (доказуемые) правила вывода в исчислении высказываний.

11.Эквивалентность двух определений непротиворечивости для теорий содержащих исчисление высказываний.

12.Непротиворечивость исчисления высказываний.

13.Полнота исчислений высказываний.

14.Независимость схем аксиом исчисления высказываний.

15.Разрешимость исчисления высказываний.

16.Другие аксиоматизации исчисления высказываний.

17.Задание теорий первого порядка.

18.Исчисление предикатов первого порядка, его непротиворечивость.

19.Формальная арифметика.

20.Понятие о теоремах Геделя.

21.Значение аксиоматического метода.

22.Теория естественного вывода.

Можно много видеть, читать, можно кое-что вообразить, но чтобы сделать, необходимо уметь, а умение дается только изучением техники.

М. Горький

§19. Упражнения

1.Является ли выводом в исчислении высказываний следующая последовательность формул:

1)( А ((А А) А)) (( А (А А)) ( А А)),

149

2)А ((А А) А),

3)( А (А А)) ( А А),

4)А (А А),

5)А А.

2.Доказать, что для любых формул А, В исчисления высказываний следующие формулы являются теоремами исчисления высказываний:

1) ( В В);	2) A ( А В);
3) ( В A) (A B);	4) (A B) ( B A);

5)A ( B (A B)); 6) (A B) (( A B) B).

3.Доказать, что в исчислении высказываний имеет место:

1) A├ А В;	2) A├ B A;
3) A,B├ А&В;	4) A,B├ B&A.

4.При доказательстве независимости А1 от А2 и А3 в исчислении высказываний введены выделенные формулы, см. § 11 (свойства исчисления высказываний). Составить программу на одном из языков программирования для выяснения что формула исчисления высказываний, содержащая три пропозициональные буквы, является выделенной. Используя эту программу получить, что аксиома, полученная по А2, является выделенной.

5.При доказательстве независимости А2 от А1 и А3 в исчислении высказываний введены гротескные формулы, см. § 11 (свойства исчисления высказываний). Составить программу на одном из языков программирования для выяснения, что формула исчисления высказываний содержащая две пропозициональные буквы является гротескной. Используя эту программу получить, что аксиомы, полученные по А1 либо А3, являются гротескными.

6.Пусть в исчисление высказываний примитивными связками являются , &,и . Формулы получены из пропозициональных букв с помощью этих примитивных связок. Каковы бы ни были формулы А, В и С, следующие формулы суть аксиомы теории L1:

А1: А (B А);

A2: (А (B C)) ((А B) (А C)); A3: A&B A;

A4: A&B B;

A5: A (B (A&B)); A6: A (A B);

A7: B (А B);

A8: (A C) ((B C) ((A B) C)); A9: (A B) ((A B) A);

A10: A A.

Правилом вывода теории L1 служит правило modus ponens (МР). Доказать для теории L1:

1) что формула A A является теоремой;

150

2)что верна теорема дедукции: если Г - множество формул, А,В - форму-

лы и Г,А├ В, то: Г ├ А В;

3)(A В),(B C) ├ (A C);

4)что формула В (A (A B)) является теоремой;

5)что формула В ((A&В) A) является теоремой;

6)что формула А ( A A) является теоремой;

7)что формула В ( A A) является теоремой.

7.Пусть формула А теории первого порядка является частным случаем тавтологии. Доказать, что А является теоремой в теории первого порядка.

8.Доказать следующую теорему дедукции для теорий первого порядка: Если Г - множество формул, А,В - формулы и Г,А├ В, и при этом существует такой вывод В из {Г,А} в котором ни при каком применении правила обобщения к формулам, зависящим в этом выводе от А, не связывается квантором никакая свободная переменная формулы А. Тогда: Г ├ А В.

9.Пусть А, В формулы теории первого порядка. Доказать, что в теории первого порядка имеем: х1А В ├ х1В.

10.Пусть А формула теории первого порядка. Доказать, что в теории перво-

го порядка имеем: ├ х1 х2А х2 х1А.