Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 123
Текст из файла (страница 123)
на с. 554) может быть определена раненстном аяп (л) а (и, О). 19 Д. Гааьберч П. Бернайс — ' 378 ПРИЛОЖЕНИЕ иу вует методу примитивной рекурсии в арифметике. Сведение носит следующий характер. Если функционал а не содержит перемен- ных д и с и выводима формула й (а) и если 5(й, с) †функцио- нал такой, что выводима формула й(д) й й(с)-~й(3(й, с)) й -~ (с, 3(д, с)), причем Б(0, О) не содержит переменных д и с, то может быть указан такой функционал ((й), что для него будут выводимы формулы й(й)-~й(((д)) й Ух(х=й-+-! (х) =((д)).
((6)) й(д) (!( )=Ь(д, ((д)), й,(с)-»[((!пп(с)) 1пп(Л„[((Л,с(т(т,(х), г)))(т,(х))])]. Наметим путь построения такого функционала. Сначала мы выводим формулу й» (й) й й (с) й ~» (д, с) -» З.т [й (х) й ЗгЗу(й гйЯС(г, с+, у) йЛ„у(т(у, и)) ='х)]. Ватем с помощью определения й (у, с, д) = е„. [й (х) й Зг=1у (й г й Бс (г, с+, у) й Л„у(т(у, и)) = Х)] вводим символ $(д, с, й) и с помощью формул ((4)) и ((5)) выво- ' дим формулу й(с)-1-Зо(й,(о) йа(о, с, О) ай 'чй(й(й) й .ч (и, с)-» 9(о, с, и+) =-ь(й, 9(о, с, й))) й Угй [й,(й) й 4 (!пи (й), с) «- 5(о, с, 1пп(и)) !пп(Л„[5(о, с, Л,и(т(т,(х), г)))(т»(х))])]!.
Если теперь по заключению этой формулы, которое имеет вид Зой((о, с); построить выражение $(~ Яф, й), й, д), то оно и окажется искомым функционалом ((д), для которого " можно будет вывести формулы ((6)). Тем самым фундамент для построения теории чисел первого и второго числовых классов заложен. Рассмотренный нами метод формального изложения этой теории соответствует канторовскому представлениЮ о числах пер- » Ю МОДИФИКАПИИ ФОРМАЛИЗМА, ИСКЛЮЧЕНИК е-СИМВОЛА Б79 вого и второго числовых классов.как о порядковых типах вполне упорядоченных множеств целых чисел. Теория эта может развнваться и независимым образом, в отрыве от такого представления, причем это можно делать, с одной стороны, аксиоматически, по аналогии с аксиоматической арифметикои, а с другой стороны, конструктивно, по аналогии с финитной арифметикой. При аксиоматическом построении этой теории рассмотренная нами формализация дает некоторый способ «сведения» этой теории к формализму анализа в том смысле, что если удастся доказать непротиворечивость формализма Н, то будет установлена и непротиворечивость этого аксиоматического формализма.
й 6. Модификации рассмотренного формализма. Исключение е-символа Формализм Н основан на систематическом использовании е-символа. Благодаря этому методу система аксиом и правил вывода формализма Н оказывается относительно простой. Правда, вопрос о том, благоприятствует ли такая структура формализма Н изучению его средствами теории доказательств, является достаточно спорным. Во всяком случае, с точки зрения аксиоматического подхода структура эта имеет определенные недостатки, так как она не позволяет четко отделять друг от друга различные содержащиеся в методах анализа предположения.
И вообще, с точки зрения логической систематики более предпочтителен формализм, который обходится без использования е-символа и а-формул '). Рассмотрим теперь формализм, который по своему устройству сходен с формализмом Н, но более привычен с точки зрения систематики (в частности, он не содержит принципа выбора), Этот формализм, который мы будем называть формализмом К, описывается следующим образом: Переменные в К такие же, как и в Н. Первоначальнымн символами этого формализма являются: индивидный символ О, штрих-символ, знак равенства, символы исчисления высказываний, кванторы с относящимися к ним (связаиными) индивидиыми и функциональными переменными, «-символ и Л-символ — оба с относящимися к ним (связанными) индивидными переменными.
Роль те р м о в играют, во-первых, свободные индивидные переменные, символ 0 и любое выражение вида а', где а-терм. Всякая свободная функциональная переменная считается функционалом. Термом будет считаться также всякое выражение вида а(3) или вида (а)(3), если а — составное выражение, где а — функцио- ») См, рассуасаеиие аа с, 30 — 3!. 19" 580 ПРИЛОЖЕНИЕ пу нал, а $ — терм. Функционалом считается всякое выражение вида Л ((8), где ) (х) получается из терма 1(е), содержащего свободную индивидную переменную с и не содержащего связанной индивидной переменной х, в результате замены е посредством х. Элементарными формулами считаются формульные переменные без аргументов, формульные переменные с аргументами, каждый из которых — либо терм, либо функционал, н, кроме того, равенства термов.
Формулами считаются выражения, которые либо являются элементарными формулами, либо получаются иэ элементарных формул при помощи связок исчисления высказываний и кванторов, причем построение формул при помощи кванторов производится следующим образом: если Я (е) — формула, содержащая свободную индивидную переменную е и не содержащая связанной индивидной переменной х, а З (е) -формула, содержащая свободную функциональную переменную е и не содержащая связанной функциональной переменной х, то формулами считаются также выражения УЛИ(8), ВЛЯ(8), УЛЕ(х) и ЖЕ(х). И, наконец, термами (е-термами) мы будем считать также выражения вида е,Я(х), если выполнены условия применимости ь-правила, т.
е. в случае выводимости относящихся к формуле 6(с) формул единственности ЗеЯ(е) и 11ече(6(е) ееИ(ее)-Э.З=й) (о какими-либо связанными индивидными переменными х и э). В качестве исходных формул мы берем тождественно истинные формулы исчисления высказываний, формулы ЧхА (х) -е- А (а), А (а) -+ ЛхА (х), УХА (х) -е- А (а), А (д) ~ БхА (х), аксиомы равенства (),) и (Зе), арифметические аксиомы (Р,) и (Ре) и аксиому индукции, т. е.
аксиомы системы (2), за исключением рекурсивных равенств для сложения и умножения'). В качестве схем вывода мы используем схему заключения и схемы для кванторов Я-~-8(а) И-~.ч)(а) 8(а)-~Я ч)(а)-~-Я И- УЛИ(г) И ИЗ($) ~86(8) Я ЗЛИ(8)- И в которых всюду а — свободная, а х — связанная индивидная переменная, 4 — свободная, а г — связанная функциональная перемене) бм, Приложение 1, е, 488, Е Е1 МОднфИКАцин ФОРМАЛИЗМА ИСКЛЮЧЕНИЕ е-СИМВОЛА 581 ная, причем н не входит ни в 6, ни в И(х), а не входит ии в Я, ни в И(х), х не входит в З(и) и г не входит в 5 (8), К этим схемам мы добавляем, кроме того, схему формул (3 1 (г)) (с) = 1 (с), в которой 1(с) — терм, содержащий переменную е и не содержа- щий связанной переменной х, а также схему е-правила :-)86 И), ~(Ж (Я (8) зе И (р) 8 = 8) 6(е Я" (е)) в которой Яе (х) означает выражение, отличающееся от 6(г) разве лишь именами связанных переменных, причем имена эти должны выбираться таким образом, чтобы выражение И (е И* (г)) было формулой.
Правило подстановки вместо свободных индивидных и вместо формульных переменных такое же, как в формализме Н. Для функциональных переменных здесь мы имеем лишь правило, разрешающее вместо свободных функциональных переменных подставлять функционалы. Правило переименования действует применительно к связанным переменным, относящимся к кванторам, е-символу н е,-символу. Производя подстановки и переименования мы будем следить за тем, чтобы не возникало коллизий между связанными переменными. Правило введения новых символов при помощи явных опред е л е н и й отличается от соответствующего правила в формализме Н .
только тем, что функциональные переменные, входящие в состав вновь вводимого символа в качестве его аргументов, должны фигурировать в нем сами по себе, т. е. без каких бы то ни было аргументов. Тем самым формализм К описан. Сравнивая его с формализмом Н с точки зрения возможности воспроизведения в нем дедунтивных построений, выполнимых в Н, отметим следующие дедуктивные средства, имеющиеся в Н и отсутствующие в К: е-символы вместе с тремя и-формулами для них; подстановку функций вместо свободных функциональных переменных и в явных определениях разрешение наличия аргументов у функциональных переменных, фигурирующих в качестве аргументов вновь вводимых символов (разумеется, при условии, что функциональная переменная, о которой идет речь, нигде в правой части определения не фигурирует сама по себе).
Что касается последних двух имеющихся в Н возможностей, то они компенсируются наличием в К схемы для Х-символа. Действительно, вместо того чтобы перейти от формулы 6(с (ае), ... Еи МОдн«ИКХПИИ «ОРМ«ЛИЗИ«, ИСКЛЮЧЕИИЕ е-СИМВОЛЛ ЗЗЗ пРилОжение пу' ..., с («,)) к формуле Я(1(а<), ..., 1(а„)) путем подстановки вместо именной формы с (а) соответствующей функции 1(а), мы можем в К подставить вместо с функционал Л 1(х) и из формулы Я ((Л,1 (х)) («,), „(Л,1 (х)) (а,)) с помощью схемы для Л-символа н аксиомы равенства ()е) получить формулу Я(1(а,), ..., 1(а,)).
А упоминавшаяся выше свобода в явных определениях формализма Н проявляется, как мы знаем, только при подстановках функций. Пусть, далее, Я(с) — любая формула, для которой в К выводима формула 317«(71(Е (3) = «(1)) Я («)) Тогда образование термов вида е.Я(х) и использование третьей е-формулы с помощью подстановки формулы Я(<) вместо формульной переменной А (Ь) в формализме К может быть заменено вве. деннем получающегося по <-правилу терма <„:-В (Я (х) й х (а) а) (с какой-либо не входящей в Я(<) свободной ннднвидной переменной а) и применением схемы <-правила н схемы для Л-символа. Действительно, если выражение ЗЛ (Я (х) й х (а) а) сокращенно обозначить через З(н, а), то с помощью формулы, выводнмость которой предполагается, могут быть выведены формулы единст.
венности :-)пб(п, а) и ЧЕМ»(6(н, а)йа(», а)-~-и=») (с подходящей связанной переменной»). Поэтому выражение <„6(н, «) может быть введено в качестве терма, н по схеме <-правила мы получим некоторую формулу 6(е(а), а), в которой е(а) представляет собой терм, отличающийся от <„Е(п, а) разве лишь обозначениями связанных переменных. Эта формула 8(е(а), а) имеет вид ЗФ(Я(х) йх(а) =е(а)). Пусть теперь» — какая-либо связанная переменная, не входящая в е(а), н пусть Ь н с — свободные функциональные переменные, не входящие в Я(х).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
