Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 48
Текст из файла (страница 48)
В зависимости от того, какой из кванторов, »!х или Зх, предшествует рассматриваемому выражению, мы преобразуем его либо в конъюкктивную, либо в дизъюнктивную нормальную форму, а затем по правилу (6) ») распределим квантор всеобщности Ух, соответственно квантор существования лх, на все члены конъюнкции, соответственно дизъюнкции, в отдельности. Тогда после каждого квантора всеобщности ч!х (т. е. в области его действия) будет стоять некоторая дизъюнкция (соответственн о осле каждого квантора существования 3х будет стоять некоторая конъюнкция) и по правилу (!) г) каждый не зависящий от х член диэъюнкции или конъюнкции мы сможем вынести из-под рассматриваемого квантора Зх, соответственно 3х. В результате вся формула в целом приобретет следующий вид.
Перед формулой будут стоять кванторы всеобщности и существования, связывающие переменные У,г,...,и; ') См. с. 177. ) См. с. 178. ) См. с. 170. !5с 228 исчисление пРедикАтОВ с РАВенстВОм игл у РАСШИРСННЫИ ФОРМАЛИЗМ 229 за ними будет идти выражение, которое образовано с помощью связок исчисления высказываний из составных частей следующего типа: 1) формульиые переменные без аргументов (т. е. формулы типа 1); 2) формульные переменные с отличной от х переменной в качестве аргумента; 3) равенства между двумя отличными от х переменными; 4) выражения вида » х (ф> (х) )/ ...
'>/ ф» (х)) илн Зх(ф, (х) &... &$1(х)), где каждый нз членов Н(х)* " ' Ф1(х) представляет собой либо равенство, содержащее переменную х, либо отрицание такого равенства, либо формульную переменную с аргументом х, либо отрицание формулы такого типа. В том случае, когда кроме х никаких связанные переменных болыпе не имеется, результирующая формула оказывается построенной с помощью связок исчисления высказываний из составных частей типов 1) — 4), причем никаких кванторов всеобщности или существования перед нею больше не будет. Теперь займемся преобразованием формул типа 4). Прежде ' всего, мы можем исключить члены вида х=х или х~х1 применяя формулы (все они могут быть выведены с помощью формулы (У>)). Далее, мы можем добиться того, чтобы в каждом равенстве, содержащем переменную х, или в отрицании такого равенства переменная зта зх(х=х) »х(х Ф х) Зх(х=х) Лх (х ~ х) ~Гх(х=х ~/ А(х)) >ух (х ~ х ~/ А (х)) Лх (х = х1& А (х)) Зх(х~х&А(х)) А>/ 1А, ° А& 1А, А>/ 1А, А& )А, А)/ 1А, ч'х А (х), Зх А (х), А& )А стояла в левой части; этого можно достичь, применив формулу 2)): а = Ь -+.
Ь = а. Наконец, мы можем добиться того, чтобы в составных частях Чх(($>(хи " Ч Ф$(х)) ни один из членов дизъюнкции не был отрицанием равенства н чтобы в составных частях Зх(>О,(х) &... &)))1(х)) ни один из чле>к ь конъюнкции не был равенством. Действительно, пусть, например, в »х(>(>,(х) >/ ... )/ >()~(х)) член >р, (х) представляет собой отрицание равенства х = с. Тогда зто выражение, которое имеет внд » х (х —.Д с ~/ Я (х)), можно сначала преобразовать в Ух (х = с -~ Я (х ) ), а затем, с применением формулы ба)), в Я (с), т.
е. в выражение, построенное с помощью связок исчисления высказывангй из составных частей типа 2) и 3). В такого же рода выражение с помощью формулы 6Ь)) г) может быть преобразовано и выражение Зх (>р> (х) & ... & ф~ (х)), в котором один нэ членов конъюнкции представляет собой равен- ство типа х = с.
Правда, процедуру эту нельзя будет применить, если дизъюнк- ция '4>>1(х) ~/ ... )/ ф~(х) (соответственно конъюнкция !(>, (х) &... & $1(х)) окажется одночленной. Но в этом случае мы можем испольэовать эквивалентности '>/х(х~а) А& >А, Лх(х=а) А ~/ > А, которые могут быть выведены из формулы (Х>). >) См. с. 214. РАСШИРЕННЫЙ ФОРМАЛИЗМ переменные, отличные от у,з,...,и, у,з,...,и ') См. с. 222 я далее. 230 ИСЧИСЛЕНИЕ ПРЕДИКАТОВ С РАВЕНСТВОМ игл у Теперь из составных частей типа 4) остаются только такие, которые — если отвлечься от переименования переменных и, может быть, от замены свободных переменных связанными — имеют один из слцдующих шести видов: 7х'(х=а ~/ х=5 ')/ ... ')/ х=г), Зх(х~а&х~Ь&... & х~г), 7х Ж (х), Зх Я (х), ~х(х=а ~/ х=Ь \/ ... ~/ х=г ~/ З(х)), Зх(х~а&х=Ь&...
&х~г& й(х)), где Ж (х) обозначает дизыонкцию, а м (х) — конъюнкцию, у кото- рой каждый член представляет собой либо формульную перемен- ную с аргумептом х, либо отрицание формулы этого типа. Среди выражений этих шести видов выражения Чхй (х) и Зхй (х) представляют собой то, что в доказываемой нами теореме мы назвали формулами типа 4. А формулы остальных типов, применяя 10а)) и 10Ь)) '), можно перевести в такие выражения, которые с помощью связок исчисления высказываний могут быть построены из составных частей типов 2) и 3) и из формул типов 5 и 6. Таким образом, результирующее выражение, стоящее за кван- торной приставкой, относящейся к переменным теперь состоит из составных частей типов 1, 4, 5, 6, 2) и 3).
В том случае, когда перед формулой больше нет ни одного квантора всеобщности или существования, составные части типов 2) и 3) могут содеряеать только свободные индивидные переменные; следовательно, они являются формулами типов 2 и 3. В этом случае вся формула в целом оказывается составленной иэ формул типов 1, 2, 3, 4, 5, 6 с помощью связок исчисления высказываний, и тем самым мы достигаем поставленной цели.
Если же связанные переменные и относящиеся к ним кванторы приставки все еще будут иметься, то предыдущую процедуру можно будет повторить. Правда, ситуация по сравнению с исходной теперь изменится вследствие того, что в области действия кванторов, входящих в приставку, появились составные части типов 4, 5 и 6, содержащие связанные но это обстоятельство не меняет ничего существенного в протекании нашего процесса.
Действительно, так как составные части типов 4, 5 и 6 не содержат ни одной из переменных у, з,..., и, то мы можем обращаться с ними в точности так же, как с формульными переменными без аргумента, т. е. выражение, стоящее после кванторпой приставки, сначала можно будет перевести в конъюнктивную, соответственно дизъюнктивную нормальную форму, причем все составные части типов 4, 5 и 6 можно будет рассматривать как нерасчленимое целое (подобно элементарным формулам). Если мы теперь применим — как мы это делали раньше — к последнему из кванторов, входящих в приставку, правила (О) и (е), то составные части типов 4, 5 и 6 выйдут на области действия этого квантора.
Получившуюся теперь формулу можно охарактеризовать аналогично формуле, полученной нами на соответствующем месте первого шага нашей процедуры. Единственное различие заключается в том, что при перечислении возможностей 1), 2), 3), 4) мы к составным частям категории 1) должны будем, кроме формульяых переменных беа аргументов, причислить еще и формулы типов 4, 5 и 6. Дальнейшее течение процедуры, где речь идет только о преобразовании формул типа 4), будет таким же, как и в предыдущем случае. После этого мы либо достигнем поставленной цели (если все кванторы, стоящие перед формулой будут исчерпаны, т. е. если все связанные переменные будут вовлечены в составные части типов 4, 5 и 6), либо смолеем применить нашу процедуру еще раз.
При каждом применении этой процедуры количество кванторов, стоящих перед формулой, будет уменыпаться на единицу. Таним образом, если число кванторов у исходной предваренной нормальной формы равно к, то и-кратное применение нашей процедуры приведет нас к формуле, обладающей заданным свойством, т. е.
к такой формуле, которая образована из составных частей типов 1, 2, 3, 4, 5 и 6 с помощью связок исчисления высказываний. Тем самым исходная формула окажется разложенной в примарные формулы. Заметим также, что рассмотренный способ разложения в примарные формулы не приводит к появлению каких-либо новых свободных индивидных переменных, Таким образом, если исходная формула с самого начала не содеряеала свободных индивидных переменных, то и после проиаведенного разложения в примарные формулы в результирующей формуле их также не будет.
Тем самым не смогут появиться никакие составные части типов 2 и 3, так что все примарные формулы обязательно будут формчлами типов 1, 4, 5 и 6. РАСШИРЕННЫЙ ФОРМАЛИЗМ 232 ') См. гл. 1, е. 31. е) См. рассуждения яе с. 35 и далее. ') См. гл. Гг', с. 160 — 1И. 1) См. гл. 1У, с. 165. исчисление пРедикАтов с РАвенством [ГЛ. Ч Укажем также на то, что при разложении в нримарные формулы можно заранее позаботиться о том, чтобы з составных частях видов 73 Ь (х), 7мхй (х), йх й (х), Змхй (х) дизъюнкция Ж (х), соответственно конъюнкция Й (х), содержала каждую входящую в нее формульную переменную только один раа. Действительно, повторяющиеся члены любой дизъюнкции или конъюнкции могут быть опушены. Может также случиться, что одна и та же формульная переменная входит в какую-нибудь дизъюнкцию или конъюнкцию в качестве члена один раз с отрицанием и один раз без него.
Но тогда можно будет применить следующие эквивалентности: )/х(А(х) )/ )А(х)) А ~/ )А, 11х(А(х) )/ е)А(х) )/ В(х)) А )/ ~А, Эх(А(х) б< )А(х)) АА )А, Эх(А(х)<я )А(х)<яВ(х)) Аб< )А. 4. Обобщение понятия 1-тождественной формулы; дедуктивная замкнутость совокупности 1-тои<дественных формул; однозначность равенства. Теперь, после того как в результате проведенных нами формальных рассмотрений мы познакомнлнсь с методикой использования аксиом (1,) и (1,), мы снова вернемся к вопросу о непротиворечивости. Нам нужно показать, что в результате добавления к исчислению предикатов анака равенства и связанных с ним аксиом равенства не возникает никакого противоречия, т.
е. что при этом никакие две формулы Я и ) Я не оказываются выводимыми одновременно. Это доказательство мы сможем провести уже применявшимся в гл. 1У способом "), распространив понятие 1- т о ж д е с т в е ни о й формулы исчисления предикатов и на формулы со знаком равенства. Формулу такого рода мы назовем 1-тождественной (1 здесь означает произвольное, отличное от нуля конечное число), если она, будучи проинтерпретирована в 1-элементной индивидной области, принимает значение «истина» при любой подстановке логических функций ') вместо формульных переменных и индивидов вместо входящих в нее свободных индивидных переменных (при этом каждому фигурирующему в роли элементарной формулы равенству в соответствии с его содержательным значением мы придаем значение «истина» или «ложь» в зависимости от того, совпадает 6 с 1 или же нет). Кроме того, понятию 1- т о ж д е с т в е н н о й формулы мы сопоставим двойственное ему понятие 1-вы пол пимой формулы.
Формула рассматриваемого нами формализма будет называться 1-выполнимой, если она, будучи нроинтерпретирована в $- элементной индивидной области, принимает значение «истина» при подходящей подстановке логических функций вместо формульпых переменных и индивидов вместо свободных индивидных переменных и при условии, что входящим в нее равенствам мы приписываем истинностные значения, соответствующие их содержательному смыслу. Если отвлечься от того обстоятельства, что здесь в рассмотрение вовлекаются свободные индивидные переменные, то определения этих понятий совпадут с приводившимися в гл. 1 определениями общезначимости и выполнимости для $-элементной инпивидной области ').