Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 39
Текст из файла (страница 39)
ИСЧИСЛЕНИЕ ПРЕДИКАТОВ [РЛ, 1У е) См. с. 162. ') Ск. с. 163. Однако в значительной мере произвольным является не только порядок кванторов; при преобрааованиях может также изменяться и их число. Например, во многих случаях число кванторов можно уменьшить применением правила (О). В рассмотренном примере это может быть сделано следующим образом. В формуле ЗхЗу ~А(х, у) ~/ УхЗу( ~В(х) ~/ С(х,у)) мы во втором члене дизъюнкцин переименовываем только пере- менную х; при этом получается ЗЕЗу 1А(х, у) )/ 'ты Зу( )В(и) )/ С(и, у)).
Применение правила (е) сначала приведет нас к формуле эи Зх (Зу )А (х, у) )/ Зу ( ~В(и) 1/ С (и, у))), которая пока еще не является предваренной. Теперь выражение, стоящее после чиЗх, мы можем преобразовать по правилам (О) и (т)). В итоге мы придем к формуле Уи Зх Зу ( ) А (х, у) ~/ ) В (и) ~/ С (и, у)), которая является предваренной и у которой квавторная приставка состоит только нз трех кванторов. Метод приведения провавольной формулы к предваренному ви- ду мы хотели бы применить еще и к упоминавшейся ранее г) фор- муле $, которая получается в результате конъюнктивного свя- аывания следующих трех формул: Чх 1Л(х,х), Чх т'у уг (Л (х, у) Ь Л (у, г) -+.
Л (х, г)), Чх Зу Л (х, у). Если здесь в третьем члене конъюнкции предварительно переиме- новать у в и, то получится )/х )Л(х, х) бе)/х Чу Чг(Л(х, у) АЛ(у, г)-~-Л(х, г)) Ь 'э'хЗиЛ(х, и). По правилу (О) перед этими тремя членами конъюнкции мы мо- жем поставить общий квантор всеобщности, так что получится )/х Р Л (х, х) бе Уу )уг (Л (х, у) Ь Л (у, г) — +- Л (х, г)) А Зи Л (х, и)).
Если мы теперь по правилу (г) преобразуем выражение, стоящее после квантора тх, то придем к предваренной формуле эх Уу 'Уг Зи () Л (х, х) й (Л (х, у) & Л (у, г) -+ Л (х, г)) А В (х, и)). $5) ИЗУЧЕНИЕ ФОРМАЛИЗМА ИСЧИСЛЕНИЯ ПРЕДИКАТОВ 165 Кроме того, выражение, стоящее после кванторов, можно, преобрааовав второй член конъюнкции (по правилу (т))), перевести в конъюнктивную нормальную форму; таким обрааом, мы получим э х э р ~г Зп ( ) Л (х, х) дс ( 1 Л (х, у) )/ ~ Л (у, г) ~/ Л(х, г)) Ь Л(х, и)). Способ, которым мы провели это последнее преобрааование, носит совершенно общий характер. В самом деле, правило (г)) в случае предваренной формулы позволяет нам в выражении, стоящем после кванторов, производить преобрааования исчисления высказываний; значит, в частности, мы можем преобразовать зто выражение в коныонктивную или дизъюнктивную нормальную форму.
Приведем, кроме того, реаультат преобразования в предваренную форму с конъювктивэой нормальной формой после кван- торов двя формулы ф, которую мы упоминали г) в связи с формулой 5; применив правила (О), (е) и (т)), мы получим здесь формулу 'э х Зу 'эх ( 1 А (х, х) А А (х, у) А ( ~ А (г, х) ~/ А (г, у))). Для таких предваренных формул с конъюнктивной или диэьюнктивной нормальной формой после кванторной приставки особенно просто может быть построено нх отрицание: нужно сначала заменить по правилу (А) каждый квантор всеобщности соответствующим квантором существования, каждый квантор существования — соответствующим квантором всеобщности, а затем взять отрицание выражения, стоящего после кванторной приставки.
Но отрицание конъюнктнвной или диаъюнктивкой нормальной формы по правилам исчисления выскааывавий заменимо выражением, которое получается взаимной заменой знаков 8~ и )/, а также элементарных формул и их отрицаний. При этом из конъюнктнвной нормальной формы получается днэъюнктивная, и наоборот.
Применяя этот способ образования отрицания, мы из формулы, в которую была переведена формула Я,немедленно получим следующее выражение для формулы 1 5: ЗхЗу Затеи(Л(х,х) ~/ (Л(х, у)бс ~Л(у, г) Ь 3 В(х, г)) ~/ ) Л(х, и)). Приведение формул к предваренному виду играет важную роль при рассмотренян проблемы раарешимоети. Так как зто преобразование может быть осуществлено для любой формулы исчисления предикатов, то проблему разрешимости достаточно будет решать в) изучение ФОРмАлизмА исчисле иия пРециклтон 137 [ГЛ, гч 186 исчисленнв пРециклтов только для предваренных формул. С помощью п р е д в а р е иной нормальной формы производитсятакжеивыявление тех случаев, для которых (помимо одноместного исчисления предикапгов) удается получить решение проблемы разрешимости.
В каждом иа этих случаев фигурирует, с одной стороны, совокупность тех предваренных формул, для которых с помощью соответствующей распознающей процедуры решается вопрос об общезначимости или же о выводимости (коротко: к л а с с с р а з р ешимой проблемой выводимости),а сдругойстороны, двойственная ей совокупность тех предваренных формул, для которых при помощи этой процедуры решается вопрос об опровержимости или же о выполнимости (коротко: к л а с с с р а зрешимой проблемой выполнимости). Вторая из этих совокупностей состоит из построенных по правилу (Х) отрицаний формул первой совокупности.
Специальные разрешимые случаи проблемы раарешимости, которые мы хотели бы адесь упомянуть, допускают классификацию по соответствующим классам (с одной стороны, относительно выводимости, а с другой стороны, относительно выполнимости). Классы с разрешимой проблемой выводнмости характеризуются следующими свойствами принадлежащих им формул: 1. Кванторы, входящие в приставку, суть либо только кван- торы всеобщности, либо только кванторы существования; либо же все кванторы всеобщности предшествуют всем кванторам существования.
2. Среди кванторов приставки имеется не более двух кванторов существования, причем в этом случае онн должны следовать непосредственно друг аа другом. 3. Выражение, идущее вслед за кванторами, либо имеет вид коньюнктнвной нормальной формы, состоящей только из одного члена, либо получается из такой формы в результате преобрааова-. ний исчисления высказываний. Из этих условий, определяющих классы с разрешимой проблемой выводимости, получатся условия для соответствующих классов с разрепгимой проблемой выполнимости, если в первых двух случаях поменнть местами кванторы всеобщности с нванторами существования, а в третьем случае вместо конюьпктивной нормальной формы говорить о дизыонктивной. Специальный характер этих частных случаев решения проблемы Разрешимости проявляется в том, что здесь проверку всякий раа можно осуществить с помощью подходящей конечной индивидной области.
Именно, во всех этих трех случаях для любой формулы из класса с раарешимой проблемой выводимости удается найти такое число 1, что эта формула выводима, если она у-тояФдественна, а для всякой формулы из класса с разрешимой проблемой выполнимости — такое число 1, чтл эта формула либо $-выполнима, либо опровернгима '). Поэтому тем более получается, что в трех рассмотренных случаях всякая формула из класса с разрешимой проблемой выводнмости, тождественная в конечном, является также и выводимой и что всякая формула иа класса с разрешимой проблемой выполнимости либо выполнима в конечном, либо опровержима.
В свете скааанного альтернатива между выполнимостью в конечном и опровержимостью имеет место, в частности (согласно второму случаю), для всякой такой предваренной формулы, у которой имеется не белее двух кванторов всеобщности, притом непосредственно следующих друг за другом. В случае, когда среди кван- торов, входящих в приставку, имеется более двух кванторов всеобщности или когда имеется два квантора всеобщности, разделенных квантором существования, упомянутая альтернатива не обязана выполняться. Зто покааывают примеры формул 'Гх ФУу)уг Зи( 1В(х, х) бг()В(х, у) 1/ !Л(у, г) )/ Л(х, г)) бг Л(х, и)) Ух Эу )Уг( !А (х, х) бг А (х, у) й ( )А(г, х) )/ А (г, у))), которые мы ранее получили путем преобразований нз формул гу и ф.
Действительно, с одной стороны, как мы уже установили в), формулы Я и ф не выполнимы в конечном, а с другой стороны, как мы покажем н гл. Ч1, онн не опровержимы, а потому и приведенные формулы, полученные преобразованием формул 5 и ф, не выполнимы в конечном и не опровержимы. Теперь, что касается решения упомянутых трех случаев проблемы иазрешимости, то первый из них может быть разрешен относителы о легко; мы будем говорить о нем в гл.
г'. Для второго случая проблема разрешимости была, независимо друг от друга, решена Геделем, Кальмаром и Шютте в). Все онн рассмотрели соот- ') Тем ве менее сы. т. 11 (укавапке 2 к оглввлвввю г. 11).— Прим. ко Р-.иу ивдаиию. в) Сы. с. 38, 162 и далее. в) Сы.,краткую заметку Геделя в Егх.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
