Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 45
Текст из файла (страница 45)
Действительно, если в процессе построения этой дизъюикции, состоящей из ! г членов, ЯИ и 6(!) являются теми двумя членами, один из которых совпадает с отрицанием другого, то уже дизъюнкция »Э! ')/ «Э! будет получаться подстановкой из некоторой тождественно истинной формулы исчисления высказываний. Формулировка и доказательство теоремы Эрбрана, приведенные выше, относятся к предваренным формулам. Но приведенный нами метод доказательства с использованием символьного решения и теоремы об элементарном выводе позволяет дать более общую формулировку этой теоремы, относящуюся ко всем таким формулам, у которых ни один квантор не стоит ни в области действия какого-либо знака отрицания, ни в каком-либо члене импликации или эквивалентности, или, выражаясь позитивно, относящуюся ко всем таким формулам, которые могут быть построены из пред- варенных формул с помощью конъюнкций, дизъюнкций и кван- торов.
Такого рода формулы мы будем для краткости называть к в аз ипредв а р енными. От любой формулы исчисления предикатов с помощью правил 2 и 4 исчисления высказываний') и правила (А) исчисления предикатов') можно перейти к квазипредваренной формуле. Если, пользуясь этими правилами, образовать отрицание какой-либо квазипредваренной формулы, то при этом получится новая квазипредваренная формула, у которой кванторы существования и всеобщности, а также и конъюнкции и дизъюнкции поменяются друг с другом местами, а отрицание 9 Этот разрешимый случай общей проблемы разрешимости отмечался уже Эрбрэном в его цитировавшейся выше днссертэцлн.
В своей рзботе «зпг 1е ргоыеше !опвзшеп1э! бе 1э 1о81Чпе шз18ешз1пчне» Эрбрзн добавляет зэмечзняе о том, что критерию выводнмостн для этого случая можно легко придать следующий внд; для любой заданной формулы рассматриваемого типа можно указать такое число 1, что эгэ формула будет выводима тогда н только тогда, когчэ онз будет 1-тождественнэ (см. цнт. соч., с. 34). Это утверждение, докэззтельствэ которого Эрбрэн не сообщил, ввиду его обманчивой прэвдоподобности было отмечено беэ всяких комменгэрнев в г, ! «Основзннй мэтемэтнкя» !с. 143 внизу (см. с. 188 — 188 русск. перевода)!. Нз го, что справедливость этого утверждения совершенно не очевидна, указал К. Шютте.
») См. г, 1, с. 79. Э) См. зз 1, с. 181. 1]з(а) =е,угой(а, и, го), введем функции зр(а, Ь) и зр(а), то из предыдущей формулы получим формулу 6 (а, Ь, р (а, Ь)) з/ ЧОЗ (а, зр(а), о), которая в свою очередь дедуктивно равна формуле 6 (а, Ь, гр (а, Ь)) 1/ З (а, ф (а), с). Эт фо уже не содержит связанных переменных, и из нее с помощью исчисления предикатов мы можем вновь получить фо 11. Те самым нами получено символьное решение фор- мулы 5. 1) См. кл. ! ° с Эб.
б дет перенесено на выражения, стоящие за кванторами, — совершенно аналогично тому, как это происходит при образовании отрицаний предваренных формул по правилу (А). Возможность распространения теоремы Эрбрана на квазипредваренные формулы вытекает из того обстоятельства, что процедура символьного решения способом, сходным со способом применения ее к предваренным формулам, может быть применена и к квазипредваренным формулам.
Поясним эту мысль иа примере, воспользовавшись методом формализации символьного решения с помощью е-символа' ). Пусть формула 5, которую мы будем рассматривать, имеет вид 'ех(зеуЗгЯ(х, у, г) з/:-(у!1'ЕЗ(х, у, г)). Эта формула дедуктивно равна формуле »ОуЗгр1(а, у, г) 1/ щизроЗ(а, и, о), а также (ввиду правила (ч)] формуле шгЯ(а, Ь, г) 1/ Зиз!/ОЖ(а, и, о).
С учетом эквивалентностей ЭЕЯ (а, Ь, г) 6 (а, Ь, е,6 (а, Ь, г)) и ЗиЭ/о»Э(а и о) чоЗ(а е чидз(а и го) о) эта формула может быть преобразована в формулу 6(а, Ь, е,6(а, Ь, г)) 1/ УОЗ(а, е,'ешЗ(а, и, го), о). Если мы теперь, пользуясь явными определениями 1р(а, Ь)=е,Я(а, Ь, г) а.СИМВОЛ я ЛОГИЧЕСдня ООРМАЛИЗМ пл, гм ТЕОРЕМА ЭРВРАИА А теперь, с учетом этого обобщения символьного решения, рассуждение, примененное иа с. 191 — 193к выводимой средствами исчисления преднкатов предваренной формуле Я, с равным успехом может быть применено и к выводимой квазипредваренной формуле гх.
В результате этого может быть построена такая дизъюнкция Фг'1/ ...')/ 6,, что: 1) она является формулой, истинной в логике высказываний, и 2) каждый ее член получается из формулы 6 в результате вычеркивания всех ее квантороа и выполнения следующих замен связанных переменных: каждая Б-переменная заменяется некоторым термом; любая Р-переменная, не попадающая в область действия ни одного квантора существования, заменяется некоторым сопоставленным ей индивидным символом; любая гй-переменная, попадающая в область действия каких-либо 1 кванторов существования, заменяется некоторым функциональным термом с сопоставленным этой чг-переменной 1-местным функциональным знаком, причем в качестве его аргументов стоят те же термы, которые появились на месте Л-переменных, связанных упомянутыми 1 кванторами существования. (При выборе порядка этих аргументов следует руководствоваться очередностью появления соответствующих кванторов существования.) При этом термы, появляющиеся на месте З-переменных, могут быть произвольным образом построены из фигурирующих в фом леКс б у гч вободных индивидных переменных, индивидных символов и функциональных знаков, а также из сопоставленных г(-переменным вновь вводимых инднвидных символов и функциональных знаков.
С другой стороны, если некоторая дизъюнкция 6г ')/ ... ')/ Ж об а л дающая перечисленными свойствами, истинна в логике выскаг '' ю зываний, то формула 6 выводима средствами исчисления предикатов. Действительно, вместе с этой дизъюнкцией истинна в логике высказываний и дизъюнкциЯ Фг ')('... ')( АР;, полУчающаЯсЯ из нее в результате замены каждого из иходящих в нее термов, начинающихся одним из сопоставленных некоторой )У-переменной функциональных знаков или состоящих просто из некоторого сопоставленного одной из а-переменных индивидного символа, какой-нибудь (вновь вводимой) свободной индивидной переменной.
А от этой дизъюнкции 6; ')/ ...')/ 6; можно средствами исчисления предикатов возвратиться к формуле 6. об Этот обратный переход может быть осуществлен специальны разом, а именно применением правил (ре) и (ч*), которые мы м сейчас сформулируем, и вычеркиванием повторяющихся членов дизъюнкции. Правила ()г*) и (Р*) являются обобщениями уже имеющихся у нас правил ()г) и (ч).
П р а в и л о ()га): Если формула составлена с помощью коньюнкций и дизьюнкций из некоторых составных частей (членов), то в любом из этих членов любой фигурирующий в нем терм можно заменить какой-либо связанной переменной, лростоеив перед этим членом соответствующий кеантор существования. Правило (чч): Если формула составлена с помощью коньюнкций и дизъюнкций из некоторых составных частей (членое) и если один из этик членов содержит какую-нибудь свободную индивидную переменную, не входящую ни е один из остальных членов, то эту свободную переменную можно зоменить связанной, простаеие перед этим членом сютеетстеующий кеантор всеобщности ').
К числу квазипредваренных формул относятся, в частности, дизъюнкцни предваренных формул. К рассмотрению таких дизьюнкций нас приводит исследование выводимости одних предваренных формул из других предвареииых формул (аксиом). Действительно, любая такая выводимость изображается импликацией вида г(гйг...бг 811 — «6, где й„..., 811 и 3 — предваренные формулы.
Эта импликация элементзрным преобразованием может быть переведена в формулу ) Лг '1/ ... ')/ ) 211')/ 6, а формулы )И„... )Яг по правилу (Х)') можно преобразовать в предваренные формулы, так что в результате получится дизъюнкция предваренных формул. Разумеется, в этом случае с помощью правила (г) з) можно все кванторы вынести наружу и, таким образом, получить одну-единственную предваренную формулу. Но этот прием в случае применения теоремы Эрбрана в форме предложения а) обладает тем недостатком, что вводимые при этом функциональные знаки получают аргументов больше, чем это необходимо.
Это обстоятельство связано с тем, что у дизъюнкции, построенной из пред- варенных формул, отчетливо проявляются некоторые характерные различия между формулами, а при сведении их в единую пред- варенную формулу эти различия оказываются замаскированными. Например, любая дизъюнкция вида ЛХ'1)Уг((Х, У) Ч ЗХЛУЗЗЗ(Х, У, г) может быть преобразована в предваренную формулу, имеющую вид Лх=)уЛЕЧиСз (х, у, г, и), но предваренная формула этого вида не всегда может быть расщеплена в дизъюнкцию указанного выше вида. Так и в вопросах, ') Пре применении правил ()гь) в (чь) следует учитывать, что, вообще говоря, одна н га же формула можег быть различными способами представлена а виде составных частей, соедааенпых знаками копьюнкцпп а дкзъюпкцаи.
а) См. т. 1, с. 181. а) См. т. 1, . 1УЗ. 21О е.СИМВОЛ И ЛОГИЧЕСКИИ фО~МАЛИЗМ 21! !гл гп зз! ТЕОРЕМА ЭРБРАНА связанных с проблемой разрешимости, мы часто бываем вынуждены для характеристики типов формул привлекать к рассмотрению дизъюнкции предваренных формул, если речь идет о выводимости, а если речь идет о двойственных вопросах непротиворечивости (неопровеижимости) илн о соответствующих неформальных вопросах «выполнимости», — конъюнкции предваренных формул. В качестве следствия из предложения б) н его обобщения получается, что осуществляемый средствами исчисления предикатов вывод любой квазнпредваренной формулы, построенной из переменных и символов исчисления предикатов и, быть может, некоторых дополнительных индивидных, функциональных и предикатных символов, всегда может быть проведен следующим образом. Мы начинаем с некоторой истинной в логике высказываний бескванторной формулы, которая не содержит никаких других символов логики высказываний, кроме встречающихся в заданной формуле, а затем подходящим гбразом применяем правила (ра) и (та) в сочетании с правилом вычеркивания повторений дизьюнктивных членов.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
