Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 40
Текст из файла (страница 40)
шаФЬ. Ко!!ой., 1932, № 2, а также его работу: С о 6 е! К. 2иш ЕпгвсЬе!йппхвргоЫеш дев!ох!всйеп Еппйг!опепйа)!Ф61в.— МопагвЬ. МаФЬ. РЬув., 1933, 40, 8. 433 — 443; далее, работу: К а 1- га в г Ь. 1)Ьег й!е Егуй1!Ьвгйвк йег)еп!гвп ЕаЫвпвйгйсйе, ке1еЬе !с йвг Хогша)!огш гке1 ЬепасЬЬагФв А11ге!сЬеп егЬа1Феп.— МаФИ. Апп., 1933, 108, №г 3, в также работы: Б с Ь й Ф Ф в К.
1)пгегвпсЬппгвп гиш ЕпгвсЬе!6ппхвРгоЫеш йвг швФЬешаФМСЬвп 1ох!Ь.— МвФЬ. Апп., 1934, 109, 8. 572 — 603; 8 с Ь й Ф Ф е К. 1)Ьег 6!в Егр31)Ьаг1гв!Ф е!пег К!авве гоп 1ох!всЬеп копке!п.— МвФЬ. Апп., 1934, 110, 8. 161 — 194. Просгвйгзкй среди подпадвюшнх под и. 2 и пеохввтывавмых к. 1 случаев проблемы раврвшвмостк рвссмотревм в работы В е г и а у в Р., 8 с Ь 6 и 1 ! п Ь в 1 М.
Епш Епгвсйе!йппдвргоЫеш йвг ювгйешаФ!всЬеп ЬохЖ.— Марш Апп., 1928, 99, №г 3. Аккерман в Сколам, иввввксвио друг от друга, решили проблему выполнимости к усгаповклк 1гл. пс 1 ь! изучение ФОРИАлизмА исчисления ПРедикАТОЗ 189 188 ИСЧИСЛЕНИЕ ПРЕДИКАТОВ ветствующий класс с раарешимой проблемой выполнимости и нашли для формул этого класса условие, необходимое для их неопровернсимости. Для тех формул, которые удовлетворяют этому условию, Гедель и Кальмар доказали, что они выполнимы при помощи некоторой модели в финитной арифметике; Шютте доказал, кроме того, их выполнимость в некоторой конечной индивидной области (с числом индивидов, оцениваемым при помощи рассматриваемой формулы).
Разрешающую процедуру для третьего случая нашел Эрбран непосредственным применением своей уже упоминавшейся ') общей теоремы. 3. Разложение формул одноместного исчисления предикатов в примарные формулы; пример. Операции, с помощью которых ааданную формулу мы переводим в некоторую предваренную, могут быть выполнены и в обратном направлении; тогда мы придем к таким преобразованиям, при которых кванторы проносятся насколько можно дальше внутрь, т. е. приближаются по возможности вплотную к элементарным формулам. Какой-нибудь просто характериауемой нормальной формы таким путем мы, конечно, не получим.
Это можно будет сделать только в случае одноместного исчисления предикатов. Здесь, пронося кванторы внутрь, мы в конце концов приходим к таким формулам, которые получаются применением связок исчисления высказываний к члримарнььы формулам», т. е. к таким формулам, которые либо являются элементарными, либо имеют один из следующих двух видов: сИх (с41с (х) !/... '!()91(х)), 3х(фс (х) &...бс))41(х)), где )(! с (а), ..., )(11(а) означают либо элементарные формулы с аргументом а, либо отрицания таких элементарных формул. (Число членов 1 от случая к случаю может меняться.) Тот факт, что каждая формула одноместного исчисления предикатов может быть переведена в такую формулу, состоящую из примарных формул, или, как мы будем для краткости говорить, может быть разложена в примарные формулы, а хьтервативу, имеющую место между опровержнмостью и выполнимостью э конечном, для тех предваренных формул, у которы~ среди кваягоро» прставки имеется только один квантер всеобщности.
Сы. А с Ь е г пс а и а %. ()Ьег с(!е Нг%1!Ьаг1се!с зечс!»»ег 2аЫ»ц»с(гйс1се.— ЫасЬ. Авп., !928, 100, )ссйй 4 — 5; 8 Ь о1е пс Т. СЬег с(!е швсЬеша!!»сЬе 1,оз!)с.— Хошй ша!. ТЫ»»1сг., 1928, 10. ') Сы. с. 169. был сделан Г. Беманом отправной точкой его исследования, посвященного одноместному исчислению нредикатов; об этом исследовании впоследствии мы будем говорить более подробно '). В воаможности разложения всякой формулы одноместного исчисления предикатов в примарные формулы можно убедиться следующим образом. Представим себе, что рассматриваемая нами формула преобразована в предваренную, и рассмотрим последний (самый правый) квантор приставки. Проводя, если потребуется, соответствующее переименование переменных, мы можем добиться того, чтобы свяаанная переменная была переменной х.
Тогда рассматриваемый квантор будет представлять собой с(х или Зи. В первом случае мы преобразуем выраясение, следугощее за )((х, в конъюнктивную нормальную форму, и затем по правилам (О), (с) н (г))») этот квантор всеобщности может быть разнесен по всем членам конъюнкции с учетом наличия в них переменной х; при этом члены конъюнкции, не содержащие х, окажутся без этого квантора всеобщности. Каждый из коныонктивных членов, перед которым стоит квантор !7 х, в свою очередь является простой дизъюнкцией, члены которой суть либо элементарные формулы, либо отрицания элеыентарных формул, либо получаются из формул такого типа заменой свободных переменных связанными. Теперь те члены днзыонкции, которые не содержат х, по правилам (с) и (с)) можно вынести за квантор всеобщности.
В реаультате получается, что выражения, перед которыми стоит квантор с~х, будут иметь вид )(1с (х) )('... ')/ср1(х)! таким образом, переменная х будет фигурировать только в примарных формулах. Так как кроме переменной х зти формулы никаких переменных балыке не содержат, то при дальнейших преобраразованиях с ними можно будет обращаться как с нерасчленимым целым, чем-то вроде элементарной формулы без аргументов. Совершенно аналогичного эффекта мы можем достичь и в случае квантора существования лх. Мы только должны будем вместо конъюнктнвной нормальной формы взять дизъюнктивную.
Коли разложение в примарные формулы на этом шаге еще не закончились, то во всяком случае уменьшилось на единицу количество кванторов, стоящих перед формулой. Тогда описанную ') См. с. 250 и далее. В своей работе (В е Ь ш а э п Н. Ве1сгаяе хш А!8»Ьга с)ег 1оя!!с, !а»Ье»оас(еге хшп Вас»СЬе!йаэдаргоЫ»ш.— МасЬ. Авн., 1922, 88, № »8 3 — 4!. Веыав, впрочем, ае поль»овался выражением «пряыаряая ФОРмула»; в сзя»и с рассматриваемым методом оя говорит о »внесении операторов (к»авторов)» (см.
11 9 — 10 цитируемого сочинения). ») Сы. с. 177 и далев. (Г11. 1У ИСЧИСЛЕНИЕ ПРЕДИКАТОВ процедуру мы можем повторить для того квантора, который теперь окажется на последнем месте. Если фигурирующая в пем переменная отлична от у, то она мон1ет быть переименована в у. Полученные к этому времени примарные формулы при этом никаких иаменений не претерпят, потому что, как мы уже заметили, с ними можно обращаться как с элементарными форму нами без аргументов Теперь появятся новые примарные формулы вида 'Фу(Ф (д) 1/ "ЧФ~(у)) Зу($ (у) 8 8 Ф~(у)). или Теперь разнесем квантор всеобщности ух по членам конъюнкции, принимая при этом во внимание, что переменную х содержат лишь первый и третий члены.
У нас получится выражение Эу(Ух( 1В(у) ~/ С' ~/ А(х)) 81( ) С ~/ 1 В(у)) 81 Ух(1С 1/ 1А(х) ~/В(х))). Теперь, вынося в дизъюнкциях с предшествующим вх из-под кван- тора всеобщности члены, не зависящие от х, мы получим Зу (( ~В (у) 1/ с 1/ 1ух А (х)) 81 ( 1 С ~/ 1 В (у)) й (~ С ~/ 1з1х ( 1А (х) ~/ В (х)))). В этих формулах переменная у может быть переименована в х.
Теперь либо мы уже у цели, либо количество кванторов в приставке снова уменьшилось на единицу, а в прочих отношениях структура формулы осталась прежней — рааве лишь добавились новые примарные формулы. Таким образом можно продолжать до тех пор, пока в приставке вообще не останется ни одного квантора, Тогда результирующая формула будет состоять из одних только примарных.
Описанный способ, вообще говоря, упрощается благодаря тому, что при преобразованиях по правилам исчисления высказываний те составные части формул, которые уже оказались раалоя енными в примарные формулы, мы можем оставлять без иаменений. В качестве примера на применение нашего метода мы разложим в примарные формулы формулу ЭХ 'Фу ((В (Х) 81 1 С-+. А (у)) 81 (С вЂ” +- 1 В (Х) 81 (А (у) — + В (у)))). Переименуем сначала х и у в у и х и приведем выражение, идущее аа Лу ух, к кокъюнктивной нормальной форме. У нас получится Буях(( 1В(у) ~/ С ~/ А(х)) 81( 1С ~/ 1В(у)) 81 ( 1 С ~/ 1А (х) ~/ В(х))). $ Й ДЕДУКТИВНОЕ РАВенСТВо и дедукцноннхя р АЯ ТЕОРЕМА 1Я Вв ыражении, стоящем после Лу, последний член 1С ~/ Ух( 1А (х) ~/ В(х)), которыи уже разложен в примарные формулы, мы можем оставить беэ изменений. Выражение (~В (у) ~/ С ~/ ~/хА (х)) 81 ( 1 С ~/ '1 В (у)) мы можем сначала преобразовать в ~ В(у) ~/ ((С ~/ ЧхА (х)) 81 1С), а это последнее опять привести к дизъюнктивной нормальной форме 1 В (у) ~/ (Ух А (х) & 1 С).
Так мы приходим к формуле Лу(( 1В(у) ~/ (Ух А(х)81 ~ С)) А( ~ С ~/ Чх( 1А(х) ~/ В(х)))). Теперь мы можем [по правилу (1)! вынести из-под квантора суще- ствования Лу сначала не содержащий у конъюнктивный член ~ С ~/ Ух( 1А (х) ~/ В(х)), а затем и не содержащий у дизъюпктивный член ~гхА(х) е 1 С, так что у нас получится (ЛУ В (У) ~/ (ух А (х) 81 1 С)) 81 ( 1 С 1/Мх (-~А (х) 1/ В (х))) Т~~ер~ у мо1ет б Тем самым мы рааложили исходную формулу в прнмар е.
Применяя правила исчисления высказываний и пользуясь формулой (2) исчисления предикатов, мы можем преобразовать иолученное рааложение в следующую более обоаримую формулу: (УхВ(х)г-'ФхА(х)) 8:(С-~Эх 1В(х) 81 Ух(А(х) — «В(х))). б Дедуктивное равенство и дедукционная теорема 1. Понятие дедуктивного равенства; два существенных случая Обе дедуктивного равенства; переводимость и дедуктивное равенство.
рассмотренные нами нормальные формы, предвареняая нормальная форма и разложение в примарные формулы (последняя введена специально для одноместного исчисления предикатов), Уже дали нам определенное представление о формализме ис числения тов. Еще более полное представление нам дадут некоторые теоремы общего характера, к изложению которых мы сейчас пе ейдем. Тео емы р эти связаны с понятием дедуктивного равенства.
"ч пере- 1гл. гч исчислиннк пгедннлтов Мы будем говорить, что формула Я д е д у к т и в но р авиа фо муле В, если Я выводима нз В, а В выводима кз Я по правилам исчисления предикатов. На первый взгляд кажется, что это понятие по существу совпадает с понятием переводимости. Тем не менее требование переводимости Я в З, т. е. выводнмости зквивалентности Я З, является более сильным, чем требование дедунтивного равенства Я и В.
Дедуктивное равенство вытекает из переводимости; действительно, с помощью формулы Я В З может быть выведено из Я, а Я вЂ” из В. Однако обратное У твержденне места не имеет: переводимость иа дедуктивного равенства не вытекает. Поясним зто на следующих двух типичных примерах: 1. Формула А (А как отдельно взятая формульная переменная) дедуктивно равна формуле ~ А. Действительно, 1 А получается нз А путем подстановки; с другой стороны, иа ~ А мы можем подстановкой получить ) ) А, а затем, воспользовавшись тождественной формулой 1 3А-+.А, получить и А. Однако переводимость А в 1 А места не имеет; действитольно, если бы формула А 1А была выводима в исчислении предикатов, то в нем была бы выводима вообще любая формула, что, как мы видели, места не имеет.