Teopeма Гёделя | страница 23
Наконец, аксиомами нашего исчисления (по существу теми же, что в 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.
Оказывается, что к числу теорем нашего исчисления относится формула «p ﬤ (~ p ﬤ q)» (выражаемая словесно следующим образом: «если p, то не p влечет q»). (Мы примем этот результат к сведению, не проводя фактического его доказательства.) Допустим, что некоторая формула S, так же как и ее отрицание ~ S, выводима из аксиом. Подставляя тогда S вместо переменной «p» в только что упомянутую теорему (пользуясь правилом подстановки) и применяя затем дважды modus ponens, мы получим, что теоремой является и формула «