Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 54
Текст из файла (страница 54)
Теперь мы можем исключить здесь и формульные переменные без аргумента. Действительно, во-первых, мы можем опустить повторяющиеся дизъюнктивные члены. Далее, если в каком- нибудь члене коньюнктивной нормальной формы формульная переменная встречается в качестве дизъюнктивного члена вместе со своим отрицанием, то по правилам исчисления высказываний весь этот член конъюнкции может быть опущен.
Если гто будет иметь место в каждом конъюнктнвном члене этой нормальной формы, то вся формула в целом будет выводимой. Тогда ее можно будет перевести и в такую формулу, которая состоит нз одних количественных формул, например, в формулу дахау(х=-у) В/ -1 дахау(х=у). Теперь осталось рассмотреть только такой случай, когда каясдая иа встречающихся в формуле формульных переменных фигурирует внутри каждого члена конъюнкции не более одного раза (с отрицанием или без него).
В этом случае исключение формульных переменных снова будет происходить таким образом, что будет преобразовываться (в смысле дедуктивного равенства) наждый в отдельности член этой конъюнкции. Пусть, например, С вЂ” переменная, которая должна быть исключена первой. Содержащий эту переменную член конъюнкции будет иметь (может быть, после перестановки диаъюнктивных членов) один из двух видов Я~/С, Я'и' ~С, где переменная С в Я не входит. Но формула Я в/ С дедуктивно равна Я.
Действительно, Я получается из Я в/ С подстановкой вместо С формулы С дс 7 С, которая может быть опущена в качестве члена дизъюнкции; фор. мулу Я в„( С тоже можно получить из Я по правилам исчисления выскааываний. Равным образом, формула Я ~ 7 С дедуктивно равна Я, так как, подставляя С ~/ 7 С вместо С и применяя правило отрицания, мы вместо 7 С получим дизъюнктивный член С А. 7 С, который опять-таки может быть опущен.
Таким образом, можно одну за другой исключить все формульпые переменные, и тогда мы придем к формуле, которая будет иметь вид конъюнктивной нормальной формы, построенной из количественных формул, и которая будет дедуктивно равна нашей первоначальной формуле. Тем самым доказана провозглашенная нами теорема о том, что всякая формула расширенного одноместного исчисления предикатов дедуктивно равна некоторой формуле, построенной иг едких только количественных формул; при атом доказательство, в полном соответствии с финитнои точкой зрения, протекает таким образом, что одновременно оно дает и способ, позволяющий для любой ааданной формулы расширенного одноместного исчисления предикатов построить дедуктивно равную ей формулу, состоящую из количественных формул.
Укааанный способ применим не только в принципе, но и окавывается приспособленным для практического использования, причем, конечно, отдельные его детали вщгут быть упрощены и далее. 4. Теоремы о полноте для расширенного одноместного исчисления предикатов. С помощью доказанной теоремы мы теперь без труда получим доказательство сформулированных выше теорем о полноте, а также и решение проблемы разрешимости для расширенного одноввестного исчисления предикатов '). Мы сначала покажем, что всякая тождественная в конечном формула расширенного одноместного исчисления предикатов всегда будет выводимой.
В самом деле, пусть Я вЂ” тождественная в конечном формула этого исчисления. Укаэанным методом мы построим формулу к), дедуктивно равную формуле Я и составленную из количественных формул. Зта формула, согласно доказанному ранее, также должна быть тождественной в конечном. Мы можем считать, что в1) имеет вид конъюнктнвной нормальной формы, и тогда каждый ее конъюнктивный член в отдельности также должен быть тождественным в конечном.
Каждый такой член имеет вид дизъюнкции количественных формул Ухиу (х= у), Зхиу (х ~ у) и их отрицаний, Сначала, пользуясь эквивалентностью -7 Чх,йУ(х=У) ЗхмУ(х~ У), здесь можно будет устранить отрицания. Далее мы сможем перевести эти диаъюнкции в дизъюнкции, состоящие самое большее из двух членов; действительно, из выводимых формул Чхиу(х=у) -в- Ухи,у(х=у) в) См. с. 250.
77 Л. Гнньеерт, и, БеРнайс 1гл. ч 259 Решение пРОБлемы РАВРешимости исчисление пРедикАТОВ с РАВенстВОм ахи у(х~у) -в- Зхиу(хну) для любых двух чисел ш и н таких, что ш)н, могут быть получены эквивалентности 7(хну(х= у) — чхиу(х= у) Ч 77хву (х= у) либо формула либо формула Зх7У (х Ф У) 77х у(х=у) 1/ Лх1У(х~у); при атом $ и 1 будут по меньшей мере равны 2.
Эта формула — как результат преобрааования конъюнктивного члена формулы ю — должна быть тождественной в конечном. Но легко убедиться, что формула '57х1 У (х у) не является Г-тождественной, а формула Лх1У (х ~ У) не является (1 — 1)-тождественной. Таким образом, следует принимать во внимание лишь случай формулы Чх7У (х =ч У) ~/ 3х1У (х ЧЬ У). Для того чтобы эта формула была тождественной в конечном, она должна быть, в частности, 1-тождественной.
Но, как легко б ) 1. видеть, это имеет место только тогда, когда б Таким образом, это условие должно выполняться. Но в этом случае выводииость рассматриваеиой нами формулы немедленно вытекает из выводимости следующих двух формул: )1х1У (х * у) 'Ч Эх1у (х ~ у), Лх1У (х ЧЬ У) ~ Зх1У (х ~ У). Зх'„у(х~у) Эхщу(х~у) 1/ Лх„у(х-ьу), а с помощью этих эквивалентностей мы можем шаг эа шагом уменьша меньшать количество дизъюнктивных членов вида 7х1у (х = у) и Зх1У(х~у) до т р, ех пор пока членов каждого из этих типов станет не больше одного. Тогда получится либо формула Чх7У (х = У), Отсюда следует, что каждый конъюнктивный член конъюнктивной нормальной формы д) является выводимой формулой, а значит, и сама З также будет выводимой.
Но 7О и Я дедуктивно равны, и, значит, Я также является выводимой формулой, что и требоВалось доказать. Метод, которым иы провели только что рассмотренное докааательство, заодно дает нам и способ, позволяющий распознавать выводнмость любой формулы расширенного одноместного исчисления предикатов. В самом деле, исходя из произвольной формулы этого исчисления и применяя наш общий метод (алгоритм), мы сначала получим для исходной формулы дедуктивно равную ей конъюнктивную нормальную форму, построенную из количественных формул. В атой нормальной форме мы затем сможеипровестн упрощения, которые только что были выполнены в применении к формуле е). Так мы получим некоторую формулу Я, представляющую собой конъюнкцию членов следующих трех видов: 'зх1у(х= у), Зх1У(х~ у), ~х1у(х=у) 1/ Зх1у(хчьу). По этой формуле Я можно будет немедленно выяснить, при каких условиях наша исходная формула является тождественной в конечном, а значит, и выводимой.
Условия эти заключаются в том, что в формуле 6 должны встречаться копъюнктивные члены только третьего вида, и притом только такие, у которых чнсло1 не превосходит числа 1. Проблема разрешимости здесь может быть решена даже в некотором расширенном смысле, а именно, как задача о тои, можно ли для любой конкретной формулы выяснить, при каких конечных (отличных от нуля) числах ш эта формула является ш-тождественной и при каких — ш-выполнимой. Обе эти двойственные по отношению друг к другу задачи сводятся одна к другой, так как всякая формула Ш-выполнпиа тогда и только тогда, когда ее отрицание не является ш-тождественным.
Несколько более отчетливый характер рассмотрение носит в случае вопроса о выполнимости. Пусть Я вЂ” рассматриваемая нами формула. Для ее отрицания 1Я мы вюжеи построить дедуктивно равную, построенную из количественных формул конъюнктивную нормальную форму вээ„ у которой каждый ее член имеет один из трех видов '77х1У(х =у), Зх1у(хчьу), ) 'Ух1У( =У) Члх1У( ~у) 1 Эта формула 6* ш-общезначима тогда и только тогда, когда шобщезначима формула 1Я. Соответственно, формула Я ш-выполнима тогда и только тогда, когда ш-вьшолнимо отрицание 771 ггсчисггнгпги гггкднклтов с елвннствоьг [гл. ч 260 ГЛАВА 1 формулы (Уе.
Это отрицание ма>нет быть преобразовано в дизь- юнкцию З, построенную из членов следующих видов: Лх1У(х и:У), Чх)У(х=У), ~е '1(1,1>1). Зх)У (х ~ У) А- У" х)У (х = У) Для того чтобы дизъюнкция З была ш-выполнимой, необходимо и достаточно, чтобы ш-выполнимым был каждый из ее членов. Итак, необходимое и достаточное условие ш-выполнимости для члена Зх)у(х~ у) состоит в том, что 1(ш, для члена Чх)у(х= у) состоит н том, что ш(1, ДЛЯ ЧЛЕНа ЛХ)У (Х =и'-. У) Сс 'ЧХ)У (Х = У) СОСтОИт В тОМ, Чта 1~(ш (1; при этом условие ш (1 понимается нами как 1~(ш (1. Обратим внимание также на следующее обстоятельство: если формула Я не является ш-выполнимой ни длн какого числа ш, то )Я тождественна в конечном и, следовательно, выводима; значит, в этом случае формула Я является опровержимой.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
