Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 37
Текст из файла (страница 37)
74 из этого вывода мы получим вывод формулы 1», осуществляемый средствами исчисления предикатов, с использованием аксиом Йз,... з(1 и без использования в-символа. Следовательно, нам достаточно рассмотреть случай, когда формула 6 выводится без применения аксиом, т. е. средствами одного только исчисления предикатов с использованием е-формулы. Еще одно упрощение может быть получено с учетом того обстоятельства, что в доказательстве нашей теоремы формула ьт. всегда может быть заменена любой формулой СР„ дедуктивно ей равной относительно исчисления предикатов.
Действительно, в этом случае формула ~~, тоже будет выводиться средствами формализма )о, и если из вывода формулы 6, применение и-символа можно будет исключить,. то с помощью осуществляемого средствами исчисления предикатов вывода формулы СР из фор- з) См. Приложение 1, с. 471. а) См. рассуждение в т. 1, с. 199. мулы 6з мы получим вывод формулы Ф, осуществляемый без использования в-символа. Поэтому, не ограничивая общности, можно, например, считать, что формула Ф имеет вид сколемовской нормальной формы ') Лр,... ЗЕ,у«,... Ч«эр(($„...,«д), где йы ..., Ге, »,, ..., «„— полный список связанных переменных этой формулы.
При этом можно считать, что по крайней мере один квантор сугцествования имеется на самом деле. Действительно, если й — произвольная формула, 8( ) — формульная переменная, с одним аргументом, а à — связанная переменная, не входящая в 8, то формула Лу((6(х) ~/ ~З(й)) се 5) и формула 11 переводимы друг в друга'). Таким образом, наша задача сводится к тому, чтобы показать, что и-символа могут быть исключены из любого вывода формулы 6 вида Ж ...
Лй, '41«з ... ~У«,Р( (йы " , «а), где ры ..., хе, «„..., «а — полный список связанных переменных этой формулы и гчьО, осуществляемого средствами исчисления предикатов с использованием е-формулы. Для случая, когда число кванторов всеобщности в приставке формулы 6 равно нулю, это утверждение получается в качестве почти что непосредственного следствия из обобщенной первой в- теоремы. Действительно, в этом случае формула 6 имеет вид Без "ЛЕ,Е(Е ° ° ° Рд, и по выводу этой формулы, осуществляемому средствами исчисления предикатов с использованием а-формулы, согласно первой а-теореме можно построить осуществляемый средствами одного только исчисления предикатов вывод некоторой дизъюнкции членов вида Р((1ы ..., 1„) ') См.
!, с. 203. е) Впрочем, случай, когда формула 6 имеет вид ~е«з" ° уран (см "° се), где Рм ..., Ра — полный список свЯзанных пеРеменных этой фоРмУлы, может быть рассмотрен уже с помошью первой е-теоремы, так как из формулы такого вила путем замены связанных переменных свободными всегда может быть получена дедуктивно ей равнав формула, нв содержашан связанных переменных.
ВТОРАЯ в.ТЕОРЕМА $п в-СИМВОЛ И ЛОГИЧЕСКИИ ЕОРМАЛИЗМ 1гл и1 где 1,, ..., 1,— термы без связанных переменных. Но от любой такой дизъюикции мы можем с помощью средств исчисления предикатов перейти к формуле Ст, так что в общем и целом у нас получится вывод этой формулы средствами одного только исчисления предикатов. Общее доказательство мы проведем по аналогии с рассмотренным частным случаем. Мы будем исходить из выводимой в исчислении предикатов формулы (1) 1(«1...'11«вА(ав, ..., а„«„..., «,)- А(а„..., а„, Ь„..., Ь,), которая получается применением основной формулы (а) (Вместе с необходимыми переименованиями связанных переменных) и правила силлогизма.
Мы введем 6 новых функциональных знаков с с аргументами (1(св, ..., с,), ..., (в(с„..., с„). Используя эти знаки, мы из формулы (1) подстановкой получим формулу У«1... 1в«вА(ав, ..., а„«м ..., «в)-« -«А(а„..., а„(1(а„..., ав), ..., (в(а„..., а,)), а из нее, применяя нужное число раз правило (6)') и производя подстановку, получим формулу :-)~," ЭГ,11« " 'ч««((й, ", ~, «, .", «) :-)йв" ЛГ,«((«1,.",й,. (1(ГО ", й,), ", (,(Гв, "„й,)), которая вместе с формулой (х по схеме заключения дает формулу (2) З~,... Э~,а (~,, ..., ~„ 1, («„ ..., ~„), ...(, (~„ ..., й,)).
Таким образом, для формулы (2) у нас имеется вывод с помощью средств исчисления предикатов и е-формулы. Согласно обобщенной первой е-теореме') по этому выводу можно построить вывод без связанных переменных для некоторой дизъюнкции в) ~„~ Е (1(м) 1(м) ( ('1(1е) 1(м)) ° ~1(м) (а)) ) (р (м) где 1,, ..., 1, — некоторые термы, не содержащие вхождений е-символа. Этот вывод можно осуществить средствами одного в) См. т.
1, с, 146. ° ) См. с. 54. только элементарного исчисления со свобвдными переменными. Процедура исключения, с помощью которой мы получаем этот вывод, дает нам вывод в такой модификации, что подстановки оказываются перенесенными в исходные формулы, так что результирующая формула (3) получается из исходных формул применением одних только схем заключения (и повторений); при этом исходные формулы получаются из тождественно истинных формул исчисления высказываний в результате подстановок. Если теперь в этом выводе мы заменим каждую элементарную формулу некоторой формульной переменной, причем так, чтобы графически совпадающие элементарные формулы заменялись одинаковыми переменными, а графически различные — различными, то схемы заключений снова перейдут в схемы заключений, а исходные формулы перейдут в тождественно истинные формулы исчисления высказываний.
Поэтому и формула, которая получится на месте формулы (3), тоже должна быть тождественно истинной. С другой стороны, формула (3) получается из этой формулы в результате подстановок, так как в только что произведенной нами замене совпадающим формульным переменным соответствовали совпадающие элементарные формулы. Следовательно, формула (3) получается в результате подстановки из некоторой тождественно истинной формулы исчисления высказываний, а потому это должно быть справедливо и в отношении любой из тех формул, которые получаются из формулы (3) путем замены терман („(1(1), ..., 10), р=1, ..., е; 1-1, ", Вв.
какими-либо свободными индивиднымн переменными, если при этом графически совпадающие аргументы элементарных формул заменяются одинаковыми переменными. Чтобы выполнить такого рода замену, мы прежде всего заметим, следующее. Если рассматривать термы (р~г,, ..., 1, ) — кото- ! (1) (1)1 рые мы для краткости обозначим посредством 1'„(р=1...., е; 1=1, ..., Вв),— интересуясь тем, как часто в каждом из них встречаются функциональные знаки из списка 1„..., (в (причем каждый из них считается с учетом его кратности), то эта «кратностьр для всех термов будет одной и той же, и, значит, оиа может быть однозначно сопоставлена числу 1, которое является номером некоторого члена дизъюнкции (3). 17З ВТОРАЯ е.тгоппмд 4П е-символ и логичнскии «топмдлизм !гл ш Члены дизъюнкции (3) можно расположитьув таком порядке, чтобы соответствующие им «кратности» при возрастании номеров дизъюнктивных членов не убывали (этого можно достичь, исполь- зуя средства исчисления высказываний).
Можно также считать, что в дизъюнкции (3) нет повторяющихся членов, потому что в противном случае эти повторения тоже можно было бы устра- нить с помощью средств исчисления высказываний, При соблюдении этих условий будут выполняться следующие два утверждения о термах, входящих в формулу (3): 1. Если р отлично от а или ! отлично от 1, то термы !' и !1 » графически различны. Действительно, графическое совпадение термов !' и !' может Р 1 иметь место только тогда, когда совпадают р и ц; кроме того, для совпадения й с 1' требуется, чтобы терм !!'! совпадал с терр « И! мом 11) при всех щ= 1, ..., т. Но при выполнении этих условий (й термы !'„..., !', совпадают с термами (1„..., 1,', а ьто может иметь место лишь тогда, когда число т совпадает с числом !.
2. Терм !'„может совпадать с одним из термов !(!) ..., 1!'! Ф или быть его составной частью лишь тогда, когда т меньше 1. Действительно, если !'„совпадает с одним из термов !(!), ... или является составной частью одного из них, то крат(!) ность, сопоставленная числу т, меньше кратности, сопоставлен- ной (, и следовательно, ! меньше !. Возьмем теперь набор ранее не встречавшихся занумерован- ных свободных индивидных переменных аы...,ам в и заменим в формуле (3) каждый из термов 7„(р= ), ..., б; т= 1, ..., щ) переменной а(; В.а+в»), причем эту замену мы произведем всюду, где терм 7„' входит в формулу (3), но не является составной частью какого-либо другого терма !!.
Тогда ввиду утверждения ! мы снова получим формулу, являющуюся результатом подстановки в тождественно истинную формулу исчисления высказываний. ) Обпзпаченпн в а, (1 — 1) е+в н другие нм подобные здесь н в дальнейшем следует понимать как обозна«сняв цифр, подучающнхсн в результате вычнсденнв соответствующих арнфметнческнх выражений.- В получившей«си таким образом формуле (3 ) 21(!т", ..., Р,", а„..., а,) )~ й((!т*', ..., !',", а«4 ы .", т ) Ч," Ч в / (в) (в) ~ ° ° ° е 1„1 а( — т) »4 3~ ° ам а) переменные а(; т).а.! „ согласно утверждению 2, не встречаются ни в одном из первых т — ! членов дизъюнкции, а также ни в одном из термов !(!1, ... ,(й е Это обстоятельство позволяет вывести средствами исчисления предикатов из формулы (3*) формулу (3), Для изложения этого вывода к ранее сформулированным производным правилам '1 (у) — ()ь) исчисления предикатов целесообразно добавить два новых.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
