Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 46
Текст из файла (страница 46)
Вывод любой не квазипредваренной формулы б теперь может быть проделан следующим образом. Сначала мы строим некоторую квазипредваренную формулу !Т„переводимую в й. Эту формулу только что описанным способом выводим из некоторой истинной в логике высказываний бескванторной формулы ц„а затем надлежащими преобразованиями возвращаемся от !Тт к 5. Формула йт в свою очередь может быть получена преобразованиями из некоторой построенной из элементарных формул конъюнктивной нормальной формы, которая тоже является истинной в логике высказываний. Если проанализировать шаги, на которые может быть разложено получение формулы б в соответствии со сказанным выше, то можно убедиться, что вполне достаточно пользоваться следующими правилами вывода: а) Правила ассоциативности и коммутативности для конъюнкции и дизъюнкции.
б) В качестве исходных формул разрешается брать формулы вида а т,у-)й1 т,ух)з )/... ~/Ю, (г~О) или конъюнкции таких формул', здесь й! — элементарная формула, а каждое к)т (1=1, ..., и) — либо элементарная формула, либо отрицание элементарной формулы. в) Выражение Яй(6 '!/ га) может быть заменено выражением (г(й6) 17(ЯйЯ); выражение (Я 11* 6) й(6 !7' 5) — выражением Я !у' (6й6). г) Выражение 6 может быть заменено выражением ) )тЛ; выражение ) Яй ) 6 — выражением ) (Л Т( 6); выражение ! 6 'у' ) 6 — выражением ) (6 й 6).
д) Разрешается вычеркивать повторяющиеся члены дизъюнкции. е) Выражение ) 6 'ту' 6 может быть заменено выражением Я- 6; выражение () 6 17 6)й(2! (/ ) 6) — выражением 6 6. ж) Выражение Чу ) 6(~) может быть заменено выражением ) чку! (к)' выражение Чг ) 6(г) — выражением ) Чтб(х). з) Если формула 6 не содержит переменной г, то можно выполнить следующие замены: выражение Уу(6(г) й6) может быть заменено выражением )7у21 (г) й 6; выражение Чр (6(г) 1г' 6) — выражением Чуу! (г) ту' 6; выражение Чу (6 (й) ~7 6) — выражением !756 (а) тг' 6; выражение Эр(6 (г) й 6) — выражением Эу)! (г) й6. и) Действуют следующие две схемы: Л(1) 6 (и) и ЭФ (Г) ~Ф (й) (здесь ! — терм, а и — свободная переменная, не входящая в выражение 6 (г); в первой схеме 1 может входить в 6(~); в обеих схемах переменная г не должна входить в верхнюю формулу).
к) Разрешается производить переименования связанных переменных, если при этом не возникает коллизий между ними. В правилах в), г), е), ж) и з) замена производится только в указанном направлении. Эти правила могут применяться не только к целым формулам, но в равной мере и к составным частям формул.
Эти части не обязаны быть формулами, но в этом случае они должны быть выражениями, получающимися из формул в результате замены свободных переменных связанными. В отношении выводимости формул описанное этими правилами ограниченное исчисление предикатов') — в силу ранее проведенного нами рассуждения, связанного с теоремой Эрбрана, — равносильно обычному исчислению предикатов. Но эта равносильность не распространяется на выводы формул из других формул. Действительно, в обычном исчислении предикатов выводимость формулы 6 из формулы Я, если 6 не содержит свободных переменных, равносильна выводимости импликацни 6-+.6. В нашем ограниченном исчислении это утверждение уже неверно, потому к.„Я-+$ что среди его правил нет схемы В отличие от этой т) Это исчисление очень близко к исчислению К,, построенному Куртом Шютте в его работе: 5 с Ь а 11е К.
5с!1!натке!зеп!та!!сй!е бег Ргсабига1еп!ояпт.— Ма!а. Апп., 1рз, 123, 6. 47 — 65. Однако оно немного уже исчислении Ка. 212 а-символ и логическии еоимдлизм (гл. Рн 213 КРИТЕРИИ ОПРОВЕРЖИМОСТИ схемы, правила описанного нами ограниченного исчисления предикатов устроены так, что они не дают возможности исключать какие-либо формулы х). Замечание. Формулировка теоремы Эрбрана, не ограничивающаяся квазипредваренными формулами, приведена в работе «Еа!зе 1.епппаз 1п НегЬгап«)з (см. сноску на с. 203).
Эта формулировка содержалась уже в диссертации Эрбрана, хотя и не в очень явном виде. Однако в его доказательство потребовалось внести существенное исправление, в результате чего лемму из раздела 3.3 пятой главы диссертации Эрбрана пришлось заменить более слабым и более сложным утверждением. Доказательство этой модифицированной леммы дано в работе Б.
Дребена и Дж. Дентона: 1) геЬеп В., Оеп(оп Л. — А. тпрр!ешеп1 1о НегЬ- гапб. — Л. ЯушЬ01(с 1.ой!с, 1966, 31, р. 393 — 398. Впрочем, эта общая формулировка теоремы Эрбрана несущественно превосходит ее формулировку для случая квазипредваренных формул.
Даваемый ею критерий выводимости формулы эквивалентен критерию, получающемуся преобразованием формулы произвольного вида в квазипредваренную формулуз) и применением к этой последней теоремы Эрбрана для квазипредваренных формул. й 4. Критерии опровержимости в чистом исчислении предикатов Наряду с формулировкой, содержащейся в предложениях а) и б) '), теорема Эрбрана допускает еще одну формулировку, которая более тесно примыкает к содержательному истолкованию формул и которой сам Эрбран отдавал предпочтение.
В общем случае эта формулировка оказывается несколько усложненной, но, если ограничиться случаем чистого исчисления предикатов, она приобретает прозрачный характер. Для того чтобы подойти к этой формулировке, мы сначала рассмотрим случай, когда формула (у имеет вид сколемовской нормальной формы ЭГ«...ЧЕ«'((1З...Ф)«6(Г«, ..., 3„«)х, ..., 0«) з) Систематическое изучзиие такого рода ограниченных, задаваемых правилами форм исчисления предихатов, дающих ту жа самую совокупность выводимых формул, ио ие содаржащих правил, позволяющих и«злю«ать иахиалибо формулы, были, впервые осущаствлвио Г. Гаицаиом в аго трактате «1(п(егзпсьппйэп йьег даз (ой!асье 3«Ы(езеп» (см.
сноску 2 иа с, 202). Рассуждении Геицеиа относятся к некоторому специальному исчислению — исчислеиию саивеиций. То, ято его рассмотрения равным образом могут быть осуществлены и средствами нашего исчиелеиия формул, было показано К. Шютте в аго ужа упоминавшейся работе «3«Ыцз«ье(зепха1йй(е баг Ргабгйа1еп!ойпйм ') Заметим, я«п это преобразование из использует тех правил преобразоваиия (гед1«з де рамайе), ив«орые создают определенные трудности в доказательства Др«беиа и Деитппа. з) См. с.
201 — 202. с следующими свойствами. !) в кванторной приставке этой формулы содержится по крайней мере один квантор существования и по крайней мере один квантор всеобщности; 2) она не содержит свободных индивидных переменных, а также и никаких связанных пеРеменных, кРоме гы ..., 3„ Ю„ ..., 1)з'). Если фоРмУла ьх является выводимой, то, согласно предложению а), для нее может быть указана некоторая дизъюнкция 1г 2! (!(в» !(м) ф, (1( ) !(щ)),з (1(м), !(м))), « истинная в логике высказываний, т. е. выводимая средствами и> 0) одного только исчисления высказываний.
Здесь ..., !(м), ..., !(ж) — термы, построенные из свободных индивидных переменных и г-местных функциональных знаков ф„..., ф . Если теперь эти термы заменить какими-либо другими термами таким образом, чтобы совпадающие элементарные формулы снова оказались совпадающими, то эта дизъюнкция перейдет в формулу, которую тоже можно будет вывести средствами исчисления высказываний. Замены такого рода можно производить, в частности, следующим образом: сначала каждый из термов !1", ..., !!", ..., !(ж), ..., 1(ж), не совпадающий ни с одним из термов ф (!(!), ...-, ((1)) (1=1, ..., 01 1=1, ..., щ), заменяется цифрой О всюду, где он фигурирует либо сам по себе, либо в качестве аргумента какой-либо из функций ф„..., фз.
В полученной таким образом дизъюнкции ц, каждый из встречающихся в ней термов оказывается построенным из цифры О и из функциональных знаков ф„..., «за. Затем функциональные знаки фы ..., ф„мы истолковываем как символы для некоторых вычислимых арифметических функций, зависящих от г аргументов, являющихся цифрами. В результате этого для термов, входящих в дизъюикцию ц:, получается некоторое распределение их значений, и если каждый из этих термов заменить цифрой, являющейся его значением, то у иас получится некоторая выводимая средствами исчисления высказываний дизъюнкция ьы состоящая из членов вида «) Случаи «=О и «=о могут быть разобраны непосредственно иа основе рвпамотраииых ранее элементарных соображений; см. т. 1, с. 239 — 243.
$41 2[4 КРИТЕРИИ ОПРОВЕРЖИМОСТИ е.СИМВОЛ И ЛОГИЧЕСКИИ ФОРМАЛИЗМ [Гл «и где и«, ..., и, — цифры, а 1; (при [ = 1, ..., 6) представляет собой значение функции «р,(п„..., е„). Пусть теперь р — наибольшая среди цифр и„..., п„стоящих в членах дизьюнкции ц4«на местах 3-переменных формулы 6. Тогда Т«будет поддизъюнкцией дизъюнкции, состоящей из (р+ 1)' членов вида «1(п, [,, и,,; 1, [. ° [к[) где номер [ члена этой дизъюнкции пробегает значения от О до (р+1)' — 1 включительно, цифры 1,, (при 1=1, ..., Е) являются значениями функций «р,(п, р ..., и,;), а список и, „ ..., и ; ...; п , ..., и «,(р+«)е — «' '''' е,(р+«)е — « содержит в каком-либо порядке все г-членные наборы цифр, не превосходящих р.
Порядок этот мы выберем так, чтобы из двух наборов, различающихся максимальными входящими в них цифрами, предшествующим считался тот, максимальная цифра которого меньше; а для наборов с одинаковыми максимальными цифрами мы будем считать этот порядок лексикографическим, так что из двух таких наборов предшествую«цим является тот, у которого цифра, стоящая на первом месте, где эти наборы различаются, является меныпей, Построенную таким образом дизъюнкцию мы обозначим через [хр . Она тоже может быть выведена средствами исчисления вы««и сказываний, так как дизъюнкция З«содержится в ней в качестве поддизъюнкции. Для любой цифры ч и для любой системы «р, состоящей нз з р-местных арифметических функций ф„..., фр, значения которых можно вычислить — а в случае конечной области определения, состоящей из р-членных наборов цифр, не превосходящих ч, даже задать путем прямого перечисления,— мы обозначим через «Р«ч' дизъюнкцию, состоящую из членов где и, р ..., п,; — всевозможные «-членные наборы цифр, не превосходящих Ч, взятые в указанном выше порядке (число этих наборов равно (я+1)', а цифры 1;; (при (=1, ..., Е) являются значениями функций «р,(е,;, ..., и, 1)1.
Для любой такой дизъюнкции можно непосредственно выяснить, выводима ли она средствами исчисления высказываний. С этой целью достаточно заменить различные входящие в нее элементарные формулы различными функциональными переменными без аргументов и проверить, является ли полученная таким образом формула исчисления высказываний тождественно истинной. если цифра [ меньше ч, то дизъюнкция (х)Р' является поддизъюнкцией днзъюнкции 6~э[. Поэтому, если Щ" окажется выводимой средствами исчисления высказываний, то же самое можно будет сказать и относительно 6~ей Итог наших рассуждений сводится к тому, что по любому выводу формулы 6 в исчислении предикатов, произвольным образом выбрав вычислимые арифметические функции от г аргументов, можно указать такую цифру [Ч что формула К~э' будет выводима средствами исчисления высказываний.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
