Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 57
Текст из файла (страница 57)
Шурвцья опубликовали аналогичное донззз. тельство ддя нормальных форм Геделя я Пепяшз, приведенных я предварен- ному виду. Сц. Л бушЪо1!с Лог!с, !947, 12, р, бб — 73, и 1960, 13, р. 16! — 173 пгиманннин к пиозлнмн рлзоншимостн 4 51 е-симзол и логпчгскип ьоомдлизм 1гл. гп В последнее время было получено несколько глубоких результатов '); касающихся теоретико-модельных нормальных форм. В качестве особенно яркого из них мы упомянем нормальную форму Шураньи )ухвгутвггт)1(х, у, х) сг т)хвуЧиВ(х, у, и), в которой фигурируют только одна двуместная формульная переменная, а остальные формульные переменные являются одноместными '). В отношении распределения квантороз эта нормальная форма является почти оптимальной. Оптимум был достигнут в работе А.
С. Кара, Э. Ф. Мура и Хао Вана' ), где было устаповлено, что форма Ух=»ут17га(х, у, е) с двуместными формульными переменными тоже является теоретико-модельной нормальной формой. Значение теоретико-мэдельных нормальных форм становится особенно ясным, если рассмотреть связь, сущесгпвующую между формулами исчисления предикагпов и различными аксиомагпическими системами. При анализе этой связи можно ограничиться рассмотрением формул, не содержа)цих ни свободных индивидных переменных, ни формульных переменных без аргументов. Неопровержимость такой формулы исчисления предикатов равносильна непротиворечивости той аксиомы (соответственно той системы аксиом), которая изобра>кается формулой, получающейся из рассматриваемой формулы в результате замены ее формульных переменных предикатными символами с тем же самым числом аргументов.
Всли рассматриваемая формула имеет вид конъюнкции предваренных формул, то после замены формульных переменных предикатными символами мы берем каждый ее конъюнктнвный член в качестве отдельной аксиомы, От полученной таким образом системы аксиом, аксиомы которой изображаются предваренными формулами без свободных индивидных переменных, мы затем можем перейти к системе аксиом з разрешенном виде, в которой каждому квантору су)цествования без предшествующих ему кван- торов всеобщности соответствует некоторый индивидный символ, а каждому квантору существования с предшествующими 1 кван- ') По поводу литературы еы.
Ае)се гот а по Угг. 9о!чаЫе Свеев о1 Ппе ))ее)в)оп Ргоыепт. — Агоиегйагн, 1954; 5 п г а и у) 3. Йейп19цонвпьеопе йев Ел1вепеюпиявргоЫеотв пп Ргай))га!ео' а1)гп! йег егцеп 51п)е.— Впйарет1, 1959. ') Си. теорему Х в упомянутой книге Шураньи, с. 72. ') К а ь г А, 5., Мо о ге Е.
Р. %) а их Нао. Еп)ве)ге)йппзвргоыеот гейпеей ьо Ше унтг саве. — Ргое. Йас. Асай. 5е1, 1962, 48, р. 365 — 377. Авторы ссылаются на рассужления Дж. Р. Бюхи (Л. Й. ВпсЫ). торами всеобщности соответствует некоторый функциональный знак с 1 аргументами. В отношении непротиворечивости эта система аксиом в разрешенном виде равносильна прежней системе аксиом.
Таким образом, если две формулы исчисления предикатов (не содержащие свободных индивидных переменных и формульных переменных без аргументов) равносильны в смысле опровержимости, то и соответствующие нм системы аксиом в разрешенном виде будут равносильными з отношении непротиворечивости. Поэтому каждая нормальная форма, приспособленная для исследования опровержимости формул исчисления предикатов, дает нам некоторую нормальную форму, приспособленную для исследования непроптиворечивости символьно разрешенных сиоп)ем аксиом, так что для каждой символьно разрешенной системы аксиом можно указать такую систему аксиом специального вида, которая эквивалентна исходной в отношении непротиворечивости.
Таким обрааом, нормальным формам 1 — 4, а также двум нормальным формам, приведенным после них, соответствуют (с учетом упомянутых выше дополнительных уточнений) следующие нормальные формы, приспособленные для исследования непротиворечивости символьно разрешенных систем аксиом: 1. Система аксиом с тремя различными индпвидными переменными, с одним двуместным и остальными одноместными функциональными знаками и четырьмя предикатными символами — тремя двуместными и одним одноместным. 2. Система аксиом с единственным (двуместным) функциональным знаком, единственным (двуместным) предикатным символом и тремя индивидными символами.
3. Система аксиом беэ индивидных символов, с единственным (двуместным) функциональным знаком и тремя предикатными символами — двумя двуместными и одним одноместным. 4. Система аксиом с единственным индивидным символом, единственным (одноместным) функциональным знаком и единственным (двуместным) предикатиым символом. (В нормальных формах 2 — 4 количество индивидных переменных не ограничивается.) 6. Система аксиом беа индивидных символов, с тремя различными нндивидными переменными, с единственным (двуместным» функциональным знаком и с одним двуместным и еще некоторыми одноместными предикатными символами.
6. Система аксиом без индивидных символов с двумя различными индивидными переменными, с единственным (одноместным) функциональным анаком и некоторым числом двуместных предикатных символов. Конечно, при исследовании непротиворечивости систем аксиом первой ступени наши критерии опровержимости могут быть е.символ и логичгскии ьормллизм )гл гн использованы и непосредственно. В частности, критерий 2" показывает, что для установления непротиворечивости какой-либо зл;анной в символьно разрешенном виде системы аксиом нерпой ступени вместо выполнения ее с помощью какой-либо финитной арифметической модели достаточно выполнения в некотором несобственном смысле; это выполнение состоит в том, что последовательно определяются расширяющиеся математические и логические функции, которые в подходящей конечной числовой области (до некоторого числа включительно) определены таким образом, что рассматриваемые аксиомы принимают значение «истина» на всех системах значений свободных индявидных переменных, при которых значения всех встречающихся в этих аксиомах термов также лежат в рассматриваемой числовой области, а при переходе от одной числовой области к другой, более широкой, области математические функции определякппся как продолжения, а логические могут быть изменены произвольно.
Если удастся убедиться, что этот процесс последовательно расширяющегося выполнения может быть продолжен неограниченно, то тем самым будет доказана непротиворечивость рассматриваемой системы. При этом непротиворечивость здесь следует понимать как невозможность вывести противоречие с помощью таких умозаключений, которые формализуются исчислением предикатов. С точки зрения теоретико-множественной логики предикатов такого рода непротиворечивость ввиду теоремы Геделя о полноте совпадает с выполнимостью рассматриваемой системы аксиом при помощи некоторой арифметической (разумеется, не обязательно финитиой) модели, а уже эта непротиворечивость, связанная с исчислением предикатов, гарантирует и непротиворечивость в неограниченном, содержательном смысле этого слова.
Для такого использования теоремы Геделя о полноте тоже имеется некоторый финитный эквивалент. Именно, можно показать, что всякая неопровержимая формула исчисления предикатов неопровержима и в рамках любого «арифметически непротиворечивого» формализма, т. е.
такого формализма, который, во-первых, непротиворечив и, во-вторых, остается непротиворечивым при добавлении арифметического формализма (если этот послед. ний еще не содержится в нем) и каких-нибудь других верифицируемых формул рекурсивной арифметики (также добавляемых в качестве аксиом). Но для того, чтобы получить этот результат, требуется некоторый шаг, который до сих пор еще не совершен, а именно нужна формализация рассуждений, проводимых в теории доказательств. К этому методу, который позволяет значительно продвинуться в различных направлениях„мы теперь и перейдем. ГЛАВА !17 У(ЕТОД АРИфМЕТИЗАЦИИ МЕТАМАТЕМАТИ К И В ПРИМЕНЕНИИ К ИСЧИСЛЕНИЮ ПРЕДИКАТОВ % 1. Арифметизация метаматематикя исчисления предикаточ и одна ее конкретная реализация а) Нумерации.
В предыдущих трех главах мы имели дело с методами, разработка которых была обусловлена введением гильбертовского в-символа. В частности, с помощью метода устранения связанных переменных нам удалось получить удовлетворительное решение проблемы символьного решения экзистенциальных аксиом; затем мы доказали одну весьма общую теорему («нп-теорему»), применяя которую, можно с помо!цью финитных арифметических моделей устанавливать непротиворечивость систем аксиом первой ступени, не пользуясь предположением о непротиворечивости формального анализа. Кроме того, этот метод позволил нам получить одно естественное доказательство теоремы Эрбрана, являющейся сильным математическим средством для изучения предикатов, а также для финитного рассмотрения различных проблем разрешимости. Однако в части, касающейся арифметического формализма, применение в-символа привело нас лишь к частичному результату, так как на этом пути удалось доказать ') непроворечивость только некоторой части системы (Х), а не всего этого формализма').
Теперь мы перейдем к рассмотрению еще одного метода теории доказательств, разработанного Куртом Геделем'), а именно метода арифметизации метаматематики. Что касается принципиальной стороны дела, то арифметизация метаматематики возможна в той же самой мере, в какой возможна арифметизация других теорий: арифметика достаточно богата для того, чтобы с ее помощью можно было строить модели различных метаматематических понятий и связей, существующих между ') См.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
