Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 38
Текст из файла (страница 38)
При в и ло (р): Если какая-либо формула имеет вид дизъююсции, то е любом ее члене любой терм можно заменить какой- либо связанной переменной, связав зтц переменную кеаитором существования, простанленным в начале етого дизъюнктиеного члено. При в и ло (н): Если какая-либо формула имеет еид дизъюнкции и если один из ее членов содержит какую-либо сеободиую индиеидиую переменную, не зходящую е другие члены етой дизъюикции, то зту сеободиую переменную внутри рассматриваемого члена можно всюду заменить какой-нибудь связанной переменной и простоеить е начале етого члена соотеетстеутощий кеаюпор всеобщности. Выбирая связанные переменные, необходимо всякий раз следить за тем, чтобы между ними не возникало коллизий.
Правило (р) получается с использованием основной формулы (Ь) и средств исчисления высказываний. Так как средства исчисления высказываний позволяют производить различные перестановки и группировки членов дизъюнкции, то можно считать, что рассматриваемая дизъюнкция имеет вид тй )/ 6 (1), где 1 — терм, который должен быть заменен связанной переменной, Таким образом, задача заключается в том, чтобы формулу И 'у/6(!) перевести в формулу вида Р! 'уу' "=)утВ (у), где й обозначает какую-либо связанную переменную, не входя') См.
т. 1, с. 145-147 н 174 — 182. всимвол и логичгскии вогмллизм! 174 (гл гп 175 ЙТОРАЯ е тгОРЕМА щую в 6 (а). Эта формула выводится нз за1~айной формулы и формулы 6 (1) е- 336 (й), получающейся путем подстановки из основной формулы (Ь). Заметим, что здесь допускается, чтобы терм 1 входил в формулу й( '1/ 6(1) и на местах, отличных от указанных (в частности, он может входить и в формулу д). В правиле (т) мы сделали более сильное предположение.
Здесь заменяемый терм должен быть свободной индивидной переменной, и он может встречаться только внутри модифицируемого члена дизъюнкции. Как и при обосновании правила (р), здесь можно считать, что заданная формула имеет вид 'в ~У 6(с), где с — свободная индивидная переменная, которая встречается только в указанном месте. Задача заключается в том, чтобы эту формулу перевести в формулу вида 'л Ч )7'Ф (г), где х — некоторая связанная переменная, не входящая в 6(с). Этот переход мы выполним следующим образом: сначала преобразуем формулу 'Л '1/6(с) фон мулу ) д -~ 6 (с), потом из этой формулы с помощью схемы (а)') [а также, возможно, некоторых подстановок и переименований) получим формулу )6- 1Уй6Ю, а затем уже с помощью элементарного преобразования получим формулу в '17' )Гй6 (Е).
Между прочим, пользуясь основной формулой (а), можно провести этот переход и в обратном направлении, так что модификация формулы по правилу (т) всегда представляет собой обратимую операцию, в результате которой первоначальная формула переходит в формулу, дедуктивно ей равную. Модификация же формулы по правилу (р), как легко убедиться, вообще говоря, не является обратимой. е) См.
т. 1, с. 142, Геперь с помопц,ю правил (р) и (м) мы произведем обратный переход от формулы (Зе) к формуле к4. Во-первых, к каждой из переменных а( ,)', „ а(„ ,), + „ ..., а , „ входящих только в последний член дизъюнкции (Зе) и не входящих в термы (,, ..., 1„, мы можем применить правило (ч) и в результате э-кратного применения этого правила (в качестве свЯзанных пеРеменных мы беРем 13, ..., 1)е) вместо этого последнего члена получится член е 'авен ((1 "° ° (, Эв ° ° е Фе) (в) (в) а в результате е-кратного применения правила ()е) (в качестве связанных переменных мы берем гв ..., хе) вместо этого члена получится член :-)~ "Ж,,~(ре,. ФЬД(у» ..., хв э» ..., уе), Переменные а(в -е).а+ в "° е а(в-е) а фигурируют только в предпоследнем члене дизъюнкции, причем они не входят в термы (в — е) (в -е) ," >(е так что с предпоследним членом мы можем поступить в точности так же, как перед этим поступили с последним, и вместо него опять в результате а-кратного применения правила (м) и последующего г-кратного применения правила (р) получится член =(Ее" ° =)йе17зе" ° яде' (Ев ".
Це). Этот процесс может быть продолжен и далее, и в результате мы получим дизъюнкцию, у которой каждый член имеет вид Бйе " 'Зй,ФЬ " ФФ (Ив " ' це), т. е. совпадает о формулой 1х. Разумеется, эта дизъюнкция с помощью средств исчисления высказываний может быть преобразована в (Е. Таким образом, действительно, с помощью средств исчисления предикатов от формулы (Зе) можно вернуться к формуле (х. Тем самым доказательство второй е-теоремы закончено. Пользуясь методом, примененным в этом доказательстве, мы получим некоторые дальнейшие результаты. 7 176 в-СИМВОЛ И ЛОГИЧЕСКИИ ФОРМАЛИЗМ 1гл.и! й 2. Распространение второй е-теоремы иа об ую аксиому равенства.
Смежные проблемы Наше доказательство второй е-теоремы, существенным образом опиралось на обобщенную первую е-теорЕМУ, благодаря которой, как мы помним, оказывался возможным переход от формулы (2) 'ЗГ!".'ЗУ,9((гы " К, (е(Ю! ", й). ". (а(йд ", Г,)) к дизъюнкции (3), состоящей из членов вида 9(~1(11, ..., 1(', г, (1(!), ..., 1(,"), ..., (а (1!0, ..., !!")) (1 = (, ..., ш). Поэтому представляется правдоподобным, что и вторую е-теорему, подобно первой, можно будет распространить на тот случай, когда в рассматриваемом формализме Р, кроме собственных аксиом, имеется общая аксиома равенства ()в). Действительно, этого удается достичь путем небольшой модификации нашего предыдущего доказательства.
Наша задача заключается в том, чтобы по любому осуществляемому в рамках формализма г выводу какой-либо не содержащей а-символа формулы (Е получить такой вывод этой формулы, в котором е-символ не участвовал бы. В данном случае можно вновь произвести те упрощения, которые были произведены нами ранее'), т.
е. можно считать, что в исходном выводе формулы й не используются собственные аксиомы, а также что формула ц имеет вид сколемовской нормальной формы, содержащей в кванторной приставке хотя бы один кваитор существования. Тем самым наша задача сводится к следующей. Пусть дана формула 6 вида =(ХА" ° =(йе!7!7А ° ° ег!!ай((й " й„зы "° > !)а), построенная из символов исчисления предикатов и, возможно, некоторых индивидных, функциональных и предикатных символов; пУсть хе, ..., Хе, !!а„..., эа — полный список входащих в нее связанных переменных, и пусть задан вывод этой формулы средствами исчисления предикатов с использованием аксиомы равенства ()в) и е-формулы! требуется построить такой вывод этой формулы, который использовал бы только средства исчисления предикатов и аксиому равенства ()в), Для этого мы, как и раньше, сйачала из формулы ц средствами исчисления предикатов выведем соответствующую формулу ц! :-(Г " 3Ю„!!1(Ге, ", й„!.(Ры ", й,) "' (а(й "' Ке)).
!) См. рассуждение на с. 170 — 175. 177 ВКЛЮЧЕНИЕ АКСИОМЫ !Л! ВО ВТОРУ!О е.ТЕОРЕМУ тнк что в итоге' получится вывод этой формулы, использующий средства исчисления предикатов, аксиому равенства ()в) и е-формулу. 1!з этого вывода по усиленной первой е-теореме' ) получается вывод некоторой дизъюнкцни Т,, состоящей из членов вида 91 , '!'), ..., 1,", (,(!1!), ..., 1(!!), ..., (,(1(!), ..., 1(!))) (!=1, ..., ш), где термы 1,, ..., 1, не содержат вхождений (1) (й е-символа, причем этот вывод осуществляется средствами элемен. тарного исчисления со свободными переменными с использованием ряда специальных аксиом равенства.
Процедура исключения, с помощью которой получается этот вывод, дает нам его в модифицированном виде, где подстановки уже перенесены в исходные формулы, так что эти исходные формулы получаются в результате подстановок частично из тождественно истинных формул исчисления высказываний, а частично из специальных аксиом равенства; результирующая же формула вывода л) при этом получается из исходных формул в результате применения одних только схем заключения (и повторений). При этом следует обратить особое внимание на то, что ни одна . из применяющихся специальных аксиом равенства не яв ляется аксиомой равенства для какого-либо аргумента какого-либо из функциональных знаков 1„ ..., (а.
Действительно, эти знаки появляются в выводе формулы 6, только в результате подстановок вместо инднвидных переменных ') и они не входят ни в одну из формул вида а = 9 — (6 (а) — е! (Ь)), которые в этом выводе формулы ц! получаются в результате подстановки в аксиому ()в). Пусть теперь Е„..., Е! — те из исходных формул, которые получаются путем подстановки из специальных аксиом равенства. Тогда по дедукционной теореме формула Еей!...й91-~-Ь может быть выведена средствами одного только элементарного исчисления со свободными переменными а) без использования аксиом. Следовательно, эта формула должна получаться в результате подстановки из тождественно истинной формулы исчисления высказываний и то же самое должно быть верно и для любой формулы, получающейся из нее в результате перестановок дизь- !) См.
с. 109 н далее. в) См. вывод формулы (2) на формулы 6 на с. 170. ') См. т. 1, с. !99 н далее. 178 (г.ч ги 191 Ч .. Ч ~91 ')7'л1е .СИМВОЛ И ЛОГИЧЕСКИЕ фО~МАЛИЗМ 1 юнктивных членов, вычеркивания внутри формулы л) повторяющихся дизъюнктивных членов или же таких замен некоторых термов другими термами, при которых совпадающие аргументы элементарных формул снова переходят в совпадающие. В результате этих операций, как было показано выше, мы можем добиться того, чтобы вместо дизъюнкции а1 у нас получилась дизъюнкция Зе, имеющая вид 11 й 1' (е1) 1(1п) Ч 11 е ''' ° 'Е ° «1е1 — 1) Е+1е . ° "Е1 6)~ где з„..., Вм — вновь введенные занУмеРованные свободные индивидные переменные, причем переменные а, а . (1-1) Е+1 "е "1 Е не встречаются ни в одном из термов 11(, ..., 1(') (1=1, ...
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
