Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 53
Текст из файла (страница 53)
Формульные переменные с одной свободной переменной в качестве аргумента. 3. Равенства между свободными переменными. 4. Формулы вида 'УхЖ (х) и Эхй (х), где як (х) обоаыачает диэъюнкцию, а Й (х) — коыъюнкцию, члены которой суть формульные переменные с аргументом х или отрица- ния таких формул, причем каждая встречающаяся формульная переменная встречается только в одном иэ членов. 5. Формулы вида !»гихл (х) и Эмхй» (х), где выражения Й (х) и Й (х) имеют структуру, укааанную в и. 4. 6. Количественные формулы, т. е.
формулы вида ')(хму(х=у) и Эхму (х~= у), Кроме того, получеыную нами формулу, построенную иэ составных частей типов 1 — 6, мы можем, пользуясь правилами исчисления высказываний, перевести в формулу, являющуюся конъюнктнвыой нормальной формой относительно этих составных частей. До спх пор все преобраэования были преобрааованиями в смысле псрсводимости. Теперь мы будем стремиться к тому, чтобы постепенно, шаг за шагом, исключить всс формульныс переменные с аргументом. Для достижения атой цели мы будем пользоваться преобразованиями в смысле дедуктивного равснства. Мы будем при атом использовать тот факт, что конъюнкция при замене ее членов дедуктивно равными формулами переходит в дедуктивно равную ей конъюнкцию.
В атом можно убедиться следующим обрааом. Пусть формулы )йп дедуктивно равны формулам ~п Тогда пэ формулы к(к~ дк к(п !) См. с. 226. РЕШЕНИЕ ПРОБЛЕМЫ РАЗРЕПГИМОСТИ 121 252 исчисление пРедиклтОБ с Рлвенством 1гл ч 293 ив которой, как мы знаем, выводимы формулы ЙО ° ° в Оа~ могут быть также выведены и формулы ~„.... 2)„, а тем самым и формула а,б ...аа„; кроме того, из последней формулы в точности тем же способом может быть выведена формула ~ 1 ~ ' ' ' б'Ма Из этого замечания вытекает, что в полученной нами конъюнк- тивной нормальной форме каждый конъюпктнвный член может рассматриваться сам по себе.
Каждый такой член имеет вид дизъюнкцин, члены которой суть формулы типов 1 — 6 или же отрицания таких формул. Здесь прежде всего можно перевести отрицания формул типов 4 и 5 в формулы тех же самых типов, но уже не являющиеся отрицанинми других формул. В самом деле, отрицания формул вида Чхй(х), Зхк(х), тих% (х), З хй(х), как мы знаем, переводимы в формулы вида Зхй (х), )7хй (х), Зиха (х), Мих'Й (х) Теперь представим себе, что встречающиеся формульные переменные с аргументом расположены с целью их исключения в определенном порядке.
Пусть  — первая в этой последовательности переменная с аргументом. В качестве именной формы для нее возьмем В (г). Переменная В может встречаться только в составных частях типов 2, 4 и 5. В случае, когда В (г) содержится в составных частях вида 7хЖ (х) или )ущх%) (х), вынесем фигурирующие в начале этих формул кванторы всеобщности по правилу (~) ') (после выполнения соответствующих переименований, которые, возможно, при этом потребуются) в начало всей нашей дизъюнкции и затем заменим связываемые ими переменные свободными. К содержащим формульную переменную В (г) составным частям Зиха (х) 1) См.
с. 179. мы применим эквивалентности 9Ь)) '), согласно которым всякая формула Зщхй(х) (а=2, 3, ...) переводима в формулу 7х чу ... 7РЗй (и~ФхА... Ли~и м Й(ю)), где число кванторов всеобщности тх,..., Ри на единицу меньше ш. Кванторы всеобщности, стоящие в начале такой формулы, после выполнения соответствующих переименований, если они окажутся необходимыми, мы снова люжем, пользуясь правилом (~) з), вынести в начало всей нашей дизъюнкции, а затем заменить связываемые ими переменные свободными. Кроме того, переименуем связываемую квантором существования переменную юв х.
Так вместо составной части Зщхй (х) мы получим формулу вида Зх (хчьай... А х~г м Й(х)) (в которой, конечно„вместо а,..., г могут стоять и какие-нибудь другие свободные переменные). После выполнения всех этих операций формульная переменная В (г) будет встречаться только в таких дизъюнктивных членах, которые либо являются формулами типа 2, либо отрицаниями таких формул, либо имеют один из видов ЗхВ(х), Зх (В (х) %6), Зх $В(х), Зх) )В(х) бс б), Ю где щ — выражение, не содержащее формульной переменной В (з).
Теперь все такие члены нашей диаъюнкцнн мы можем перевести в члены вида Зх(В(х) йщ) или Зх( )В(х) Аб). Действительно, для формул типа 2 и их отрицаний мы в своем распоряжении имеем эквивалентности В(а) Зх (х=айВ(х)), ~В(и) Зх(х=ай ЪВ(х)), которые с помощью подстановки получаются из формулы 6Ь)) з); а формулы ЗхВ(х) и Зх-) В(х) 1) См. с. 219. з) См. с. 179. з) См. с. 214.
254 ИСЧИСЛЕНИЕ ПРЕДИКАТОВ С РАВЕНСТВОМ (гл. У могут быть переведены в формулы Зх(В(х)&х=х) и Зх(-) В(х) Ах =х). После того как эти преобразования будут выполнены, вся наша дизъюнкция (после подходящей перестановки членов) приобретет вид Я )/Зх(В(х) &6')2'(х)))/ ... )/ Зх(В(х)А 61" (х)) Ч Зх (-ч В (х) А 6'!ю (х)) )/ . Ч Зх () В (х) А 6!" (х)) где выражения Я, 61" (х), ..., 6)1" (х), 6)ю (х), ..., 612' (х) уже не содержат формульной переменной В(в).
Эту формулу можно сначала перевести по правилу (8) ') в Я )/ Зх!((В(х) А 6)" (х)) ))/ ... )/ (В(х) А 61" (х)) ))/ (~ В (х) А 6)ю (х)) )/ ... (7 В (х) А 6(ю (х))), а затем с использованием закона днстрибутивности и правила (ч) 2) — в формулу Я )/ Зх((В(х) А(6')2'(х) ))/ ... ~/ 61" (х))) ~/ (.Ч В(х)А(6))з)(х) )/ ...
)/ 6(ю(х)))), т.е, в формулу вида Я )/ Зх((В(х) &6оо(х)) )/ (~ В(х) &6'2'(х))), где снова выран<ения Я, 6'О(х) и 6'2'(х) ке содержат формульной переменной В(в) 2). Эта формула дедуятпвно равна формуле Я ~/ Зх (6'2) (х) А 6'О (х)). Действительно, если в предыдущей формуле вместо переменной В (2) подставить формулу 6оэ (в), то получится Я '„/ Зх ((6'2' (х) А (Ун) (х)) )/ (-) 6)2) (х) А 6)2) (х))); а так как дизъюнктивпь)й член 6(2) (х) А 6)2' (х) ') См. с. 178.
2) См. с. 177. з) В том случае, когда одно вз чисел 1, ! равно нулю, немедленно получается (с помов)ью соотвотствующзй подстановки вмзсто В (з)), что этв формула дедуктивно равна формуле ))(. 1 2) РЕШЕНИЕ ПРОБЛЕМЫ РАЗРЕШИМОСТИ может быть опущен, то отсюда получается и только что упомянутая формула Я )/ Зх(6'2'(х) &-6'О(х)); с другой стороны, исходя нз этой формулы и применяя тождественную формулу С А Р -). (А А Р) ~/ ( )А А С),Я из которой в результате подстановки получается 62'(а) А 6ОВ (а) — )-(В(а)А 6оэ(а)) )/ (-7 В(а) & 62'(а)) '), мы с использованием правила (б),2) и тождественной формулы (С -+ Р) — (А ))/ С вЂ” А ')/ Р) возвращаемся к формуле Я г/ Зх((В(х) А 6П) (х)) )/ (-7 В(х) А6'" (х))). Дедуктивное равенство доказано. Теперь исключение формульной переменной В (в) завершается переходом к формуле Я Ч Зх(6(2)(х)А(У)п(х)).
Правда, относительно полученной формулы мы не можем утверждать, что она составлена из примарных; но разложение в примарные формулы можно будет произвести дополнительно и получившуюся таким образом формулу мы затем сможем преобразовать в копъюнктивную нормальную форму, конъюнктивные члены которой снова можно будет рассматривать по отдельности. Существенно, что при этой процедуре новых формульных переменных с аргументом не появляется, так что в целом количество подлежащих исключению форыульных переменных с аргументом уменьшается. Продолжая таким образом и далее, мы в конце концов добьемся того, что все формульные переменные с аргументом будут полностью исключены.
Когда этот процесс будет закончен, мы, во-первых, соберем вместе все те конъюнктивные члены, на которые шаг за шагом была расщеплена наша исходная формула; действительно, при исключении очередной формульной переменной с аргументом происходит дальнейшее расщепление на конъюнктивные члены и для каждого члена исключение должно проводиться в отдельности. ') Если взремзвяая а входит в ба' (а) влп в Ю'з' (х), то вместо а в указанной формулз нужно будвт взять какую-нибудь другую свободную впдпвидную переменную. з) См. с. 146. 257 Решение НРОБлемы РАЗРешимости вю ИСЧИСЛЕНИЕ ПРЕДИКАТОВ С РАВЕНСТВОМ [гл ч 255 Далее, мы заменим все встречающиеся свободные индивидные переменные связанными. Затем мы применим процедуру разложения в примарные формулы.
Так как теперь уже больше не будет свободных индивидных переменных и формульных переменных с аргументом, то составные части, из которых (после произведенного разложения в примарные формулы) оказывается построенной паша формула, могут быть только формулами типов 1 и 6, т. е. только формульными переменными без аргументов и количественными формулами. Мы снова придадим этой формуле вид конъюнктивной нормальной формы.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
