Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 43
Текст из файла (страница 43)
Вслед за этим мы ~водим символ сс и формула Я(а) берется в качестве новой исход- 1) См. с. 1?З. 7~ !Гл, сч ИСЧИСЛЕНИЕ НРЕДИКАТОВ 202 1 61 дедуктиВное РАВенстВО и дедукциОннАя теОРемА 203 Вой формулы. Затем с использованием формулы Я (сс) выводится некоторая формула В, в которой символ и не встречается и относительно которой мы без ограничения общности можем считать, что она не содержит никаких свободных индивидных переменных.
Мы теперь покажем, что формула В может быть выведена и прямо из формулы Зх Я(х). Действительно, из вывода В с помощью формулы Я (а), согласно дедукционной теореме, мы получаем (так как Я (а) не содержит никаких свободных переменных) вывод формулы Я (а)-+В, который осуществляется средствами исчисления предикатов без использования формулы Я (а).
В атом выводе, не нарушая его дедуктивной структуры, вместо символа а можно всюду подставить какую-нибудь ранее не встречающуюся свободную индивндную переменную (например, с), и тогда мы получим вывод формулы Я (с) — ~й. Так как переменная а в ней не встречается (Я (а) и В по предположению не содержат свободных инднвидных переменных), то, подставив а вместо с, мы получим формулу Я (а)-с-й, а нз нее по схеме (р) получим Зх Я (х) -Р В.
Итак, эта последняя формула выводима в исчислении преднкатов и, значит, в сочетании с формулой ЗхЯ (х) она дает нам формулу В. Возникает вопрос о том, нельзя ли распространить проведенное здесь рассуждение и на тот случай, когда нам дается теорема существования вида «для произвольных а, Ь, ..., й существует 1 такое, что Я (а, Ь,..., )с, 1)» и когда вводится специальный символ уже не для индивида, а для функции. Действительно„ такое распространение может быть осуществлено, но приводить доказательство этого факта нам сейчас не хотелось бы; позднее оно будет получено нз одной весьма общей теоремы ').
4. Дедуктивное равенство произвольной формулы подходящей еколемовской нормальной форме, а также нормальной диэъюикции; упрощение этого перехода. Теперь мы перейдем к другой общей теореме исчисления предикатов, касающейся предваренной нормальной формы. Как мы уже знаем, каждая формула исчисления предикатов может бьжь переведена в некоторусо предваренную форму. Здесь имеется в виду преобразование типа переводимости. ') См.
Указ«низ 3 после оглаелення т. 11. Если же мы будем интересоваться лишь дедуктивным равенством, то можно будет дополнительно предъявить особые требования к порядку следования предваряющих формулу кванторов всеобщности и существования. К этому кругу вопросов относится одна теорема, которую мы хотели бы назвать теоремой Сколелса, поскольку она получается из одного доказанного Сколемом в связи с проблемой распознавания выполнимости формул утвержденна '), если перейти от вопроса о выполнимости формул к вопросу о их выводимости. Зта теорема утверждает, что всякая формула исчисления предикатов дедуктивно равна такой пред- варенной нормальной форме, у которой все кванторы существования предшествуют всем кванторам всеобщности («сколемовская нормальная формаз). Мы проведем доказательство таким образом, чтобы заодно получить и некоторый более сильный результат.
Именно, мы покажем, что Всякая формула исчисления предикатов дедуктивно равна некоторой диаъюнкции, членами которой являются такие предваренные формулы, в кванторной приставке которых имеется не более одного квантора всеобщности, и в случае, когда такойкван- тОР ИМЕЕТСЯ, ОН ЯВЛЯЕТСЯ ПОСЛЕДссИМ КзаптОРОМ ПРИСтаВКИ. Иа этого утверждения теорема Сколема может быть получена совсем просто. Действительно, дизъюнкция, члены которой суть предваренные формулы с нужным нам свойством (такие формулы мы будем называть «нормальными дизъюнкциямиз), всегда переводима в сколемовскую нормальную форму.
Пусть, например, у нас имеется нормальная дизъюнкция Зх Зу 7з Я (х, у, з) с/ Зу Зи В (у, и) )/ Зз сУх )б (х, з), где Я (х, у, з), В (у, и) и 6 (х, з) кванторов не содержат; тогда с помощью переименований переменных мы можем сначала перевести ее в формулу Зх Зу Чз Я (х, у, з) с/ Зх Зу В (х, и) )/ Зх )си 6 (и, х), ') См. уже уиомннззшуюон работу: 8 Ь о 1 е ис Т. Ьоу!«СЬ-ЬошрйиасоссзсЬе ПисегзисЬшзеи...— Угйеиз)с.
Бйс!1сег, 1 Мас.-изс. К1., 1920, № 4. В втой работе Сколеы показал, что с точки зрения еыиолннмостн любая формула исчисления предзкатоз равнозначна такой предзаренной формуле, у которой зсз кзанторы всеобщности иредшзстзуют всем кзанторам существозання. Это рассуждение поззолязт пронззестн переход от проблемы выполнимости к проблеме зызоднмостн, причем з окончательном результате кззнторы всеобщности н существования меняются ролями. Это позволяет созершнть переход к сформулированной з тексте теореме н к ез доказательстзу.
Уклон з сторону теории доказательств можно найти ужз з работе Рйлеля: С о й е 1 К. Ьце той«санс)!3Ь«!с с)ег Ах!ошз с)ез 1оп!зсЬеп Риийс!оиеийзПсй1з.— Мона««Ь. МАСЬ. РЬуз., 1930, 37, № 2, теорема 1У. Доказательство иерзоначзльной теоремы Скол«ма о выполнимости читатель может найти е т. 11 (указание 4 после оглавления т. И). Дня срззненнн можно рекомендовать иознакомнтьсн с ннм уже сейчас. ! 6] дгдуктиВное РАВенстВО и двдукционнАЯ теОРемА го5 [ГЛ. 1У ИСЧИСЛЕНИЕ ПРЕДИКАТОВ а эту формулу, применяя правила (О) и (1), можно будет перевести в Зх Зу 1Уг тУи (Я (х, у, г) ~/ (8 (х, у) ~/ Ж (и, х)), что и даст нам' искомую сколемовскую нормальную формулу.
Иаложенный на этом примере метод применим и в общем случае. 11оэтому для доказательства теоремы Сколема достаточно будет показать, что всякая формула исчисления предикатов дедуктивно равна некоторой нормальной диэъюнкции. Мы рассмотрим это доказательство на примере, причем можно считать, что рассматри- ваемая формула с самого начала дана в предваренной нормальной форме. Пусть она имеет вид ((1)) 7х 3у Чг Зи Я (х, р, г, и), и при этом Я (х, р, г, и) уже не содержит кванторов всеобщности и существования.
Для этой формулы мы следующим обраэом пост- роим некоторую дедуктивно равную ей формулу. Возьмем три не встречающиеся в данной формуле формульные переменные — В с тремя аргументами, С с двумя аргументами и Р с одним аргу- ментом — и будем исходить из формул Чх 7у 7г (А (х, у, г) — » В (х, у, г)) — » (Э1х Зу7г А (х, р, г) — »Чх ЗуМгВ(х, у, г)) Чх ~у (А (х, р) -» С (х, у)) — » (Мх Зу А (х, у) — » 7х Зу С (х, р)), выводимость которых мы установили на с. 201, а также из формулы (11) ') 'Фх (А (х) — 1- В (х)) -» (!Ух А (х) — » 7х В (х)).
Подставив в первой формуле ЗиЯ (а, Ь, с, и) вместо именной формы А (а, Ь, с), во второй !1гВ (а, Ь, г) вместо А (а, Ь) и в тре- тьей ЗуС (а, у) вместо А (а) и Р (а) вместо В (а), мы получим сле- дующие три формулы: ух Чу эг (Зи Я (х, у, г, н) — » В (х, у, г)) — » (э1х Зу 7г Зи Я (х, у, г, и) — » Ьх Зу Чг В (х, у, г)), 'ФхЧу(э1гВ(х, у, г)-»С(х, у)) — »(!1хЗуЧгВ(х,у, г) — МхЗуС(х,у)), ух(ЗуС(х, у)-»Р(х))-»фхЗрС(х, у) — » ухР(х)).
Если теперь мы присоединим к ним нашу формулу 'ух Зу Чг Зи Я (х, у, г, и), то с помощью исчисления высказываний мы можем в первой из трех упомянутых выше формул устранить вторую посылку (пере- 1) См. с. 153. становкой посылок и применением схемы ааключепия), так что получится Чх уй Э1г (Зи Я (х, у, г, и) » В (х, у, г)) — » 7х Зу у г В (х, р, г) . Эта формула вместе со второй и третьей иэ указанных выше формул по схег!е заключения с применением тождественной истинной формулы (А — » Р) -»(( — 1- (П вЂ” » К)) -»((С»(г'-1.)р))-» (А&В&С -1 И'))) дает формулу ((2)) ~х эу 7г (Зи Я (х, у, г, и) -» В (х, у, г)) & ~хну(7гВ(х, у, г) — » С(х, у)) &Мх(Зд С(х,у)-»Р(х)) — »Ъ'хР(х).
Тем самым формула ((2)) оказывается выводимой иэ заданной нам формулы 7х Зу Чг Зи Я (х р г, и). Имеет место и обратная выводимость. Действительно, если в предыдущей формуле вместо В (а, Ь, с), С (а, Ь) и Р (о) подставить соответственно формулы 3 иЯ (а, Ь, с, и), угЗиЯ (а, Ь, г, и) и Зу7гЗи Я (а, у, г, и), то получится — поскольку по нашему предположению переменные В, С иР в Я (х, у, г, и) не входят— формула Чх ту уг (Зи Я (х, у, г, и) -» Зи Я (х, у, г, и)) & ~хну(УгЗиЯ (х, р, г, и) — »7гЗЕЯ (х, р, г, и)) & '11х (Зу 'у г 3 и Я (х, у, г, и) -» Зу Чг Зи Я (х, у, г, и)) -» э!х Зу угЗи Я (х, у, г, и). В ее посылке стоит конъюнкция, члены которой являются выводимыми формулами.
Поэтому сама эта конъюнкция также вывод1лма и по схеме эаключения мы получаем ЧхЗу7г ЗиЯ (х, р, г, и), т. е. формулу ((1)). Тем самым (при сделанных предположениях относительно формульных неременных) мы установили, что заданная нам формула ((1)) дедуктивно равна формуле ((2)). Это дедуктивное равенство можно объяснить, сравнив эти формулы с точки зрения их содержательной интерпретации. В самом деле, легко убедиться, что общезначимость формулы ((1)) равВозначна общеэначимости формулы ((2)).
Докаэательство дедуктивного равенства формул ((1)) и ((2)) как раз и дает нам усиление этого факта в духе теории доказательств. Теперь формула ((2)) может быть переведена в нормальную диэъюнкцию. Именно, сначала по правилам исчисления выскаэыва- $ з1 дедуктиВное РАВЕНСТВО И деДУКЦИОННАЯ ТЕОРЕМА 207 1гл, 17 ИСЧИСЛЕНИЕ ПРЕДИКАТОВ 206 ний ее можно будет преобразовать в формулу 1 '1(х зу )7з (Зп Я (х, у, з, и) -+. В (х, у, з)) 1/ 1'зх Чу (17з В (х, у, г) -э С(х, у)) ~( 1 Ух(Зу С(х, у) — >-Р(х)) ~/ Чх Р (х); далее, по правилу (А) ') формулу 1 Ъх Чу 'уз (Зи Я (х, у, з, и) -Р В (х, у, з)) можно будет преобразовать в Зх Зу Зг 7 (Зи Я (х, у, з, и) — ~- В (х, у, г)), затем, по правилам исчисления высказываний и по правилу (7)) з), в ЗхЗуЗз(ЗВЯ (х, у, з, и) & 1В(х, у, з)) и, по правилам (с) и (7)), в ЗхЗуЗзЗи(Я (х, у, г, и) & 7 В(х, у, з)); совершенно аналогичным образом формулу ~ 'ух Чу (Чз В (х, у, з) -э С (х, у)) можно преобразовать в ЗхЗу'Рз(В(х,у, з) & 7 С(х,у)) и формулу 1 Ух (ЗуС (х, у)-Р Р (х)) в ЗхЗу(С(х, у) & 7 Р(х)), так что в целом мы получим формулу Зх Зу Зз Зи (Я (х, у, з, и) & 1 В (х, у, з)) 1/ Зх Зу чз (В (х, у, з) & 1 С (х, у)) 17' Зх Зу (С (х, у) & 1 Р (хЦ '17' Чх Р (х).
Эта формула имеет искомый вид нормальной дизъюнкции и при атом она дедуктивно равна заданной формуле ухЗу узЗиЯ (х, у, з, и), так как мы получили ее путем соответствующего преобразования иэ формулы, дедуктивно ей равной. Иа рассмотрения этого примера можно без труда извлечь и общий метод, применяя который можно для любой заданной формулы построить дедуктивно равную ей нормальную диэъюнкцию. Тем самым мы заодно получили и дока- тельство теоремы Сколема. Д о п о л н е н и е 1.
Рассмотрение приведенного нами дока- зательства непосредственно показывает, что теорема Сколема, а также и более сильная теорема о нормальной дизъюнкции, оста- ') См. с. 161. ~) См. с. 177. ется справедливой и в том случае, если мы будем рассматривать такие формулы, в которых кроме логических знаков и переменных фигурируют также предикатные, а быть может, и индивидные сим- волы. Д о п о л н е н и е 2.
Процедуру перехода от заданной пред- варенной формулы к нормальной дизъюнкции мы выбрали с таким расчетом, чтобы запоминание ее было возможно более легким; именно, каждому в отдельности квантору всеобщности или суще- ствования, входящему в приставку предваренной формулы, не считая первого из ннх и следуя в обратном порядке, мы поста- вили в соответствие некоторую формульную переменную.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
