Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 61
Текст из файла (страница 61)
Я суть конъюнкции, построенные из равенств и неравенств а также > е их отрицаний. 2. Эатем мы исключим вс ечаю е нив кажд аждыи конъюнктивный член тр щиеся в нем отрицания заме> а<Ь \/ Ь< а, ~ (а<Ь) посредством а ьаждыи член посредством а=Ь Ч Ь< а. ри этан замене структура нашей дизъюнктивной но мальн " ее, пользуясь дистрнбутивн ван Таким образом, вместо выражения Я (хл мы пол м ктивную нормальн ф .ь ую форму х) мы получим такую дизъюн- ~ЛУ ' У')а в которой й), ... В б вен ств. В, будут конъюнкциями равенс тв и нева- 3. В .
В тех равенствах и неравенствах, кото ые пе содержат в обеих част х, которые переменную х тях, мы заменим х пос едством 0 говоря, всякое встречающе с е я нам равенство р и, иначе х(1) х(1) мы заменим равенством а всякое неравенство неравенством 0(1) = 0(1), х(" < х(1) О(" < 0(1).
ем самым мы добьемся того, что в каждом авенст неравенстве переменная х б ет р енстве и в каждом ая х удет встречаться самое большее в одной обозначать то выражение которое п уча вания на него ( т . П ое пол ется штрихов. Посредством а»в мы из а путем навешисамо выражение а.
ы будем обозначать Теперь мы выполним над выражением Я(х) я и е б л. Сперва мы преоб х рядпрео разований. нормальную форму рео разуем его в как ю-ли у -либо диаъюнктнвную <гл. Рг нАчАЦА Агиеметикн 292 з з) ПРОЦЕдуРА Редуктгии 293 из его частей; если равенство буде~ содержать х в правой части, мы поменяем его части местами. 4. Пусть | — наибольшее число штрихов, навешенных на переменную х в получившейся таким образом формуле. В каждом равенстве и неравенстве, в котором х стоит с меньшим числом штрихов (это число Г может оказаться равным и нулю), мы к обоим выражениям, стоящим слева и справа от символа = или (, добавим < — г штрихов.
В результате мы добьемся того, что во всех элементарных формулах, содержащих х, переменная х будет снабжена одним и тем же числом 1 штрихов. Наконец, дизъюнктивные члены этой дизъюнктивной нормальной формы мы расположим в такой последовательности, чтобы члены, не содержащие х, стояли последними. После выполнения операций 4 — 4 вместо Я (х) получится выражение, обладающее следующими свойствами. Оно представляет собой дизъюнктивную нормальную форму, построенную из равенств и неравенств, каждое из которых (если оно содержит х) имеет один из следующих трех видов: х(~)~а, х(")(а, а(х(~), где < всюду одно и то же (оно может быть равно и нулю), а а не содержит переменной х; диаъюнктивные члены с х стоят впереди.
Таким образом, наша дивъюнкция имеет вид причем переменная х входит только в те члены, где это указано специально. Мы заменим теперь выражение Лх Я(х) дизъюнкцией ~хб,(х(~)) )<' ... ')(' ~хб (х()) )<' Ж~~, ')(' ... ')(' 6„. Для каждого члена Зх(Ь,(х()) (г=(, ..., ш) имеются две возможности: либо в 6 (х(г)) входит какое-нибудь равенство х(о=а, либо х(1) встречается в нем только в неравенствах.
В первом случае Лхб (х(г)) имеет вид Эх (х(г) = а & 6", (х(0)) (причем допускается и такой случай, когда х(1) в 5*,(х(г)) вовсе не входит) или же просто вид Вх (х( ) = а). Каждый член вида Зх (х(0 = а & 6* (х(~))) мы заменим не зависящим от х выражением (00) = а ')/ 0(0 ( а) & 6' (а), а член Эх (х(г) = а) мы заменим выражением 0(") = а (/ 0(~)(а. Во втором случае мы сначала вынесем из-под квантора существования члены конъюнкции, не содержащие х(0 .
Тогда под квантором существования останется конъюнкция Й (х(0) неравенств вида а ( х') или х< ' ( а. Таким образом, общий вид конъюнкг (г ции к (х(0) будет таков: а~(х(0& ... & а<«х(г) & х(г)(Ь, & ... &х(0(Ь . Мы заменим теперь Зхк(х(Г)) не содержащей х конъюнкцией 0(0(Ь, & ... &0(1)(Ь &а,'(Ь,& ... &а,'(Ь, & &а~(Ь & ... &а<(ЬЮ < Если и (х')) не содержит членов вида а ( х(г), то надо будет взять одну только конъюнкцию О<')' =Ь,& ...
&О(')(Ь,; если не будет членов вида х(0 ( Ь, то Лхй (хо)) надо будет заменить равенством 0=0. Применив эту процедуру замены ко всем выражениям Ь Ь„( (0), мы получим вместо первоначальной составной части Зхл (х) рассматриваемой нами формулы пекоторое выражение, не содержащее переменной х, которое содержит только такие связанные пере- нАчАлА АРиюмвтики )гл. уг 295 ПРОЦЕДУРА РЕДУКЦИИ менные, которые связываются квакторами существования, содержащими в своей области действия это выражение.
Если в полученном выражении будут встречаться не все те отличные от х свободные и связанные перелгенпые, которые входили в Я (х), то для каждой такой недостающей переменной — например для а или для у,— мы добавим к этому выражению в качестве конъюнктивного члена соответствующее равенство а = а или у = у так, чтобы получающееся выражение содержало в точности те же самые переменные, что и Я (х), ва исключением переменной х. Если в рассматриваемую нами формулу вместо ее составной части Зх Я(х) мы подставим это вырахгение, то количество кванторов существо- ванин у формулы уменьшится на единицу. Эту процедуру мы теперь можем применить еще раз к одной из аналогичных внутренних составных частей Эхк) (х).
Продолжая таким образом и далее, мы по очереди удалим все квапторы существования и придем к формуле, которая вообще не будет содержать связанных переменных. При этом в ней будут встречаться те же самые свободные переменные, что и в первоначальной формуле. Любую из полученных таким образом формул мы будем называть редукцией нашей исходной формулы, а саму процедуру ее получения мы будем называть о п е р а ц и е й р е д у к ц и и. 2.
Верифицируемые формулы; теорема об однозначности; леммы. С помощью этого понятия мы придем к желаемому обобщению определения и с т и н н о й формулы, которое, как мы помним, было сформулировано только для нумерических формул. Это обобщение мы получим в результате введения понятия верифицируемой формулы, которое мы — предварительно ограничиваясь рассмотрением формул без кванторов всеобщности — определим следующим образом: 1. Нумерическую формулу мы будем называть верифицируемой, если она является истинной.
2, Формулу с одной или несколькими свободными индивидными переменными (но без других переменных) мы будем называть верифицируемой, если она истинна при любой замене этих переменных цифрами '). 3. Формулу со связанными переменными, но без формулькых переменных и кванторов всеобщности мы будем называть верифицируемой, если применение процедуры редукции переводит ее в верифицируемую формулу (в смысле, определенном в пп. 1 и 2). Последнвй пункт этого определения, относящийся к формулам со связанными переменными, чуждается в специальном обосно- ') Такую замену можно рассматривать и как подстановку. Здесь и далее в этой главе мы будем пользоваться выражвкивм з а м е к а с учетом будущих обобщений понятия ее риф и пир уз кос г и, в связи с которыми каы придется иметь дело с заменой свободиых переменных такими выражвкиими, которые ив относятся к вашему дедуктивному формализму.
ванин, поскольку процедура редукции определена не вполне однозначно. Действительно, некоторый произвол имеет место уже при построении дизъюнктивной нормальной формы. Для того чтобы наше определение верифицируемости для формул со связанными переменными получило однозначный смысл, необходимо, чтобы этот произвол в процедуре редукции не оказывал влияния на верифицируемость результата. Это мы действительно можем доказать, опираясь на следующую, несколько более сильную теорему: Если Я и йэ суть редукции одной и тойже формулы 5, то при любой замене входящих в них свободных переменных цифрами эти формулы либо обе окажутся истинными, либо обе будутя ложными ').
Из этой теоремы об однозначности немедленно вытекает, что если Я и )Π— редукции одной и той же формулы и Я верифицируема, то верифицируема и З. Такии обрааом, все дело теперь сводится к тому, чтобы доказать эту теорему об однозначности з). Теорема эта верна в тг)м случае, когда формула 5, редукции которой мы рассматриваем, не содерлзат связанных переменных, так как в этом случае единственной редукцией $ является сама эта формула.
Далее, заметим, по если наша теорема будет иметь место для формул $„..., з) то она будет справедлива и для любой их комбинации, эп у построенной с помощью связок исчисления высказываний, так как редукция б строится из редукций формул гы..., $ в тем же самым способом, которым 5 строится из 5ю..., 5г Действительно, операция редукции, как мы внаем, сводится к последовательному, идущему изнутри наружу исключению кван- торов существования; при атом очередность прилгенения связок исчисления высказываний, ке попадающих в область действия кванторов существования, не подвергается никаким изменениям.
Теперь уясним себе следующий факт. Редуцирование любой формулы Зх 6 (х) производится таким образом, что сначала в ней устраняются наиболее глубоко расположенные кванторы существования. При этой процедуре с переменной х мы обращаемся так, как если бы она была свободной переменной. Поэтому, если Я (х) обозначает выражение, в которое 6 (х) перецдет в результате исключения стоящих внутри него кванторов существования, и если мы подставим вместо х какую-нибудь свободную переменную, не встречающуюся в 6 (х) (а значит, и в )К (х)), например с, то Ж (с) будет представлять собой редукцию б) (с), а всякая редукция формулы лх)й (х), полученная в результате дальнейшего ') Заметим, что 9) содержит тв же свободные первквикые, что и Е.
з) Соображения, которыми мы для этого воспользуемся, одновременно послужаг и вспоыогательвык средством для установления кепротиворечивости рассматриваемой нами системы аксиом. ПРОГШДУРА РКДУКЦИИ [гл. Рг НАЧАЛА АРИФМВГИКИ 297 296 развертывания процедуры редукции, будет редукц ей формулы ЗхЯ (х). Таким образолы если переменная с не входит в 6 (х), то любая редукция формулы Зхб (х) одновременно будет редукцией и всякой такой формулы ЗхЯ (х), у которой Я (с) яеллетсл редукцией Ю (с).