Cтраница 3
Теперь рассмотрим общий случай и покажем, что, отправляясь от любого, построенного в соответствии с нашими правилами вывода, после конечного числа применений операции устранения индукции и квантора существования мы придем к такому выводу, в котором ни одна схема индукции не будет примыкать к концевому фрагменту, а в самом этом фрагменте - после вычисления нумерических термов и разделения связанных переменных - будут отсутствовать ветвления. [31]
Совершенно не ясно, как в этом случае добиться того, чтобы ни одна из посылок критических формул - в том виде, как они будут выглядеть после выполнения операции возвратного переноса подстановок, - не содержала выделенной переменной какой-либо из схем индукции. [32]
Возникает естественный вопрос о том, можно ли нашу процедуру устранения е-символов, с помощью которой сначала была доказана первая е-теорема, а затем, с использованием этой теоремы, и нп-теорема, модифицировать таким образом, чтобы видоизмененная процедура была применимой и при добавлении к формализму неограниченной схемы индукции. [33]
Аналогичным образом можно убедиться, что предположение б2) и добавляемые к нему условия на выводимость выполняются также и для всех таких формализмов, которые, с одной стороны, очерчены достаточно четко, а с другой стороны, включают в себя способы умозаключений исчисления предикатов и обладают средствами, достаточными для изображения понятий и способов умозаключений арифметики, так что в них, в частности, изобразимы рекурсивные функции и соответствующие рекурсивные равенства являются либо аксиомами, либо выводимыми формулами, а кроме того, содержится ( в качестве основного правила или производной схемы) схема индукции. Поэтому ко всем таким формализмам применима вторая теорема Геделя о неполноте. [34]
В нашей схеме индукции слова имеет место нельзя интерпретировать как является общезначимым. Действительно, формализованная арифметика не является максимальной теорией, а поэтому у нее нет адекватных семантических моделей ( см. 12.3 и стр. [35]
Аксиомы As включают эту схему индукции, 0 0 и uOV 0 Так как QH ( xlt х2, хг х2 является логическим следствием конъюнкции Apf Asf A, мы заключаем, что программа остановится для xz, больших 0, и когда она остановится, ее выходом будет х1 - - хг. [36]
В системе FA арифметики формальной схема индукции состоит лишь из тех И. [37]
IV с тем ограничением, наложенным на схему индукции, что в А ( х) переменная х не входит свободно в область действия какого-нибудь квантора, просто непротиворечива. Аккерман [1924 - 26], Нейман [ 19271; см. Тильберт я Бер-найс [ 1939, стр. [38]
При таком распределении истинностных значений постоянных элементарных формул все аксиомы системы ( Z), как легко убедиться1), оказываются верифицируемыми формулами. Поэтому для системы ( Z) при условии исключения из нее схемы индукции будут справедливы все утверждения нашей нп-теоремы и, в частности, утверждение о том, что всякая выводимая формула, не содержащая ни связанных индивидных, ни формульных переменных, является верифицируемой. [39]
Во-первых, мы будем рассматривать выводы, в которых нет примыкающих к их концевым фрагментам применений схемы индукции и в которых уже произведено вычисление значений нумерических термов и разделение связанных переменных. Ввиду того, что связанные переменные нами разделены, это может иметь место только тогда, когда в данном выводе эти два вхождения данной экзистенциальной формулы связаны друг с другом. В этом случае должно иметь место некоторое ветвление ( в указанном ниже смысле слова): нить вывода, выходящая из этой аксиомы для квантора существования ( в направлении к заключительной формуле), и нить, ведущая от нижней формулы рассматриваемой схемы вывода для квантора существования к заключительной формуле, должны сходиться к посылкам некоторой схемы заключения. В верхних формулах этой схемы упомянутая экзистенциальная формула должна фигурировать в качестве молекулы, а в нижнюю формулу она может и не рходить. [40]
А теперь, прежде чем приступить к доказательству того, что операции устранения квантора существования и индукции в определенном смысле дают действительные упрощения, мы должны еще рассмотреть случай, когда к концевому фрагменту вывода не примыкает ни одна схема индукции, а также не выполнено и предварительное условие проведения операции устранения квантора существования. В этом глучае у нас имеется фигура вывода, в которой к концевому фрагменту не примыкает ни одна схема индукции, а в самом этом фрагменте после вычисления нумери-ческих термов и разделения связанных переменных любая экзистенциальная формула, к которой относится какая-либо аксиома для квантора существования, отлична от всех экзистенциальных формул, к которым относятся какие-либо ( граничащие с концевым фрагментом) схемы для квантора существования. Заметим также, что в соответствии о нашими соглашениями, касающимися разделения связанных переменных, эта операция делает различными только такие формулы, которые нигде внутри рассматриваемого нами концевого фрагмента ( где имеются лишь формулы, истинные в логике высказываний, и схемы заключения) не играют роли одной общей молекулы. [41]
На основании этого результата и со ссылкой на одно проведенное в гл. Действительно, для этого достаточно показать что в любом выводе нумерической формулы, осуществляемом средствами рассмотренного формализма с добавлением ограниченной схемы индукции, после исключения формульных переменных результирующие формулы всех применений схемы индукции являются верифицируемыми. [42]
Логический формализм, лежащий в основе рекурсивной арифметики, представляет собой элементарное исчисление со свободными переменными. К нему в качестве исходных формул добавляются аксиомы равенства и формула О Ф О, а в качестве схем - схема индукции и схема примитивной рекурсии. Средств этого формализма уже достаточно для того, чтобы с их помощью можно было изобразить различные понятия, утверждения и доказательства элементарной арифметики. С другой стороны, этот формализм еще допускает определенное финитное истолкование. Но и без прямого обращения к этому истолкованию мы легко смогли доказать непротиворечивость этого формализма и даже установить, что всякая выводимая в нем формула, не содержащая формульных переменных, при любой замене входящих в нее свободных индивидных переменных цифрами после вычисления значений соответствующих функций переходит в истинную формулу. [43]
Далее, мы выяснили, что к этому формализму, не нарушая применимости нп-теоремы, можно добавить: 1) схему индукции для формул без связанных переменных, 2) схемы рекурсий рекурсивной арифметики и 3) аксиомы равенства для любой вновь вводимой функции. [44]
Во-первых, при добавлении схемы индукции возникают трудности с выполнением одной из операций, подготавливающих процедуру устранения е-символов. Именно, после возвратного переноса подстановок в исходные формулы нельзя будет произвести полное исключение свободных переменных, так как в результате этой операции схемы индукции теряют свой вид. [45]