Teopeмa Гёделя

5 Один пример абсолютного доказательства непротиворечивости

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

Мы покажем здесь коротко, как можно формализовать элементарную логику высказываний, являющуюся некоторым фрагментом системы, описанной в Principia Mathematica. В результате формализации упомянутый фрагмент Principia станет исчислением, состоящим из неинтепретированных символов. После этого мы уже сможем провести нужнее нам доказательство.

Формализация проходит в четыре этапа. Прежде всего нам понадобится полный перечень символов, которые используются в нашем исчислении, они составят так называемый алфавит системы. Далее нам надо будет сформулировать «правила образования», согласно которым из «букв» алфавита составляются «формулы» (причем только такие, «правильно составленные», сочетания символов мы будем считать предложениями нашей системы). Можно было бы считать совокупность правил «грамматикой» исчисления. Затем мы отбираем некоторые формулы нашей системы в качестве ее аксиом (или «исходных формул»), аксиомы служат «базисом» системы. И, наконец, мы сформулируем «правила преобразования», точно описывающие, каким образом из одних формул некоторого вида «выводятся» другие формулы определенного вида; иначе говоря, правила эти — не что иное, как правила вывода. Теоремой нашей системы мы будем называть теперь любую формулу, получаемую посредством последовательного применения правил преобразования к аксиомам. Формальным «доказательством» мы будем называть любую конечную последовательность формул рассматриваемого исчисления, каждая из которых либо является аксиомой, либо выводима из предшествующих формул данной последовательности с помощью правил преобразования[1].

Алфавит логики высказываний (называемой часто «пропозициональным исчислением») очень несложен. Он состоит из переменных и констант. Переменные, поскольку вместо них можно подставлять предложения (sentences) системы, называют сентенциональными (чаще — пропозициональными) переменными. В качестве переменных мы будем использовать буквы «p», «q», «r», …, «p₁», «p₂» …, «q₁», «q₂» ….

Постоянные символы (константы) — это «пропозициональные» связки и знаки препинания. Мы будем употреблять следующие пропозициональные связки: «~» читается как «не»; ˅ — «или»; «ﬤ» — «если…, то…»; «·» — «и»; знаки препинания: «(» — «левая скобка», «)» — «правая скобка».

^{Действительно, перечисленные связки возникли как сокращенные обозначения для указанных в скобках выражений; более того, при устном чтении формул исчисления высказываний этими выражениями часто называют соответствующие формальные символы (скажем, формула «~ p ˅ q» читается как «не p или q» и т. п.). Следует, однако, твердо помнить, что эти «названия» связок не нужны для описания исчисления (неинтерпретированного!) как такового; они относятся к его метатеории, и, скажем, электронно-вычислительная машина, производящая операции с формулами исчисления высказываний как с таковыми, в такого рода «названиях» не нуждается. — Прим. перев.}

Правила образования указывают, какие именно комбинации элементарных символов алфавита мы будем считать формулами нашего исчисления. Прежде всего формулой, по определению, является каждая пропозициональная переменная. Далее, если «S» обозначает некоторую формулу[2], то ее «формальное отрицание» «~ (S)» также есть формула. Аналогично, если «S₁» и «S₂»суть обозначения некоторых формул, то выражения «(S₁) ˅ (S₂)», «(S₁) ﬤ (S₂)» и «(S₁)·(S₂)» также суть формулы.

Примеры формул:

«p», «~ p», «(р) ﬤ (q)», «((q) ˅ (r)) ﬤ (p)».

Однако выражения «(p)(~ q)» или «((р)ﬤ(q))˅» формулами не являются, так как они не удовлетворяют приведенному здесь определению формулы[3].

Правил преобразования имеется два. Первое из них — правило подстановки (вместо пропозициональных переменных) — гласит, что из произвольной формулы можно вывести другую формулу посредством одновременной подстановки некоторой формулы вместо некоторой входящей в исходную формулу пропозициональной переменной, причем такая подстановка (одна и та же) должна производиться вместо каждого вхождения выбранной переменной. Например, из формулы «p ﬤ p» можно, подставив вместо переменной «p» переменную (а тем самым — формулу) «q», вывести формулу «q ﬤ q»; подставив в ту же исходную формулу вместо «p» формулу «p ˅ q», мы выведем формулу «(p ˅ q) ﬤ (p ˅ q)» и т. п. Или, если интерпретировать «p» и «q» как некоторые русские предложения, то из «p ﬤ p» можно, например, получить предложения «Лягушки квакают ﬤ лягушки квакают», «(Летучие мыши слепы ˅ летучие мыши едят мышей) ﬤ (летучие мыши слепы ˅ летучие мыши едят мышей)» и т. п. Второе правило преобразования — это так называемое правило отделения (или modus ponens). Согласно этому правилу из любых двух формул, имеющих соответственно вид «S₁» и «S₁ ﬤ S₂», можно вывести и формулу «S₂». Например, из формул «p ˅ ~ p» и «(p ˅ ~ p) ﬤ (p ﬤ p) мы можем вывести «p ﬤ p».

Наконец, аксиомами нашего исчисления (по существу теми же, что в Principia Mathematica[4]являются следующие четыре формулы[5];

1. (p ˅ p) ﬤ p

[если p или p, то p];

2. p ﬤ (p ˅ q)

[если p, то p или q];

3. (p ˅ q) ﬤ (q ˅ p)

[если p или q, то q или p];

4. (p ﬤ q) ﬤ ((r ˅ р) ﬤ (r ˅ q))

[если p влечет q, то (r или p) влечет (r или q)].

Здесь вначале приведены аксиомы, а в квадратных скобках указаны их «переводы» на обычный язык[6].

Каждая из приведенных аксиом представляется довольно-таки «очевидной» и тривиальной.

^{Если, конечно, иметь в виду некоторые «естественные переводы» (т. е. интерпретации!) аксиом, самих по себе никакого «смысла» не имеющих. Аналогичное замечание следует иметь в виду при чтении следующей фразы текста и всюду в аналогичных случаях далее. — Прим. перев.}

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

((p ﬤ q) ﬤ ((r ﬤ s) ﬤ t)) ﬤ ((u ﬤ ((r ﬤ s) ﬤ t)) ﬤ ((p ﬤ u) ﬤ (s ﬤ t))).

В данный момент нас, однако, не интересует вывод теорем из аксиом. Цель наша состоит в том, чтобы показать непротиворечивость этой системы аксиом, т. е. дать «абсолютное» доказательство невозможностивывода из данных аксиом с помощью правил преобразования никакой формулы S одновременно с ее формальным отрицанием ~S.

1

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

2

Именно обозначает, но не является формулой (является именем формулы); S, не принадлежащая алфавиту описываемого исчисления, относится к его метаязыку. — Прим. перев.

3

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

4

В Principia была еще аксиома «(p ˅ (q ˅ r)) ˅ (q ˅ (p ˅ r))» выводимая, однако, как установил П. Бернайс (1926), из остальных четырех аксиом. — Прим. перев.

5

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

6

«Переводы» эти, разумеется, к самому исчислению не относятся. — Прим. перев.