2.4.4. Теорема Гёделя о неполноте

в определенной мере сущность теоремы Гёделя о неполноте дедуктивных систем содержится в следующей фразе Св. Иоанна Дамас-

«Бог есть, это очевидно. Но что есть Он по существу и естеству, - это совершенно непостижимо и неведомо» [5, с.6.

Ему предшествовал Григорий Богослов:

«...если познание имеет предметом своим вещи существующие, то уже то, что выше познания, конечно, выше и бытия, и снова: то, что превышает бытие, то выше и познания» [5, с.7.

То же, но уже в формулировке Гёделя:

Теорема 2.9. Во всякой теории первого порядка, включающей формальную арифметику,

1) существует такая (истинная) формула Л, что ни Л, ни ~iA не являются доказуемыми;

2) утверждение о непротиворечивости этой теории - это формула данной теории, которая не является доказуемой.

Доказательство. См. [8, с.298-310 или [21, с.116.

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

Традиционная история приписывает этому греческому богослову и философу следующие годы жизни - 675-753.

А.Н.Колмогоров: «Математикам хорошо известно, что в пределах каждой формальной системы, достаточно богатой математически, можно сформулировать вопросы, которые кажутся содержательными, осмысленными и должны предполагать наличие определенного ответа, хотя в пределах данной системы такого ответа найти нельзя» [15].

Собственно говоря, так вышло с доказательством непротиворечивости формальной арифметики (§ 2.4.3).

Кроме того, теорема Гёделя говорит о несостоятельности идеи полной формализации процесса логического вывода. Иначе говоря, не все может быть формализовано, как бы этого ни хотелось математикам.

2.4.5. Курт Гёдель

«Австрийский математик Курт Гёдель родился в Брно (Словакия) на двадцать семь лет позже Эйнштейна и получил физическое и математическое образование в Венском университе- те. Его научные интересы частично

1 Щ nepeceKajmcb с интересами Эйнштей-

"Звр Скромный математик - одиночка

J Гёдель, в зрелом возрасте также при ll ехавший в Принстонский институт к 1 перспективных исследований, внес важнейший вклад в основы математики, настолько революционный, что раз-Рис. 2.1: Курт Гёдель двинул границы этой дисциплины и (1906-1978). оказал существенное влияние на общее

мировоззрение и культуру 20 века» [37]. «Оказавшись в Принстоне, Гёдель предложил оригинальное решение выведенных Эйнштейном уравнений общей теории относительности. Из этого решения, между прочим, следует принципиальная возможность машины времени. Вообще же с математики он переключился на философию, увлекся трудами Лейбница - и пришел к выводу, что тот открыл - ни много ни мало - Тайну Жизни. Впрочем, по мнению Гёделя, до нас это открытие не дошло, ибо современные Лейбниглу мракобесы подвергли его сочинения жесточайшей цензуре. В последние двадцать лет жизни Гёдель не опубликовал ни одной работы. Умер он в возрасте 71 года, при явных признаках психического расстройства. Уверившись, что врачи пытаются его отравить, он отказался принимать пищу, и голодное истощение, наряду с распадом личности, фигурирует в медицинском свидетельстве о его смерти» [12].

2.5. Автоматический вывод теорем

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

Доказанная теорема - это новая открытая истина. Автоматический поиск выводов, таким образом, является открытием истин, которое доверено ЭВМ. Машина, «доказывая теорему» Л, ищет конечную последовательность формул, последняя из которых - это формула Л, удовлетворяющую определению (формального) доказательства, данного в § 2.1.1.

Одной из первых работ (1960) по созданию алгоритма автоматического вывода была статья Ван Хао [2. В СССР автоматический вывод в рамках исчисления высказываний в 1960-е годы осуществлялся на машине «Урал~4» группой Н.А.Шанина [47].

Наиболее крупными достижениями по созданию методов автоматического доказательства теорем являются «обратный метод» С.Ю.Маслова [23, 24] и «метод резолюций» Дж.Робинсона (см. §1.3).

2.5.1. СЮ. Маслов

Серхей Юрьевич MaCJЮв родился 10 июня 1939 юда. Он один из ведущих математических логиков своего поколения. Его первые исследования, подытоженные в кандидатской диссертации 1964 года, были посвящены каноническим исчислениям Поста - универсальному аппарату математической логики и теории алгоритмов.

Работы С.Ю.Маслова в области теории поиска логического вывода* и прежде всего созданный им (и опубликованный на год раньше метода резолюций) обратный метод поиска вывода известны не только логикам, но и специалистам по вычислительной науке и искусственному интеллекту. Обратный метод, поставивший его автора на одно из первых мест в мире в области поиска логического вывода, позволил получить глубокие результаты в проблеме разрешения для исчисления предикатов. СЮ.Маслов был первым не

Использована статья о С.Ю.Маслове, находящаяся на сайте: http: www.philosophy.ru/library/logic / maslov/Ol.html