Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 94
Текст из файла (страница 94)
Значит, наше утверждение о формализме (3) будет доказано, если мы покажем, что любая формула вида выводима в ()). При этом мы можем ограничиться такими формулами 6, которые не содержат явно определенных связок, т. е. отрицания и эквивалентности. Для элементарных формул 6 выводимость в (3) импликации 1 1 6 -«Л получается из установленной нами выводимости формул ) ~(а=Ь) — «а=Ь и ) ~(а~Ь)-«а~Ь.
Поэтому, для того чтобы выводимость в (3) нмпликации ) ) 'л -«и установить для любой формулы Я (из числа входящих в наше рассмотрение), достаточно установить справедливость следующих утверждении 1 — 3: 1. Если формулы 1 1З-«З и ) 16-«6 выводимы в (3), то в (3) выводима также и формула ) ) (Зйб)-«ЗЬ6. 2. Если формула ) ~6-«6 выводима в (3), то в (3) выводима также н любая формула ) ~(З -«6) †«(3 -~- 6). 3. Если З(с) — формула, не содержащая ни связанной переменной е, ни свободной переменной а, и если формула ) )З(а) — «З(а) выводима в (3), то в (3) выводима также и формула 1 1 'ФЛЗ (й) ИйЗ (Ь'). Для доказательства этих утверждений мы воспользуемся схемой 6-«З 116-«1 1З которая получается двукратным применением производной схемы Я-«З Эту схему мы будем называть схемой двойной контр а позициии и.
Кроме того (для утверждения 2), мы воспользуемся выводимой схемой формул (6 — «З)-«(116-«11З). С использованием этих схем указанные три утверждения получаются сравнительно просто. Именно: 1. С помощью двойной контрапозиции из схем ЗК6 — «3 и 3 е6-«6 мы получаем схемы 11(За6)-«11З и 11(Зй6)-«116.
С помощью этих схем со ссылкой на выводимость формул 11 3-«З и ~ )6-«6 получается выводимость формул 11(ЗЙ6)-«З и 11(ЗЬ6)«6, а следовательно, и формулы Из этои схемы в случае выводимости формулы 116-«6 мы для произвольных 3 и 6 получаем формулу З-«() ~(З-«6)-«6), а из нее формулу 1 1(З-«6) -«(З-« 6). 3. Из схемы ЧЛЗ(Л)-«З(а) двойной контрапозицией мы получаем схему 1 ) У~З(й)-«3 ~З(а). НЕПРОТИВОРЕЧИВОСТЬ ЯРИФМГТИКИ 1гл Р й з1 выход зя »ямки теории докдзятельств Следовательно, для формулы 6 (с), для которой импликация ) ) 6(а)-ь6(а) выводима, выводима также и формула 1 1756(б)-».6(а).
Наконец, если 6(с), а потому и 6(5), не содержит переменной а, отсюда по схеме (а) получается формула 1 1'дб6(б) - йУ56(б). Таким образом, действительно, для любой формулы Я формализма д) формула ) )Я-ьр! выводима в (3). Замечание. Обратим внимание, что это утверждение по своему характеру отличается от утверждений о том, что из основных схем формализма (з!) выводимы те или иные схемы формул.
Выводимая схема формул остает<я применимой и в том случае, когда к формализму добавляются какие-либо новые символы, в то время как наше утверждение о выводимости формул вида ) ) Я- Я существенным образом связано со способом построения рассматриваемых формул Я и перестает быть применимым, если мы, например, включим в формализм (3) символ дизъюнкции. Итак, наше утверждение, что любая не содержащая формульных переменных, дизъюнкций и кванторов существования формула системы (Х), выводимая в этом формализме, выводима также и в (3), доказано.
Тем самым получается, что для формул системы (Е), не содержащих формульных переменных, замена всякого выражения 911/6 выражением ",( ) Яй ) 6) и всякого выражения ЧЕЯ (5) выражением ) ЮАНЯ (5) представляет собой некоторого рода перевод, при котором каждой выводимой в (Х) формуле в качестве ее перевода соответствует некоторая формула, выводимая в (3).
Формализм (3) образует (об этом мы здесь твлько упомянем) подсистему того формализма, который был предложен Гейтиигом в качестве формализации интуиционистской арифметики '). Правда, в формализме Гейтинга отрицание фигурирует в качестве основной операции. Однако в нем выводима эквивалентность )А (А-»1+1=1), так что и здесь отрицание может быть выражено через импликацию. Возможность такого перевода обычного арифметического формализма (если ограничиться формулами без формульных переменных) в формализм Гейтинга, при котором выводимые формулы ') Не у1! ой А. 01е !опоя!еп кейе1ц дег 1п1ц111оп1«11««Ьеп Мз1Ьепзв1й,— Вцгвой«Ьет.
ргецй. Айяд. %!зз., рйуз.-тз1Ь. К1., 1930, П, будут переходить в выводимые, была установлена Геделем '). Наше рассуждение по методу совпадает с рассуждением Геделя. Из полученного результата, в частности, вытекает, что противоречие в системе (Е) дало бы также себя знать и в виде противоречия в системе (3). Действительно, в случае выводимости в системе (Е) двух формул Я и )Я в (Х) была бы выводима формула О'=О, а тогда эта формула должна была бы выводиться и в системе (3). Таким образом, оказывается, что трудность фнннтного доказательства непротиворечивости формализма всей арифметики определяется вовсе не тем, что в этом формализме содержится формализованная версия закона исключенного третьего. Препятствия возникают уже при попытке фннитно доказать непротиворечивость (3).
В самом деле, рассуждение, с помощью которого мы доказали, что наличие противоречия в (Х) имело бы в качестве следствия противоречие в (3), было вполне финитным. С другой стороны, если мы стоим на содержательной точке зрения, то формальные выводы в (3) должны истолковываться как изображения правильных с содержательной точки зрения рассуждений, и потому ввиду связи, установленной между формализмами (2) и (Д), непротиворечивость системы (Х) становится для нас очевидной.
Главная проблема содержательного истолкования формализма (3) заключается в истолковании импликации. Пожалуй, наиболее просто приходящая в голову интерпретация нмпликаций Я -э-6 как гипотетического предложения «если Я, то 6» оказывается здесь неподходящей, поскольку фигурирующие в (3) импликации, вообще говоря, не выражают зависимости от переменных условий; и, действительно, по большей части мы имеем дело с такими импликациями 31-+.6, у которых посылка Я не содержит свободных переменных. Истолкование «не Я или 6», принятое в логистике, здесь не подходит, так как оно пригодно лишь в том случае, когда в основе рассмотрения лежит закон исключенного третьего.
(Так, уже истолкование импликацни Я-~-Я дало бы нам закон «не Я нли Я».) Можно было бы попытаться дать для импликации дедуктивное (Ьетче!з1есйп(зсйе) истолкование — вроде того, чтобы каждую ') С 5 де! К. уцт 1огцрдопнй1чсЬеп А«11Ьвзе1й ццд ЕзЫео1Ьеопе.— Егй«Ья. е1вез язз1Ь, Ко!!оф, 1932. Такое же открытие вскоре после этого было еде. лево к Гекцевом. Сходное утверждение содержатся уже в ооубляковзвяой в 1925 г. работе: Колмогоров А. Н. О принципе 1ег11ото поп йз!о«.— Метем. сб., 1925, 32, е. 646 — 667.
Кзк укззывзет Гедель, в исчислении вы«к«. зывзвкй возможность перевода обычного формализма в некоторый падформзлвзм гейткяговского формализма получается вз одного замечания В. И. Глявекко; см. его работу: С 1 ! ч е и й о У. Бог чое!Чоез ро1огз де 1з Ьоб19це де М. Вгоцтчег. — Асад. тоу, де Ве12!Чце, Вц11. С!. 3с!., 5ег. 5, 1929, 15. Выход ВА РАмки теории докдздтельств 1гл. ч НЕПРОТИВОРЕЧИВОСТЬ АРИФМЕТИКИ 9 з! импликацию И-ь.а рассматривать как некоторую схему доказапзельшпва, с помощью которой мы констатируем возможность получения формулы З из формулы И.
Однако такой подход сопряжен с многими неприятностями. Во-первых, при истолковании формул вида (И-+Е)-+ 5 получается несогласованность, состоящая в том, что, с одной стороны, посылка этой импликации должна истолковываться неформально, в то время как, с другой стороны, в силу дедуктивного подхода эта посылка должна рассматриваться как формула, потому что у нас нет никаких правил для вывода следствии из неформальных предложений. А во-вторых, если бы мы попытались доказать на основе такого истолкования непротиворечивость нашего формализма, то, помимо всего прочего, мы должны были бы показать, что схема заключения Я, йб-+.~ всегда от истинных (в смысле этого истолкования) формул ведет к истинным.
Для этого мы должны были бы показать, что если формула 1: истинна, а из 1: по нашим правилам выводима формула хе, то ч. тоже истинна. Если в качестве 4Р взять какую- нибудь истинную формулу, например 0=0, то дело сведется к тому, чтобы показать, что каждая выводимая по нашим правилам формула является истинной. Но в этом как раз и заключается наша задача доказательства непротиворечивости. Этих трудностей можно избежать, последовательно интерпретируя импликацию в содержательном смысле, так, чтобы импликация И -~- З выражала возможность приходить на основании содержания формулы И к констатации содержания формулы Ят). Такой взгляд на импликацию находит, в частности, применение при брауэровском понимании импликации И-ч-О'=0 как «абсурдности».
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
