Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 68
Текст из файла (страница 68)
От аксиоматической версии этого принципа мы теперь можем перейти к его формализации; она может быть произведена, с одной стороны, посредством некоторой формулы, а с другой стороны, посредством некоторой схемы. Эта формула, а к с н о м а и нд у к ц и и, записывается в виде А (0) дг 1ух (А (х) — ь А (х'))-+ А (а). Что же касается схемы индукции, то она имеет вид Я (0) Я (а) -ь Я (а') Я (а) Эта схема (подобно схемам нашего исчисления предикатов) должна применяться при условии, что переменная а в Я (а) встречается только там, где она указана в качестве аргумента.
В том, что это ограничение необходимо, можно убедиться на простых примерах. Если мы, например, возьмем в качестве Я (с) формулу с = 0 ~/ а' = с, то соответствующие формулы Я (0) и Я (а) -ь Я (а') 327 игл. уг нАчАлА АгиФметики 326 ВКЛЮЧЕНИЕ ПОЛНОЙ ИНДУКЦИИ будут выводимыми. Если бы мы допустили применение схемы индукции к этим формулам, то в результате получили бы формулу а =0 ~/а' =а, а из нее подстановкой — формулу 0' =0 ~/О' =0', которая в сочетании с выводимыми формуламн 0' ф= 0 и 0" чь 0' привела бы нас к противоречию.
Оба способа формализации принципа полной индукции равносильны в том смысле, что схема индукции может быть получена иэ аксиомы индукции в качестве производного правила, а с другой стороны, аксиома индукции тоже может быть выведена с помощью схемы индукции. Именно, подстановкой формулы Я (с) вместо именной формы А (с) мы из аксиомы индукции получаем формулу Я (0) й Чх (Я (х) -» Я (х4)) -» Я (а). Если переменная а встречается в формуле Я (а) только там, где она указана в качестве аргумента, т. е. если в Я (с) переменная а ие встречается, то иэ формулы Я (а) -» Я (а') мы по правилу (у') ') получим формулу ух (Я (х) -» Я (х')); эта формула вместе с Я (0) по правилам исчисления высказываний дает формулу Я (0) & з х (Я (х) -» Я (х')), а эта последняя в сочетании с формулой Я (0) Й ух (Я (х) — » Я (х')) -» Я (а) дает формулу Я (а).
Таким образом, от формул Я (0) и Я (а) -» Я (а') мы с помощью аксиомы индукции приходим к формуле Я (а). 1) См. с. 446. И обратно, если мы в качестве правила возьмем схему индукции, то формула А (0) й зх (А (х)-» А (х')) — » А (а) окажется выводимой. Действительно, обозначим для краткости вту формулу посредством Я (а). Тогда, на основании схемы индукции, для вывода Я (а) достаточно будет вывести формулы Я (0) и Я (а) » Я (а'), т. е. А (0) й 7х (А (х) » А (х')) -+ А (0) и (А (0) й 'зх (А (х)-» А (х'))-» А (а)) -+.
(А (0) й 'Фх (А (х) — » А (х'))-» .4 (а')). Первая из этих двух формул получается непосредственной подстановкой иэ тождественной формулы А8сВ-» А, а вторая с использованием тождественной формулы (А -» ( — 1- С)) †» ((Р й А †» В)-» (Р 8с А -» С)) может быть получена из формулы 'ух (А (х)-» А (х'))-» (А (а)-» А (а')), которая в свою очередь получается подстановкой из основной формулы (а) исчисления предикатов.
Мы теперь покажем, что присоединение схемы индукции к нашей системе аксиом (А) не расширяет запаса выводимых формул, не содержащих формульных переменных, так что любая неверифицируемая формула, не содержащая формульных переменных, будет невыводимой и после присоединения схемы индукции. Представим себе, что нам дан вывод формулы 5, произведенный на основе исчисления предикатов с помощью аксиом (А) и с привлечением схемы индукции. Предположим,что формула 5 не содержит формульных переменных. Тогда мы сможем, пользуясь нашей прежней методикой, разложить зто доказательство на нити, поступая со схемой индукции аналогично тому, как мы поступали со схемой заключения, т.
е. сопоставляя каждой такой схеме фигуру вида :й(О) 6А(а)--Я(а') ИАчАлА АРНФмнтики 328 329 ВКЛЮЧБНИБ ПОЛНОЙ ИНДУКЦИИ При этом следует заметить, что переменная а в третьей формуле схемы не связана с переменной а во второй формуле; то, что для зтих двух формул схемы индукции мы берем одну и ту же переменную а, представляет собой некоторое соглашение, само по себе не необходимое. Таким образом, нижняя (третья) формула схемы индукции вводит некоторую новую свободную индивидную переменную, в то время как раньше по нашим правилам свободные переменные вводились только исходными формулами. Отсюда следует, что в случае фигуры доказательства с встречающимися в ней схемами индукции возвратный перенос подстановок может вести не только к исходным формулам, но и к нижним формулам каких-либо схем индукции.
Такого рода формула Я (а) тогда перейдет в Я($) с каким-нибудь термом н Теперь для того, чтобы в рассматриваемом выводе формулы б" произвести возвратный перенос подстановок, мы, во-первых, должны будем ввиду наличия схем (а) и (р) исчисления предикатов осуществить обсуждавшиеся ранее ') меры предосторожности, которые состоят в том, что в случае каждой такой схемы переменная а заменяется какой-нибудь новой переменной, которая прежде в фигуре разложения не встречалась. Очередность этих замен следует устанавливать в соответствии с обратным просмотром фигуры разложения и замену встречающейся в каждой такой схеме переменной а следует проводить до тех пор, пока рассматриваемое вхождение переменной будет прослеживаться в соответствии с зависимостью формул в выводе.
Необходимость етого мероприятия вытекает из ограничения, которое налагается на применение схем (а) и (р). Аналогичное ограничение действует и в случае применения схемы индукции, и поэтому мы должны осуществлять упомянутое мероприятие применительно и к атой схеме, заменяя всякий раз переменную а в формуле Я (а) -~- Я (а') какой-нибудь новой, ранее не встречавшейся переменной и продолжая зту замену в обратном направлении.
В остальном мы, как и раньше, перенесем подстановки назад, а затем исключим быть может еще оставшиеся формульные переменные. Все зти преобразования не затрагивают заключительной формулы 5, так как она формульных переменных не содержит. В получившейся таким образом фигуре разложения мы рассмотрим теперь одно из тех применений схемы индукции (соответственно тех фигур, получающихся из них в результате проведенных модификаций), которым при просмотре нитей доказа- 1) См. с. 286. тельства в направлении от исходных формул (т. е. в направлении развертывания вывода) не предшествует никакое другое применение схемы индукции.
Пусть формулы этой схемы в первоначальном выводе имели вид В (О), 3 (а) -~ 3 (а'), З (а), а в результате выполненных преобразований на их месте оказались формулы З* (О), В* (г) -~ З' (г'), З' (Г). При этом $ — какой-нибудь терм, а относительно переменной г мы гарантированы(в результате принятых нами мер), что в В с (г) она встречается только там, где она указана в качестве аргумента. Кроме того, мы знаем, что З*(г) не содержит никаких формульных переменных. Нити доказательства, ведущие от исходных формул к формулам В*(0), В'(г)-~В'(г ), не содержат применений схемь1 индукции, позтому они дают вывод обеих этих формул, использующий только аксиомы (А). Пусть теперь 3 — какая-либо цифра; тогда из формул В' (О), З' (г) -~.
В* (г') путем подстановок и повторного применения схемы заключения можно будет вывести В* (3). Таким образом, для любой цифры 3 формула В* (3) оказывается выводимой иа системы аксиом (А). Кроме того, эта формула не содержит формульных переменных. Следовательно, по одному из наших утверждений о системе аксиом (А) '), формула ухй* (х), а значит, и формула Зс ($) тоже могут быть выведены из системы аксиом (А) без использования схемы индукции.
Если мы теперь для какого-нибудь такого вывода формулы В* (3) осуществим разложение его на нити, возвратный перенос подстановок и исключение формульных переменных, то полученную таким образом не содержащую схем индукции фигуру разложения с заключительной формулой З* (3) мы сможем подставить вместо всех тех нитей нашей первоначальной фигуры разложения, которые ведут от исходных формул к формуле Зс (3). ') См. с. 323.
ззв нАчАлА АРИФмзтики [ГЛ, Уг ВКЛЮЧЕНИИ ПОЛНОЙ ИНДУКЦИИ в в~ Таким образом, в результате получится некоторое новое разложенное на нити доказательство формулы 5, в фигуре разложения которого схема индукции встречается на один раз меньше, чем в первоначальной фигуре разложения. Мы можем повторить использованный нами прием нужное число раэ и таким образом устранить друг за другом все применения схемы индукции, так что в конце концов мы придем к некоторому доказательству формулыЯ, проведенному без использования схем индукции, с помощью одних лишь аксиом (А). Тем самым мы фактически показали, что в результате присоединения схемы индукции к системе аксиом (А) выводимыми оказываются только те формулы без формульных переменных, которые можно было вывести и беэ использования этой схемы. В точности то же самое справедливо и в отношении аксиомы индукции, так как она выводима с помощью схемы индукции и, следовательно, не может дать больше, чем сама эта схема.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
