Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 131

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 131)

Формулы г=6 и г=6-+.(Я(г)- Я(6)) имеют порядковые числа, равные О. Поэтому порядковое число формулы Я(г)-~-Я(6) также равно 0 и, следовательно, Я(6) имеет то же самое порядковое число, что и Я(г). Таким образом, в результате этого перехода порядковое число формулы не изменяется. Значит, го же самое будет верно и при нескольких таких переходах — в частности при формализованном вычислении нумерических термов данной формулы. Теперь мы перейдем к доказательству того, что при производстве обеих рассматриваемых нами операций устранения порядковое число вывода уменьшается.

При устранении индукции мы имеем дело с некоторой примыкающей к концевому фрагменту схемой индукции Я (0), Я (с) -и. Я (с') Я (1) в которой с — какая-либо свободная переменная, а 1 в нумерический терм. Все трн формулы этой схемы имеют одну н ту же степень, а потому и одну и ту же высоту. Пусть порядковые числа верхних формул равны а и Ь соответственно. Если значение 1 равно О, то эта схема заменяется формальным переходом от Я(0) к Я(1) при помощи термального равенства 0=1. При этом, как только что было показано, порядковое число формулы не изменяется, и, значит, Я(1), как и Я(0), будет иметь порядковое число а, в то время как в первоначальной схеме индукции порядковое число нижней формулы Я (1) было больше а. Если же 1 имеет отличное от 0 значение в виде некоторой цифры 1', то, устраняя данное применение схемы индукции, мы будем заменять вывод формулы Я (г) -~ Я (г') соответствующими 61б пгиложвннв е11 доказатвльство кальмАРА ему выводами формул 6(0)-» 6(0 ), 6(0 )-~ 6(0 ), ..., Я(1) -~6(1'), получающимися в результате повсеместной подстановки вместо переменной с цифр О, 0', ..., 1.

В этом случае нз заключитель- ' ных формул этих 1' подвыводов и нз формулы 6(0) в результате надлежащего числа применений схемы заключения получается формула Я(1'), от которой с помощью термального равенства .1'=1 можно перейти к формуле 6(1), Прн таком получении формулы 6(1) из формул 6(п) ».6(п') (п О, 0', ..., 1) и равенства 1'=1 (с использованием одной фор- мулы равенства и одной схемы заключения) все формулы, за исключением, может быть, равенства 1'=1, имеют одну н ту же степень.

Поэтому в преобразованном выводе все формулы 6(п)-» -~-6(п') будут иметь ту же самую высоту, что и формула 6(1), а тем самым и ту высоту„которую формулы Я(1) и Я!с)-~6(с') имеют в первоначальном выводе. Отсюда, во-первых, вытекает, что при замене вывода фор- мулы 6(с)-» 6(с') выводами формул И(п)»-6(п') (и О, 0', ..., 1) эти формулы 6(п) »-6(п') получают то же самое порядковое число Ь, которое первоначально получала формула Я (с) -~ 6 (с'), а кроме того, отсюда следует, что в схемах заключения 6 (и), 6 (и) -»- 6 (и') (и=О, 0', ..., 1) И (и') порядковое число нижней формулы 6(п') всякий раз равно нату- ральной сумме Ь и порядкового числа формулы 6(п), так что формуле И(1'), получающейся в конце этих 1 следующих друг,' за другом схем заключения, сопоставляется порядковое число а ~Ь:ФЬЮ...ф Ь, имеющее 1' слагаемых Ь, причем это поряд- ковое число не изменится и при формальном переходе от И(1'), к 6(1).

Таким образом, и формуле 6(1) тоже будет сопоставлено порядковое число а Ьч1 ...ФЬ, а оно, как установлено ранее,,' меньше порядкового числа, соотнесенного нижней формуле 6(!) кашей первоначальной схемы индукции. Таким образом, в резуль-: тате устранения рассматриваемой схемы индукции порядковое..' число формулы 6(1), которая является одной из исходных фор- . мул концевого фрагмента вывода, уменьшится, и это уменьшение распространится по нити вывода, ведущей от формулы 6(1), лежа- щей в концевом фрагменте, к заключительной формуле всего нашего вывода сквозь следующие друг за другом заключения (других схем в концевом фрагменте нет!) вплоть до заключитель- ной формулы.

В самом деле, порядковое число нижней формулы любой схемы заключения получается, как мы помним, из поряд- ковых чисел верхних формул при помощи натурального сумми- рования и, быть может, применения показательной функции, а обе эти функции, как мы в свое время установили, строго монотонны. Итак, в целом в результате применении операции устранения индукции порядковое число заключительной формулы (а значит, и всего вывода) уменьшается. А теперь, прежде чем перейти к операции устранения кван.

тора существования, мы напомним, что, как было отмечено выше, проводимая нами подготовительная операция вычисления значений нумерических термов не меняет порядковых чисел формул вывода. Рассмотрим теперь вопрос о том, как влияет устранение кван- тора существования на порядковое число вывода, к которому предварительно были применены подготовительные операции разделения свободных переменных, исключения излишних свободных переменных, вычисления значений нумерических термов в конце. вом фрагменте и разделения связанных переменных и в котором затем оказались выполненными условия применимости операции устранения квантора существования: т.

е. к концевому фрагменту этого вывода не примыкает ни одна схема индукции„ а кроме того, в нем имеется ветвление. Пусть среди имеющихся ветвле. нии' выделено то, которое на данном этапе должно устраняться в соответствии с нашими соглашениями. Пусть у этого ветвления =)г6(х) представляет собой ту самую формулу, к которой отно.

сится как нижняя формула некоторой (граничащей с концевым фрагментом) схемы 6 (а) -~ Э Зй6 (а) 9 так н некоторая (фигурирующая в качестве исходной формулы этого фрагмента) аксиома для квантора существования 6 (1) Зй6 (й) (с некоторой цифрой 1), выходя из которых, нити вывода, ведущие к заключительной формуле, сливаются в некоторой схеме заключения Ю, Ю-»-ч. причем эта экзистенциальная формула )х6(х) фигурирует в верхних формулах Еб и Ж-~й в качестве молекулы. Пусть в нити вывода, ведущей от нижней формулы ч".

данной схемы к заключительной формуле всего нашего вывода в целом, формула К первая (считая по направлению к заключительной формуле) такая, что высота ее й меньше степени й формулы Зхб(х). Так как 619 618 пеиложянне Фп докАЗАтельство кАльмАРА в концевом фрагменте нет схем вывода, отличных от схем заключения, то формула Й является нижней формулой некоторой схемы заключения 9, й-~ Й В частности, она может совпадать со схемой Согласно выбору Й высота формул е и 9-~й должна равняться по меньшей мере д, и значит, быть больше Ь. Следовательно, эта высота должна совпадать со степенью! формулы е.

Поэтому разность высот у схемы равняется 1-Ь. Пусть порядковые числа верхних формул этой схемы суть р и з. Тогда порядковое число формулы Й будет получаться из натуральной суммы раз в результате (1 — Ь)-кратного применения показательной функции. Пусть результат Ь-кратного применения показательной функции к 0-а-фигуре г обозначается через ехрз(г), так что ехРА (с) = с и ехРьм (с) = в'"зАИ. Тогда порядковое число формулы й в рассматриваемом выводе изобразится посредством ехр~ А (р Ф Ч).

Операция устранения квантора существования, как известно, заключается в том, что сначала строятся два подвывода, которые дают формулы 6О)- й и '16О) Й а затем из них по правилам логики высказываний выводится формула Й, начиная с которой вывод протекает так же, как н раньше. Посмотрим сначала, каковы высоты формул 6 О)-+ й и )6О)-~й в модифицированном выводе.

Все формулы, участвующие в получении Й из двух указанных выше формул (схема заключения применяется дважды), быть может, вплоть до самой формулы Й, имеют высоту а — 1, которая, как мы знаем, является степенью формулы 6О), (Высота Ь формулы й не превосходит К вЂ” 1.) Поэтому равность высот может быть отлична от нуля только во второй схеме заключении, где она равна б=й — 1 — Ь (д) О). А теперь посмотрим, какие порядковые числа получают заключительные формулы этих двух подвыводов. Для этого мы должны будем исследовать высоты формул нашего вывода.

В первом подвыводе мы сначала получаем формулу 6 О)-~ Е, заменяя в первоначальном выводе формул 6 (а) -+.Е переменную а всюду, где она входит, цифрой 1. Затем от формулы 6 О)-+ 9 мы по правилам исчисления высказываний переходим к формуле 6О)-~-(Згб(г)-~-Е). Так к формуле Зу6(е)-эапервоначального вывода импликативно добавляется посылка 6 О), и эта посылка распространяется дальше по нити, идущей от этой формулы к формуле Й, что, как мы указывали, совершается при помощи надлежащей модификации схем заключения. Прн этом каждая схема заключения заменяется двумя, идущими друг за другом, с привлечением формул, истинных в логике высказываний. В частности, так на месте схемы й, М-+Й й первоначального вывода в зависимости от того, через какую формулу идет рассматриваемая нить вывода, через 2 или через 9-+ й получаются либо схемы 6(1)- й, (6О)- И- (Ф- й)-.(6О)- й)) 2 -~ й, (2 - й) -+ (6 О) -~ й) 6О)- й либо схемы 6 О) (й й) (6 О) Р й)) (2 (6 О) й)) й- (6О)- Й) 6О) й Здесь в обоих случаях нижняя формула имеет высоту К вЂ” 1, тогда как остальные формулы в качестве высоты имеют степень 1 формулы й, которая не меньше д.

Это справедливо, в частности, и в отношении формулы 6О) — 2 илн соответственно формулы 6 О)-~-(е-. Й). Следовательно, в переработанном выводе эта формула будет иметь ту же самую высоту, что и соответствующая ей формула 2 (соответственно 2-~К) первоначального вывода. Отсюда, далее, получается, что при возвращении от этой формулы к формуле 6 О) -~ (Зрб (р) -~ й) соответствующие друг другу формулы модифицированного и первоначального выводов имеют одну и ту же высоту. А кроме того, при получении формулы 6 О)-~Е формулы модифицированного вывода имеют ту же самую пРиложение 621 докАЕАтельство кАльмАРА )и высоту, что и соответствующие им формулы первоначального вывода формулы 5 (а) -~Е.

Характеристики

Список файлов книги