Гильберт, Бернайс - Основания математики. Теория доказательств (Гильберт Д. - Основания математики и прочие работы), страница 3

Из числа вставок и изменений особого упоминания заслуживают следующие: 1. В 3 3 гл. ГП наряду с доказательством теоремы Эрбрана, использующим некоторое обобщение первой В-теоремы, при~одится другое.еедоказательство, которое вместо этой е-теоремы использует лишь так называемую «теорему об элементарном выводе», В формулировке которой упоминания об В-символе отсутствуют вообще.

На это более простое для запоминания рассуждение мое внимание впервые обратил Эрик Стениус. ГЛАВА! 1В пгвдисловия ко второму издлнию 2. При обсуждении следствий из теоремы Эрбраиа более подробно рассматривается то из них, которое касается вопроса о заменимости обычного исчисления предикатов некоторым исчислением специального вида. Обсуждается также одно обобщение этой теоремы, не рассматривавшееся в первом издании. 3.

При доказательстве теоремы Геделя о полноте мы опираемся на некоторый «критерий неопровержимости», полученный ранее с помощью довольно длинного рассуждения. В специальной вставке мы показываем, как упомянутую ссылку иа этот критерий можно заменить более прямым рассуждением. 4. В п. а) $ 1 гл. 17 мы упростили одно доказательство, относящееся к парадоксу Ришара. 5.

В комментариях ко второй теореме Геделя мы добавили одно принадлежащее Г. Крайзелу рассуждение, показывающее необходимость соблюдения так называемых «условий на выводимость» (с. 355), без чего теорема перестает быть верной. 6. Способ введения различия чисел, применяемый в п. 6) $3 гл, Ъ', где строится бескванторный арифметический формализм, не содержащий принципа «(егПшп поп дарит», как это видно из критики П, Лоренцена, ранее производил впечатление какой-то хитрости, несмотря на отчетливое указание, что речь идет о формализации некоторого специального предположения.

Теперь это введение различия видоизменено таким образом, что упомянутого недоразумения можно больше не бояться. 7. В 9 7 Приложения Гу', где рассматривается логика второй ступени с применением связанных формульных переменных, один из выводов заменен более простым. Кроме того, сведение рекурсивного определения к явному, выполненное в первом издании методом Дедекинда, видоизменено по указанному П.

Лореиценом способу. При этом, как ни странно, оказалось, что в данном формализованном изложении требуется произвести лишь одно незначительное изменение. Последнее объясняется тем, что в рассматриваемой формальной системе высказывания о функциях переводимы в высказывания о предикатах. Я снова хотел бы выразить мою сердечную благодарность господам Герту Мюллеру и Дирку Зифкесу за их активное участие в чтении корректур и за внесение дополнений в предметный указатель.

Равным образом я хотел бы поблагодарить господина Дитера Реддинга за составление именного указателя. Господину Л. Кальмару я сердечно благодарен за то, что он уже много лет тому назад предоставил мне для опубликования свое прекрасное ° доказательство непротиворечивости. Господина Г. Крайзела я сердечно благодарю за его вклад в дискуссию по поводу второй теоремы Геделя. Цюрих, март!970 в. Пауль Бернайс МЕТОД ИСКЛЮЧЕНИЯ СВЯЗАННЫХ ПЕРЕМЕННЫХ ПРИ ПОМОЩИ ГИЛЪБЕРТОВА а-СИМВОЛА й 1.

Процедура символьного решения экзистенциальных формул И сле ование логика-математического формализма, проведенное нами в т. 1, укладывается в рамки так называемой ло и перво й ступени, т.е. в рамки таких способов умозаключей, п и формализации которых можно обойтись связ вязанными ни, при — связанными пер еменными одного-единственного типа, а именно— индивидными переменными '). В качестве логического исчисления для умозаключении этого типа в т.

1 было развито — по образцу того, как это было сделано неге фр ге и Расселом,— так называемое исчисление преян дикатов, которое ое в дальнейшем было пополнеио аксиомам равенства, представляющими собой формализацию понятия индентичности, а также ь-правилом '), представляющим собой формализацию понятия «тот, который» '). Мы детально рассмотрели это исчисление и способы его исполья при дедуктивном изложении аксиоматических теорий.

зования п„и Однако ряд принципиальных вопросов все еще н д д е ове ен нами до конца. ак, в Т частности, мы пока не доказали непротивореото ой формализма системы аксиом (Х) '), посредством которо чивость ,„ м в рамках исчисления предикатов формализуется р включением принципа (егПига пап йа(иг для целых чисел. Кроме того, мы пока не ответили на вопрос о том, можно ли, вводя соответствующие функциональные и индивндные символы, обходиться без экзистенциальных аксиом. Этот вопрос мы разберем в первую очередь, так как рассмотрение его одновременно приведет нас и к тем методам, с помощью которых Гильберт начал ') Г системах вхсвом, термин первая ступень и р в ь пел«сооб в»во оворя о — ввзыввть, хзх это в Увот еблвть в узком смысле этого слона, э именно в в !Ч г.

1 (см. с. 199), свстемо.~ в«свои первой ступени твхую делзлось в гл. г. см. с. мв бвз,„о м львых перемеи- систему, аксиомы которой мзобрзжвются формулвмв бв р у .1, вых в, следовательно, являются сов отвез вымя ми в в омом хм в (см. т. гл, )т111, с, 511), ') См. т. 1, с. 467 в Приложение 1, с. 464. ') С л вывода этого фоомзлвзмз в ховспвятввяом ваде Символика в правила првведевы в Приложении 1 (см. с, 457 в далее. ') См. т. 1, ю 454. !в ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРГМЕННЫХ й и СИМВОЛЬНОЕ РЕШЕНИЕ ЭКЗИСТЕНЦИАЛЬНЫХ ФОРМУЛ 19 !Гл. ! наступление на проблему доказательства непротиворечивости арифметического формализма.

сна Чтобы отчетливо уяснить себе постановку этой пробле чала рассмотрим один частный случай, для которого ответ на наш вопрос уже был получен ранее. Итак, пусть в какой-либо системе аксиом Ж с аксиомами равенства имеется экзистенциальная аксиома Зхй((а, ..., л, х), не содержащая никаких других свободных переменных, кроме а,, й. Пусть из аксиом системы «О может быть выведена формула )гхч!у(21 (а, ..., й, х) ЬЯ(а, ..., й, у)-+.Х=у) (например.

эта формула может являться одной из аксиом рассматриваемой нами системы). Тогда по г-правилу мы можем ввести терм «,Я (а, ..., й, х) и использовать формулу Я (а, ..., й,ь Я (а, ..., й, х)) в качестве исходной. Если мы теперь при помощи явного опре- 1(а, ..., Й) = «,Я (а...,, й введем функциональный знак 1(а, ..., й), то получим фо , то получим формулу Я(а, ..., й, ! (а, ..., й)). Эта формула может заменить собой нашу экзистеициа аксиому т ициальную =)ХЯ(а...,, л, х).

Действительно, воспользовавшись основной формулой (Ь) исчисления предикатов, мы немедленно выведем из э й фо . упомянутую аксиому ЗХЯ(и, ..., й, х). Так мы приходим к й я от прежней некоторой новой системе аксиом чо', отличающейся системы (О тем, что в ней появился функциональный знак ! (а,,й), а вместо формулы ВХЯ(а, ..., й, х) в качестве аксиомы взята ормула Я (а, ..., й, 1 (а, ..., Й)). Этот переход от системы (О к системе «О' мы осуществляем с использованием ь-правила. Пользуясь нашим общим методом устра- пения ь-символов' ), мы можем произвести и обратный переход от кУ' к Я. Таким образом, получается, что системы «О и Я' равнозначны в следу!ощем точном смысле: Всякая формула, построенная в формализме системы Я', с помощью аксиом этой системы переводима в некоторую другую формулу, не содержа:цую функционального знака ( и, следовательно, принадлежащу!о формализму системы (О.

Л!Обая формула, ие содержащая функционального знака ! и выводимая средствами системы бб', выводима также и средствами системы Я. Вследствие сказанного можно говорить о заменимости экзистенциальной аксиомы =)х21 (а, ..., й, х) аксиомои Я (а, ..., й, ( (и, й)) Таким образом, в результате введения функционального знака ((а,..., Й) указанная экзистенциальная аксиома становится ненужной. Рассмотренный метод, позволяющий получить этот результат непосредственно, связан с одной особенностью нашего формализма. Именно, возможность применения ь-правила в данном случае была основана на том, что в нашем формализме в качестве аксиомы или в качестве выводимой формулы имелась формула хйх1(у (Я (а, ..., й, х)(й Я (а, ..., й, у) -ьх = у). Теперь естественно возникает вопрос о том, нельзя ли получить аналогичный результат и без использования этого предположения.

Для экзистенциального высказывания без параметров, которому соответствует формула Лей( (е) без свободных переменных, положительный ответ на этот вопрос был получен раньше при помощи рассуждения, которое в гл. 1ьг т. 1 приводилось в качестве примера использования дедукционной теоремы а). В этом примере мы рассматривали способ умозаключений, состоящий в том, что после доказательства теоремы существования типа «Существует объект х, для которого имеет место Я(х)» вводится специальный индивидный символ 6 и далее проводится рассуждение: «Пусть б — объект, обладающий свой- В См. т. 1, гл. У!11, с, З!Π— 532. Тап пап зтп рассуждение носит всего лпшь подготовительный характер, пе будет большой беды, если отдельные дегалп приведенного здесь доказательства покажутся чптагелв педпстатпчпо полными. з) См.