Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 23
Текст из файла (страница 23)
исключением те ма !. Во втором случае вместо терма 1 из ч. в ~т д терма нительно появляется некоторый терм из ~, р " р ности элементов из ч.» располагается раньше 1. Согласно ска- занному, шаг нашей процедуры, устраняющий формулу 5 из числа исходных, п х, приводит к тому, что в очередности термов из ~» этих те мов, и инадле- уменьшается номер самого последнего из этих термов, пр к ч,. Если максимальный номер терма, входящего в жавшего к з шагов нашей вначале был равен 1, то не позже чем через» процедуры все формулы фо мулы в-равенства, связанные с основным типом 1, окажутся исключенными.
Тем самым возможность совместного устранения критических формул и формул е-равенства доказана, в) Усиленный вариант первой е-теоремы и нп-теоремы. Теперь мы извлечем следствие из полученных нами результатов. Если мы вспомним рассуждения, которые привели нас к созданию нашей обобщенной процедуры, то убедимся, что благодаря возможности совместного устранения из нормированных доказательств критиче- ских формул и формул в-равенства первая в-теорема продолжает оставаться справедливой и в случае таких формализмов, которые включают в себя оби(ую аксиому равенства (д,) и е-формулу.
Поэтому имеет место следующая Теорема. Пусть Р— формализм, получаюи(ийся из исчисле- ния предикатов в результате добавления к нему 11О исслндовлнин лриемнтики пни помощи е-символл 1гЛ. и 1) и-символа и г-формулы, 2) знака равенства и аксиом (Лх) и (Зе) 3) некоторого числа индивидных, функциональчых и предикатных символоз и ряда содержащих эти символы собственных аксиом ' '))м ., Ф! без связанных переменных.
Если средствами этого формализма выводима формула 6, не содержащая связанных переменных, то по любому ее выводу мы сможем построить такой вывод этой формулы, в котором будут отсутствовать связанные переменные, так что этот вывод будет укладываться в рамки элементарного исчисления со свободными переменными.
Далее, если средствами формализма Р выводима формула ЗГ> ° ° ° =)ьпа(еп> "°, еп)> где х„..., уп — все входящие в эту формулу связанные переменные, то по любому выводу этой формулы мы слюжем получить, не прибегая к использованию связанных переменных, вывод некоторой ди ъюнкции формул, имеющих вид '((1> ° > 1п)> где 1ы ..., 1п — некоторые не содержащие г-символа термы. Кроме того, можно доказать, что в обоих этих случаях применение аксиомы (Ле) может быть заменено применением специаль.
ных формул равенства вида а=Ь-+.(С) (а)->-х)(Ь)) и а= Ь-~() (а) =((Ь)). относящихся к предикатным и функциональным символам формализма Р. В число этих формул, в частности, должна быть включена формула (!) На самом деле этот дополнительный результат получается прямо из процедуры устранения, в которой указанная замена осуществляется по ходу дела. Пусть теперь Р, обозначает формализм, который получается из Р в результате замены аксиомы ()е), указанной выше, специальными формулами равенства. Тогда, согласно сказанному, всякая не содержащая переменных формула, выводимая средствами формализма Р, будет выводима и средствами формализма Р„ и для всякой выводимой средствами Р формулы Зьпй! (1' " ~„) ВКЛЮЧГНИП ЛКСИОМЫ 1ЭО В ПНПНХЮ е.тепппмг такой, что ника икакие связанные переменные, кроме хм ..., Гп, о м лу не вхо ят, одят, мы можем указать некоторую выводиф Р изъюнкцию, состоящую из чле- м ю средствами рормализма, д му 6(1 ..., 1 ) с но содержащими е-символа термами 1„...
нов вида ' 1„..., 1п. . 1 нп-теорему'), и тогда получается, что для формализма вгл. ннп-теорема справедлива в следующей фор у р м лн овке: Пусть для элементарных формул без переменных формализма ется такое распределение истинностных значений, в силу код редикатных и функциональных символов из ве- и и и 1емы. Тогда всякая выводимая средствами ф р о мализма Р буд т истинной, всякая выводимая сред- ства ф, одержащан никаких переменньы, кр фо м ла без переменных ет ис к оме сво .
д ., б д ифицируемой и для всякой выво- ствами Р формула, не со е ж свободных индиги ных, у ет вер димой средствами Р формулы вида ЧГ1 ° 1УУп>=й)п ° ° Ъп~(Е>> "° > У>п> Рт ° 1)п) суть все входящие в эту формулу пере- где х„..., у„„рм ...,,п у в без пере') для любых фиксированных терман в,, ..., мы 1, ... 1 без пере- менных можно будет указать такие термы , ..., 1, б т истинной. менных, что формула Л(бм ..., Вв, 1м ..., Эт ленную нп-теорему мы можем применить к рассмоту уси гл. 1 системам аксиом элементарной евкл д ренным в гл.
с '). 3 есь оль специальных ментарной неевклидовой геометрии,. д р а, кото ые нужно взять вместо аксиомы лиро анные для о м ла (1), аксиомы Равенства, сроРмУ о ов бг Ъч и = (из этих аксиом могут быть предикатиых ымв лов Са, ю выв едены остальные относящиеся к этим предикатн о м лы авенства), и, кроме того, форму р лы авенства, относяс й) а в случае неевклидовой знакам >р(а, Ь, с> й) и $(а, Ь, с,, а в с и том распределении истин— е е и к у(а, Ь, с).
Можно без труда показать, что при том значений постоянных элементарных р у, о м л, которое мы ностных знач иальные аксиомы равенства бе этйх сйстем аксйом геометрйй тельство непротиворечивости о их этих ') См„с, 59 и дплее. д когда число п> кппнторое всеобщности ') Свдп пклвчеетсп и тот случп, когда и приставке равна нулю. и) См с б! и далее 119 112 ИССЛКдОВЛНИВ дГИОМКтИКИ Пан ПОМОШИ «.СИМВОЛЛ 1ГЛ и «з1 е.символ и оормллиздция поинципл индукции распространяется также и на те формализмы, которые получаются . из них, если на место прежних аксиом равенства поставить аксиомы (Яг) н ()з); при этом существенно обратить внимание на; то, что в логическом формализме, лежащем здесь в основе нашего рассмотрения, допустимыми являются также в-снмвол и е-фор- ' мула '). Фигурирующее в этой усиленной нп-теореме предположение .
о вернфицируемости специальных аксиом равенства выполняется, в частности, всегда, когда распределение значений для равенств, не содержащих переменных, — мы будем называть его выделенным распределением значений для равенства — таково, что при этом распределении равенство 6 1, где 6 и 1 — термы без переменных, принимает значение «истина» или «ложьз в зависимости от того, совпадает или не совпадает значение 6 со значением 1. Таким образом, для любого формализма г", получающегося из исчисления предикатов добавлением к нему е-символа и в-формулы, аксиом равенства (3,) и (Лз), а также некоторых индивидных, функциональных и предикатных символов и формулируемых с помощью этих символов собственных аксиом ф,, ..., р(, не содержащих связанных переменных, утверждения нп-теоремы оказываются справедливыми при любом распределении значений элементарных формул без переменных, при котором аксиомы 1))„...
..., р1 являются верифицируемыми формулами, а соответствующее распределение истинностных значений равенств является выделенным. Впрочем, для того чтобы усмотреть этот факт, нам не обяза. тельно вводить формализм га, Более того, для перехода от в-теоремы к нп-теореме достаточно установить, что всякая формула, выводимая средствами формализма г' без использования связанных переменных, является истинной. Но это может быть доказано рассуждением, совершенно аналогичным тому, с помощью которого в гл. 1 мы доказали нашу ип-теорему'), причем мы должны будем воспользоваться тем обстоятельством, что при рассматриваемом распределении значений элементарных формул без переменных аксиомы Ч)„..., Ч)1 предполагаются верифицируемыми и что каждая формула без переменных 6 = 1 — (9( (6) - й (1)) г) дкя случая, когда в основе рассмотрения лежит одно только нсчнсленне преднкатов, наш результат не дает ничего нового, так как в этом случае мы имеем в своем распоряжении теорему нз гл.
г'11 т, 1 о возможноств замены аксиомы равенства (3,) собственными аксиомами. а) См. с. 55 — 59, получающаяся подстановкой в аксиому ()е), при выделенном аспределени и делении истинностных значений для равенства является как либо ее посылка является ложной (если 6 и 1 истинном, так как л имеюч различные значения), либо (если значение 6 совпадает со значением 1) истннностное значение Д(6) совпадает с истинностным значением Й(1), и, тем самым, заключение гд(6)-ьй((1) этой формулы является истинным. Тем же самым способом с применением рассуждений, прове- в ~ ~1 данной главы'), можно показать, что утвери ля .„о мализма, ждения нашей нп-теоремы остаются в силе и д я р который получается из рекурсивной арифметики в результате и исоединения к ней рм л мул и схем для кваиторов, а также з-снмвола и е-рормулы, п -ф '), поскольку в качестве распределения элементарных формул без переменных (в данном значений для э ае это б дут одни только равенства) мы берем а р ртакое асп еделение, которое индуцируется выделены " ц ой о енкой истинностных значений для равенства и процедурой вычисления значений рекурсивных функций.
й 3. Причины, препятствующие распространению процедуры устранения ее-символов на неограниченную схему индукции. в ой млы Формализация принципа индукции с помощью второ фор у для е-символа. Переход к первоначальному гильбертовскому подходу Распространив доказанные нами в-теорему и ип-теорему на б аксиому равенства, мы в известной мере ликвидировали ощую ак о тво наших ез льнекото„ рое имевшееся до сих пор несовершенст р татов.
И все же серьезным их недостатком оста ется то обстоятельство, что результаты, касающиеся арифметического формая лишь к схеме индукции в ограниченном виде, а именно, — к схеме индукции, применяемой к формулам ез ванных переменных а), Из-за этого, в частности, до сих пор не не ротиворечивость формализма системы Е . но ли наш проВозникает естественный вопрос о том, мож у о ью кото ой сначала была цедуру устранеяия в-символов, с помощью о р пе вая в-теорема, а затем, с использованием этой теодоказана первая зим об азом, чтобы видоремы, и нп-теорема, модифицировать таким о р измененная процедура была применимой и р д м й и п и добавлении к ормализму неограниченной схемы индукции. р ии.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
