Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 43
Текст из файла (страница 43)
Применяя правило (1А), эту формулу можно затем преобразовать в формулу :-)14сх4ссу)иВо'егВв4Л(1, х, у, и, о, г, в), т. е. в формулу й. м из тех членов Описанную процедуру мы применим к каждому из дизъюнкцни „у к ни г) которых переменная а,„встречается в Ь-терме. Если при этом возникнут повторения каких-либо членов дизъюнк- ции, то лишние члены мы вычеркнем. ем к некоторой днзъюнкции е:4, которая, вообще Так мы придем к -п вых члены вида говоря, будет содержать члены трех типов: во-перв ЭвЛ(Ь„ас, аь, с„Ь„а, в), которые мы будем называть дизъюн нктивными членами первого рода, во-вторых, члены вида Эи3оУг3вд(Ь„а ., ас, и, о, г, в), которые мы будем называть д и з ъ ю ъюнктивными члеиамн ий собой второго рода, и, р о д а, и в-третьих член, представляющий со формулу й. теОРЕМА ЭРБРАНА 4-СИМВОЛ И ЯОГИЧЕСКИИ ЬОРМАЛИЗМ <гл гп !9Я того, что вн т н эт " Переходя от дизъюнкции х< к дизъюнкции Х, .
4, мы добиваемся утри этой последней переменная а не встр -, <- или Ь-терме. Пусть переменная а„,* имеет номе наибольший с е и н м кой-либо из е р д омеров переменных а, встречающ а щихся в каиз еще имеющихся в Ж4 Ь-, <- или Ь-термов. И из е, -, - . - рмов, з нумерау из го обстоятельства, что в дизъюнкции 24 что если пе ни один и ее членов не повторяется дважды, , снова получается, переменная и,„содержится в дизъюнк Ж цни , внутри дизъюнктивного члена первого рода =Ып'(Ьь ай, а<, <и Ьо а, и<) ь' в одном из термов 1 < Ь ;, то переменная а, входит в 2 тол , только в одном-единственном месте; значит, п и к переменной а и после ю применением правила (Р) " а и последующим двукратным применением пра- вила (р) рассматриваемый член этой дизъюн р р дизъюнктивный член второго рода.
зъюнкции может быть А теперь такое же преобразование мы произведем над вс . 0 рода, задающими указанным м, и устраним все возникающие в рез льтате эти образований повторения сред и членов дизъюнкции. В пол чив- шейся таким образом днзъюнкции Ж , переменная а„,* больше уже учив- не может входить ни в <-, ни в Ь- ься в -те мах — о нак -термы, но она еще может встрер — д о только внутри дизъюнктивных членов члене второго рода.
Встречающиеся в каком-либо таком д таком дизъюнктивном ЛиЛО'чгЛи<й(Ьь и, иь, и, и, г, и<) переменные и . и а не г мо ут встречаться в 4~4 в каких-либо других местах — это опять след ет из нов. Поэтому рассматриваемый дизъюнктивный член п имен пе еменной и<, а затем к переменной а — и последующим применением правила (14) может быть пре- образован в формулу 6. Применив эт п оце второго ода изъ у р дуру к каждому дизъюнктнвному чле р д юнкции ЖБ, содержащему переменную и ° внучлену три какого-либо Ь-терма и ст анив нктивных членов, мы получим некоторую дизъюнкцию Ж„ в которой переменная а„, больше уже не будет встречаться ни в одном из Ь-, <-, Ь-термов.
члены пе вого ода в Продолжая этот процесс и п об реобразовывая дизъюнктивные < первого рода в члены второго рода, члены второго рода— в формулу 6 и вычеркивая возникающие при этом повторения членов дизъюнкции, мы последовательно удалим все те Ь-, <- и Ь-термы, в которые входят какие-либо из пронумерованных переменных а), причем эти переменные мы будем перебирать по очереди, в порядке убывания их номеров. После не более чем (р — 1)-кратного повторения описанной процедуры мы придем, наконец, к дизъюнкции, каждый член которой будет являться либо дизъюнктивным членом первого рода, либо дизъюнктивным членом второго рода, либо формулой Кроме того, ни один из членов этой дизъюнкции не будет повторяться дважды н ни один из входящих в нее 6-, <- или Ь-термов не будет содержать переменных из списка а„..., а„ Все члены первого рода такой дизъюнкции, согласно нумерационным условиям, с помощью правил (14) и (Р) можно преобразовать в члены второго рода, а после то<.о кгк это будет сделано и все возникшие повторения дизъюнктивных членов будут устранены, все члены второго рода можно будет преобразовать в формулу 6.
Но тогда — если еще раз устранить образовавшиеся повторения дизъюнктивных членов — у нас получится формула 6. Так может быть осуществлен вывод формулы <т из дизъюнкции Ж,. А так как формула Ж, получается подстановкой из некоторой тождественно истинной формулы исчисления высказываний, то мы получим вывод формулы 6 средствами исчисления предикатов. В итоге мы получаем доказательство следующего утверждения: Формула 6 ЧЮх4<уЗиЗО<вгЗ<вЛ(Г, х, у, и, и, г, <в) выводима тогда и только тогда, когда выводима формула (5) Э<'=)и=ЬЗшй((1, <9(1), ф(Г), и, и, Х((, и, о), и<), построенная с помощью ранее еще не встречавшихся функциональных знаков <9, <р и т, или (что согласно первой е-теореме сводится к тому же самому) когда некоторая дизъюнкция Ж, состоящая из членов вида '" (ч <р (ч) ф (ч) < в, х (9.
<, в) 1) где а, <, В и à — термь<, построенные из одних только свободных переменных, индивидных символов и функциональных знаков, получается подстановкой из некоторой тождественно истинной формулы исчисления высказываний. (Эта дизъюнкция Ж находится по выводу формулы (5) приме пением процедуры исключения связанных переменных с помощью введения н последующего исключеиия е-символа.) Кроме того, получается еще и следующая -символ и логичгскии фогмллизм сгл. сп Теорема. По выводу формулы 6 вида 3Яхлсупи3о'с(гЗсвй(с, х, у, и, о, г, св) всегда можно найти некоторую дизъюнкцию Ж„состояи(ую из членов вида 6(ц, в, Ь, с, 6, с, с), где в, Ь, с — свободные переменные, а ц, г, в, 1 — некоторые псермы, причем хл получается подстановкой из некопюрсйс тождественна истинной формульс исчисления высказываний, а формула Су может бьипь получена из нее применением правил (р) и (ч) и вычеркиванием повторяюсцился дизъюнктивных членов.
Полученные результаты немедленно могут быть усилены следующим образом. Искомую дизъюнкцию Ж можно всегда указать таким образом, чтобы, кроме функциональных знаков ср, лр и т, она содержала только такие внелогнческие символы, которые входят в К. Это требование равносильно условию, чтобы в термы г, с, 6 и С, фигурирующие в членах дизъюнкции О, входили только такие индивидные символы и только такие отличные от ср, лр и т функциональные знаки, которые входят в 6.
Действительно, добиться выполнения этого условия нетрудно. Именно, если в термах в, с, 6 и С первоначально будут иметься какие-либо не входящие в 6 и отличные от символов ср, лр и т инднвидные или функциональные символы, то достаточно будет всюду заменить каждый такой индивидный символ и функциональный знак переменной а. Получающаяся в результате этого дизъюнкция снова будет состоять из членов вида сс(ч, ср(ч), лр(ч), с, в, Х(ч, с, в), 1), но только термы в, с, в, 1 будут теперь другими. Сохранится и свойство днзъюнкции быть результатом подстановки в тождественно истинную формулу исчисления высказываний, потому что производимые замены сохраняют совпадение термов, а потому и элементарных формул.
Точно так же можно добиться, чтобы дизъюнкция хл содержала только такие виелогические символы, которые содержатся в 6. (По отношению к формуле Жс функциональные знаки ср, ф и )( перестают занимать особое положение.) Метод доказательства, с помощью которого мы получили перечисленные результаты, как нетрудно видеть, абсолютно не зависит от того, что взятая нами формула 6 имела некоторый специально выбранный частньпс вид.
Совершенно аналогичным образом этот метод может быть применен и к любой наперед заданной предваренной формуле. При этом имеются в виду (что в дальнейших формулировках иногда и не будет специально оговариваться) си тгогвмл згсгюсл 201 такие ч оумулы, ф рмулы которые строятся из переменных и символо исчисления предика о, р икатов, и, быть может, из некоторых индивидных функциональных и предикатных символов.
Чтобы сформулировать наш результат для произвольной фор мулы С такого типа, м (у г типа, мы заметим, что для связанных переменных входящих в К, порядок следования их в кванторной приставк станавливает некото екоторую их очередность. Переменные, связанны кванторами всеобщности, мы будем кратно называть У-п е р пе еменные, связанные кванторами существовани го, читывая, и будем называть Б-переменными; кроме то, у минавшуюся нами очередность связанных переменных, мы уде говорить об З-переменных, п р е дш ест ву ю щи х некоторо . начинае Заметим также, что в случае, когда формула на квантором всеобщности, всем 7-переменным, которым не предш :-)-переменньсе, согласно нашей процедуре должн ы так сказат быть сопоставлены некоторые индивидные символы (так бы нап име, в ра в е е ея, ой тся еы ь, н льместные функциональные знаки).
Если, р р ами формуле К не было квантора существования 31 асс ж ения и аргументной переменной с, то в начале нашего р с у д на месте выводимой формулы (1) оказалась бы формула Чх1чуА (х, у)-~А(а, й), в которой индивидные символы сх и р (как ранее ср и ф) надо было бы взять такими, чтобы они не фигурировали в самой фор- муле 6.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
