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