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