Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 118
Текст из файла (страница 118)
По ряду соображений, связанных с дедуктивной целесообРазностью, мы добавим к Йв схемУ Явного опРеделения. ') Этв схема формул предложена дж. фое Неймвеом в вго работе: )Че в'"вео 3. у. ьос НцЬсг)всЬсо Веже!З)Ьеог!е.— Мвйь Е„1927, 28, Б. 18. 661 ПОСТРОЕНИЕ АРИФМЕТИКИ ПРИЛОЖЕНИЕ а 21 пу Всякое явное определение представляет собой формулу одного из следующих трех видов: 6=1, ( (с) = й (с), ® здесь 1 — терм, й — функционал, с — свободная индивидная пере-, менная, ч.— формула, а б, ! и ьз — выражения, состоящие из вновь вводимого символа и его аргументов.
При этом в обеих' частях соответствующего равенства или эквивалентности должны. фигурировать одни и те же свободные переменные. Аргументные места формульных переменных, фигурирующих в качестве аргументов вновь вводимых символов, указываются путем заполнения связанными индивидными или соответственно функциональными' переменными; аргументное место фигурирующей в качестве аргу-. мента функциональной переменной а во вновь вводимом символе„ указывается только тогда, когда в правой части определения; переменная и не фигурирует сама по себе, но н в этом случае' это аргументное место можно не указывать.
Связанные переменные, используемые для указания аргументных мест аргументов вновь вводимых символов, должны быть попарно различны; по-' мимо соответствующих аргументных мест, они записываются иг у самого этого символа — в качестве индексов или каким-нибудь, другим образом. Схема явного определения представляет собой пра. вила, согласно которому любое явное определение может быть", добавлено к формализму в качестве исходной формулы, причем выражение, состоящее из введенного символа и его аргументов,. а также любое выражение, получающееся из него в результате каких-либо подстановок вместо его свободных переменных (если ' при этом не происходит коллизий между связанными переменными), .
допускается в качестве терма, или функционала, или формулы, смотря по тому, какой — первый, второй или третий — вид имеет это явное определение. Разумеется, правило переименования свя* ванных переменных распространяется и на связанные переменные ' вновь введенных символов. Присоединение этой схемы к формализму Н, дает нам новый ' формализм, который мы будем называть формализмом Н. При, исследовании вопроса о непротиворечивости Н формализм этот' с помощью общего метода исключения явных определений можег;; быть сведен к формализму Н,.
В самом деле, наши соглашения.'': касающиеся внешнего вида явных определений, выбраны с таким' расчетом, чтобы этот метод оказался применимым '). В Особого рассмотрения требует случай, когда вновь вводимый символ .' нмеетодну нлн несколько функцнональных переменных в качестве аргументов.' а 2. Построение арифметики д теперь мы вкратце покажем, как из формализма Н могут быть полУчены исчисление пРедикатов, аРифметика и анализ. Сначала при помощи явных определений ь»'хА (х) А (е„) А (х)), ЭхА (х) А (Е„А (х)), ь»хА(х) А(е; 1А(х)), ЭхА (х) А(а;А (х)) могут быть введены кванторы.
Из этих определений в сочетании с первой и третьей а-формулами основные формулы (а) и (Ь) исчисления предикатов могут быть получены в качестве выводимых формул, а схемы (сс) н (р) — в качестве производных правил') (причем в отдельности для индивидных и для функциональных переменных). С помощью первой и второй а-формул, аксиомы равенства ()2), третьей арифметической аксиомы и средств исчисления высказываний схема индукции, как мы знаем, может быть получена в качестве пронзводнои схемы' ), а с помощью схемы индукции в сочетании с формулой (а) и аппаратом исчисления высказываний может быть выведена аксиома индукции'). С помощью соответствующих явных определений могут быть введены и обычные символы для чисел.
Теперь, чтобы в нашем распоряжении оказался весь формализм арифметики, нам достаточно получить схему рекурсивного определения. На самом деле примитивные рекурсии (как, впрочем, и более общие схемы рекурсии) в формализме Н могут быть полностью сведены к явным определениям. Причем это можно сделать единым приемом, путем указания одной универсальной для рекурсивных функций функции, из которой отдельные рекурсивные функции получаются соответствующими подстановками. Метод построения этой функции можно было бы оформить и несколько проще, если бы в нашем формализме имелись функциональные переменные с двумя аргументами.
Но так как в Н мы их не ввели, то нам придется сначала формально построить отображение числовых пар на числа. Требующиеся для этого Рекурсивные функции можно получить при помощи следующих явных определений: сначала с помощью равенства +ь-Р. !»»ьь= ьч*»»ь ь-»»*ь'ы)ььь > с. ) Сн с !17 119 ") См. т. 1, с. 397. ПОСТРОЕНИЕ АРИФМЕТИКИ ПРИЛОЖЕНИЕ 11тг мы определяем сложение. Из этого равенства могут быть выведены рекурсивные равенства а+О=а н а+Ь'=(а+Ь)'.
Их вывод может быть построен с помощью формулы Зх(х(0)=айг'чг(х(г') =х(г)')), которая получается применением схемы индукции по отношению к переменной а (индукцией по а). Вывод посылок Я(0) и л(а)-~Я(а') данной схемы индукции производится с помощью формул Эхтг(х(г) =г) и =(хааа(х(г) =с(г)'), получающихся с помощью выводимых формул Уг(г=г) и А (а) Р -"$хА (х) и правила подстановки функций т). Из рекурсивных равенств для а+Ь, пользуясь схемой индукции, мы получаем формулы, изображающие обычные законы, которым подчиняется операция сложения. Воспользовавшись сложением и взяв явные определения а(Ь Чх(а~й+х) и а(Ь 3Х(а+Х=Ь), можно ввести предикатные символы «с.» и «~».
Из этих определений могут быть выведены формулы 1(а(а), а<ЬЕЬ<с- а:,с, а~Ь ~/ Ь(а, а(Ь а=Ь Ч а(Ь, а(а', а С.Ь' а~Ь. Аналогично сложению, равенством а Ь=(е„(х(0)=Обгьтгг(х(г') Я(г)+а)))(Ь) мы определим умножение. Из этого равенства могут быть выведены рекурсивные равенства а0=0 и аЬ' аЬ+а. Вывод их производитая с помощью формулы :-1х(й(0) =Ой 'й(й(г') й(г)+а)), ') .Возможность такого введения сложения н аналогичная возможность для умножения была впервые установлена Л. Кальмаром.
В этом методе, допускаююем н непосредственную содержательную ннтернретвцню, существенно то, что индуктивное рзссужденне, нз которого получвется рвзрешнмость втнк рекурсивных равенств прн номоцю некоторой двуместной функции, проводится не по той переменной, по которой пронзводнтся рекурсия, е по параметру рекурсии. которая опять-таки может быть выведена индукцией по а с нс. пользованием выводимых формул ') Бх'Фг (х (г) = 0) с(0) = Ой Уг(с(г') =с(г)+а)-Р с(0)+0=01 Чг(с(г) + г'=(с(г)+г\+ а).
Из рекурсивных равенств для а Ь можно получить формулы, выражающие обычные законы, которым подчиняется умножение, а также формулу а (Ь+с) =а. Ь+а.с, А теперь мы введем функцию с(п)=е,(х+х=п и'). Индукцией по и легко получается формула Вх(х+х=п и'), из которой можно сначала вывести равенство $ (и) + $ (и) = и и', а затем и формулы й(0)=0 и $(и')=$(п)+и'. Зти формулы вместе с рекурсивными равенствами для сложения составляют рекурсивное определение функции $(и). Далее, если с помощью равенства т(а, Ь) =$(а+Ь)+а определить функцию т(а, Ь), то для нее можно будет вывести равенства т(0, 0) =О, т(0, а') =т(а, О)', т(а', Ь) =т(а, Ь')', из которых индукцней по п получается формула ВХЗу(т(х, у) =п).
Кроме того, можно будет получить формулу а+Ь(с+с(-ьт(а, Ь) .-т(с гй ') Вывод первой нз этих формул, например, может быть получен с нспользоввннем равенстве е (в=лаз=а)=0. ПРИЛОЖЕНИЕ ПОСТРОЕНИЕ АРИФМЕТИКИ !ди а с ее помощью — формулу т(а, Ь)=т(с, а)-~а=сйЬ=е(. Если теперь с помощью явных определений т,(л)=а Зу(т(х, у)=л) 'еа(л) = ив-1х(т(х, у) =л) т,(л) и т,(л), ввести функции ня(а, Ь)=а ((аФЬ вЂ” ь.х=О)й(а=Ь х 0)) мы вводим функции а(а, Ь) и р(а, Ь). Из этих определений легко могут быть выведены формулы а = Ь -д-ех (а, Ь) = О, а Ф Ь -д- а (а, Ь) = 0', а~Ь-+ р(а, Ь)=0, а=Ь-т 11(а, Ь)=0'.
Используя эти формулы, мы получим формулу (2) с (0) = а й Уг [г:, л -Р с (г') = Ь (т (г, с (г)))1 й 7г(д(г) =с(г) а(г, л')+Ь(т(л, с(л))) и (г, л'))-э. д (0) = а й де г 1г( л' -+ д (г') = Ь (т (г, у (г)))1, ') Метод проведения данного вывода восходит к дедекинду. См, его книгу: 0 е д е К ! и о Ге. %ая а!по ппо «'аа ао1!еп о!е кашен? — Вг Ь 1887, $9. — аипас дте!К, то с помощью полученных формул можно будет вывести равенства т(т,(л), т,(л))=л, т,(т(а, Ь))=а, т,(т(а, Ь))=Ь. Т ем самым мы получаем формализацию некоторого конкретного взаимно однозначного отображения числовых пар на числа.
Теперь мы продвинулись настолько, что можем построить упоминавшуюся уже универсальную для рекурсивных функций функцию. Явное определение этой функции записывается в виде р„(а, Ь(х), гд) =[а [х(0) =ай дгг[х(г') =Ь(т(г, х(г)))1Ц(л). Чтобы получить из него равенства, характеризующие эту функцию, мы выведем формулу (1) :-1х [х(0) = ай д!Ег[х(г') =Ь(т(г, х(г)))1). Наметим вкратце ход этого выводад). Сначала явными определениями а(а, Ь)=а„((а=Ь-эх=0)й(ачьЬ-~-х=О')) и затем с помощью этой формулы и легко выводимой формулы :-1х (У (0) а) индукцией по л мы получим формулу Зх [х(0) =ай дтг[г~л-+ х(г') =Ь(т(г, х(г)))Ц, а из нее — формулу (3) (е (л)) (0) = а й ддгг [г (л-+.
(е (л)) (г) = Ь (т (г, (е (л)) (г)))1, где е(л) представляет собой функционал е;[х(0)=айдгг[гс л-+ х(г')=Ь(т(г, х(г)))Ц. Но нз (3) с использованием формулы й(л-т.(е(л'))(й) =(е(л))(й), которая выводится индукцией по л, можно получить формулу (е (О)) (0) = а й (е (л')) (л') = Ь (т (л, (е (л)) (л))), а из нее формулу (1), После того, как формула (1) выведена, мы из явного определения функции р (а, Ь(х), л) получаем равенства р (а, Ь(х), 0)=а, р„(а, Ь(х), л')=Ь(т(л, р„(а, Ь(х), л)). На основании этих равенств любое определение функции при помощи примитивной рекурсии [(ад, ..., а„О) =о (ад, ..., а„), ((ад, ..., а„л') =Ь(а„..., а„, л, [(а„..., а„л)) может быть сведено к соответствующей подстановке в функцию Ря(а, Ь(х), л). Действительно, достаточно сформулировать явное определение 1(а„ ..., а„ л) = р, (о (а„ ..., а,), Ь (аы , , а„ т, (х), е, (х)), л), и тогда оба эти рекурсивных равенства окажутся выводимыми формулами.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
