Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 56
Текст из файла (страница 56)
выполнены равенства и„„= а(г (и, Пг,з=ф(П«, 11=ф(П„1 1, =ф(пм и,), П„а> ф(п„г~,+1), ггеа)> '''' гаг-1='Ф( г' гг-а)> и аг-1)> 1,), ..., 1=ф(п„., 1«.), из которых следуют соотношения 1,=х,(пы ..., и ), ..., 1 (хб(пз, ..., и ), 1« ~1! 5 (и, ... Пг хз (Пз, ... Пг) ... х! (ПН Пг))' Но среди этих формул, как мы знаем, находится по крайней мере одна такая, которая в результате рассматриваемых замен принимает значение «ложые Таким образом, действительно, при любой замене формульных переменных логическими функциями, определенными для цифр, лежащих в пределах от 0 до ф(Ч, 1), по крайней мере одна из формул (8) оказывается ложной. Но функция ар всегда имеет значение, большее, чем ее аргументы, и всякое значение, которое она принимает, принимается ею только один раз.
Следовательно, функция ар образует разделяющую систему функций, и потому, согласно нашему критерию 3, формула ® опровержима в исчислении предикатов. Теперь предположим, что опровержима формула Ж Тогда, согласно критерию 1, начиная с некоторой цифры р, среди тех формул (8), вкоторых 1,, 1,, и,, ..., и,, „1,, ..., 1з изменяются в пределах от 0 до р, при любой замене формульных переменных формулы Й логическими функциями должна найтись по крайней мере одна ложная.
В частности, это справедливо н для всех тех замен, при которых вместо формульной переменной А (а, Ь, г) подставляется логическая функция, которая для любой тройки цифр а, Ь, г. принимает значение «истина» или «ложь» в зависимости от того, является или не является г (вычислимым) значением функции 'ф(а, Ь).
Я Д. Гнаьберг, П, Берееас формула Ф(пз, ..., п„, 1, ..., 1«) примет значение «истина», тем самым каждая из таких (р+1)г формул примет то же самое истинностное значение, что и соответствующая формула а-символ и логичгскип фопмализм 1гл пс 259 $51 ппичгигниг к ппоалемг. п«зпгшимости Если мы теперь возьмем для рассматриваемой цифры г какие- нибудь замены формульных переменных, входяших в выражение З(~», ..., па), т.
е. формульных переменных, входящих в формулу 11, какими-либо логическими функциями, определенными для цифр, лежащих в пределах от О до ф(Р, 1) [другие иифры не входят в формулы (8) в качестве аргументов), и объединим эти замены с только что упоминавшейся заменой для формульной переменной А(а, Ь, с), то в упомянутых формулах (8) все конъюнктивные члены А (1„1„ф (1„1,)) окажутся истинными, Поэтому значение «ложь» могут принять только те из этих формул, у которых ([)(и,, ..., и,„,, 1,, ..., 1«) принимает значение «истина», а 6(п......
и„, 1,, ..., 1„) — значение «ложь». Но если этот случай будет иметь место, то вследствие выбора логической функции, заменяющей формульную переменную А, цифры и,„..., и„,, 1,, ..., 1«(принадлежашие ряду от О до в) должны удовлетворять равенствам (9), в соответствии с которыми 1; при 1=1, ..., й является значением х;(и„, ..., и,), и потому при рассматриваемых цифрах и,, ..., и, формула 6(п,, ..., и,, х (и, ..., пс), ..., х (и, ..., и,)) должна принять значение «ложь». [При этом значения функций х; (и,, ..., и,) должны не превосходить 1.~ И так как это верно для произвольных замен формульных переменных формулы 5 логическими функциями, определенными для цифр, не превосходящих ф(1, р), то формулы 6(пс,), ..., и, р х,(пир ..., и„„), ..., х,(пь), ..., и, 1)) 1=О, ..., (р+»" — 1 не могут быть совместно выполнимыми.
[Получается, что совместно выполнимыми не являются даже те из этих формул, в которых все значениЯ фУнкций х,(пий ..., п„))... х,(п,,, ..., пс,) не превосходят р.) Поэтому из критерия 3 вытекает, что формула $ опровержима. Тем самым установлено, что формулы 5 и (Э равносильны относительно опровержимости их в исчислении предикатов. Но для всякой формулы 11 рассматриваемого специального вида соответствуюшую формулу Ф можно указать непосредственно, и эта формула имеет вид (1). Следовательно, для любой формулы (! рассматриваемого вида, а потому, вследствие сделанного ранее замечания, и для произвольной формулы исчисления предикатов, можно построить равносильную ей с точки зрения опровержимости формулу вида (1).
Таким образом, мы нашли финитное доказательство теоремы Пепиша в ее теоретико-доказательственной формулировке. Как мы убедились, для того чтобы придать этому доказательству фииитный характер, не требуется никаких новых соображений. Напротив, наши критерии опровержимости позволяют нам скопировать идеи теоретико-модельного рассуждения и ограничить при этом рассуждения, касающиеся логических функций, конечными индивидными областями. Конечно, перевод теоретико-медельных рассуждений в финитные теоретико-доказательственные не всегда бывает таким простым, как в только что рассмотренном случае,' иногда, вместо того чтобы пользоваться критериями опровержимости, оказывается более предпочтительным применять какие-нибудь прямые способы. Такого рода случай имеет место, например, с теоремой Левенгейма о равносильности (в отношении выполнимости) любой фо(»- мулы исчисления предикатов некоторой «бинарной» формуле, т.
е. формуле, все формульные переменные которой являются двуместными. Теоретико-доказательственным двойником этой теоремы является утверждение о том, что всякая формула исчисления предикатов в отношении выводимости равяосильна некоторой бинаоной формуле. Для доказательства этой теоремы можно, как это и сделал Эрбран, преобразовать с помощью критериев опровержимости доказательство теоремы Левенгейма в финитное доказательство соответствующей теоремы теории доказательств.
И тем не менее это доказательство, как показал Л. Кальмар'), можно получить заметно проще некоторым прямым способом. д) Теоретико-модельные нормальные формы. Мы изложим здесь некоторые новые важные результаты, которые касаются равносильности формул по отношению к выполнимости. Эти результаты также могут быть усилены до соответствующих фииитных утверждений, касаю!цихся равносильности формул по отношению к опровержимости. Чтобы иметь возможность кратко формулировать эти результаты, мы введем понятия теоретико-модельн ой н о р м а л ь но й фо р м ы.
Так мы будем называть некоторый специальный вид формул, если будет иметься соответствуюшая процедура, позволяющая преобразовывать формулы исчисления предикатов в формулы рассматриваемого специального вида, равносильные исходным формулам по выполнимости. Теоретико-модельными нормальными формами, в частности, являются: ') К а! ш а г 1.аа»1б. Оьег е!пеп 1.с!«епьоппас!~еп Ьа1». — Ас!а $«1.
Ма1Ь. Ьаекеп, 1934, 7, № 2. 9' Е-СИМВОЛ И ЛОГИЧЕСКИЙ ФОРМАЛИЗМ !ГЛ. РП и!'Именение к пРОБлеме РАЗРешимОсти !. Нормальная форма Геделя р((хл!ууЗи(А (х, у) Й В(у, и)) Й Чгхлчургггй((х, у, г) Й ргхЛО, ... Эпилхл(х, и,, ..., и„), использующая только двуместные формульные переменные'). 2. Нормальная форма Кгьрьмара ЧгхЧру=)гй(х, у, г)Й щи, ... 'ЗиюЧ(п, ... Уояб(ии ..., и„„п,, ..., в„), использующая только одну (двуместную) формульную переменную *).
3. Нормальная форма Непигиа Ч(хЧ(уЗЕА(х, у, г)Й ч!и ... Уияб(и, ..., и„). 4. Нормальная форма Аккермана') ЧлхЗуА (х, у) Й игл!Уи, ... лз ияЭ (г, и,, ..., и „), Все этн нормальные формы мыслятся как формулы бея еагь бпндых индиеидных переменных. 3 а м е ч а н н я. В нормальной форме Пепиша первыи член ЧгхЗуЛгА(х, у, г) может быть заменен членом Чрхлггу=)г (А (х, г) Й В (у, г)) з). ') См. О б б е! К. Яшп Еп1зсйе!бцпйзргоЫеш без 1оймсьеп Рцпы!опепйз! ° Лц!з. — Мопр(зЬ.
Мз1Ь. РЬуз., 1933, 40, № 2. Очень похожая георетякомодельная ворызльявя форма была указана Т. Сяолемоы в его работе: 5 Л о1еш ТЛ. Е!п 5з(з йЬег ЕаЛ!зцзбгйсйе.— Ас!в бс(. Мв1Л.5зейеб, 1936, 7,№4. Опв имеет следующий вяд: ЧгхчлуЭап (х, у, и) Й чхчгуВолз (х, у, и) Й 'лхлуучгз(4 (х, у, з) Йлрг. В ... В рй (., и, ..., в„) я тоже содержит только двуыествые форыудьяые перел, .Г«ые. доказательство Сколемз заодно дает и новое доказательство теоремы Левевгейыз и рпы что дюбзя формула исчисления предяхвтов равносильна по выполнимости иехоророй бинарной формуле. р) К в(ш з г !..
2цгцсыйЬгцпя без Еп1зсЬе№цпгзргоЫегпз зц( беп Рв!1 гоп Роппе1п лпц е1пег е!пх!геп, Ыпвгеп Рцпыюпзчзг!зЫеп.-Сорпрозй(в !пей., 1936, 4, № 1. р) А с Легше пи !Ал. Вецгзхе хип ЕБ1зсье!бцпйзргоЫерп бег прв!ЬешвнзсЬеп пой!Л. — Мзй. Апп., !936, 112, № 3. ° ! Пепиш заметил, что пря доявззтедьстве возможности построеявя его теоретико-модельной нормальной формы (№ 3 в нашем списке) отношение ф (а, Ь)=с «ожет быть представлено с помощью двух двумесгцых логических функций в виде Ч', (а, с) ЙЧ'р (Ь, с), где Ч',(а, с) ястццяо тогда в только тогда, когяз 2«является наибольшей вгепеяью числа 2, делящей с, з 'р„(Ь, с) истинно тогда я только тогда, когда 2Ь+ ! является язябольшяц нечетным чисдолл, делящим с.
Кроме того, как люказал Г1епнш, можно добиться, чтобы в этой нормальной форме кроме двуместных формульных переменных А н В встречалась только одна одноместная формульная переменная, Отсюда в свою очередь можно заключить, что в нормальной форме Кальмара в качестве ш можно взять число 3, так что в приставке второго члена этой конъюнкции будет стоять только три квантора существования '). В нормальных формах Геделя и Аккермана, как тоже было показано Пепншем'), можно обойтись тремя двуместными и одной одноместной формульнымн переменными. Кальмар показал, что в нормальной форме Лккермана, приведенной к предваренному виду, можно обойтись всего лишь одной-единственной бинарной формульной переменной з).
Из нормальных форм 1 — 4 после приведения фигурирующих там конъюнкций к предваренному виду получаются новые наглядные нормальные формы. В частности, из геделевской нормальной формы получается некоторая специальная сколемовская нормальная форма, содержащая трн квантора всеобщности, а из нормальной формы Пепиша — сколемовская нормальная форма с одним только квантором существования. Нормальная форма Кальмара переводима в предваренную формулу вида ши ...
Эи,цвхЧ(Ущглг(п, ... Р((оя6(и,, ..., из„х, У, г, и„..., о„) а нормальная форма Аккермана — в формулу вида щгЧ(хшуЧги, ... лггия(Ь (х, у, г, и,, ..., и„). Все упомянутые нормальные формы являются заодно н нормальнымн формами для исследования опровержимости формул в исчислении предикатов. Конечно, для того чтобы онн оказались таковыми в фннитном смысле, требуется фннитный перевод соответствующих теоретико-модельных доказательств. Путь для такого перевода указывают наши критерии опровержимостн 1 н 3, как это было продемонстрировано нами в случае нормальной формы Пепиша.
л) На зто обстоятельство указал А. Лиядецбрум в своем реферзте цитяровзвшейся выше статьи Кальмара. См. 2Ы. Мвй., !937, !3. ') Сы. упоминавшуюся яв с. 248 рзботу Пепяшв: Р е р (з 3. 1/п1егзцсвцпйеп йЬег бзз ЕпйсйепйщзргоЫеп! бег рпз1Ьегпз1!зсЬеп ! ойй, — Рцпбзлп, прзй.. 1938, 30. ') См. К з)гпзг 1.. Оп йе цебцс(!оп о! йе Пес!Моп РгоЫеш. Р!гз! Рврег. — Л 5ушЬоцс (длй!с, 1939, 4, р. 1 — 9. Позднее Л. Кальмар в Я.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
