Cтраница 2
Ко всему этому добавляется еще одна арифметическая схема - схема индукции. [16]
Из рекурсивных равенств для а - - Ь, пользуясь схемой индукции, мы получаем формулы, изображающие обычные законы, которым подчиняется операция сложения. [17]
Добавив к элементарному исчислению со свободными переменными схему примитивной рекурсии и схему индукции вместе с аксиомами равенства и аксиомой 0 О, мы получим формализм рекурсивной арифметики. [18]
Аналогия между схемой индукции для высказываний ( определение 1.2.2) и схемой индукции для семантических таблиц очевидна. [19]
А для случая, когда к рассматриваемому концевому фрагменту не примыкает ни одно применение схемы индукции, мы определим некоторую другую операцию - операцию устранения квантора существования. Она будет применяться при соблюдении некоторых дополнительных условий, которые еще должны быть сформулированы. [20]
Иногда в наших доказательствах непротиворечивости используется один вид полной индукции, который не формализуется схемой индукции рекурсивной арифметики. Этот выход за рамки рекурсивной арифметики связан с тем, что в наших формулировках и доказательствах время от времени встречаются такие допущения, в которых говорится об истинности некоторых всеобщих предложений; таковы, например, предположение о невыводимости или о неопровержимости какой-либо формулы, или предположение о непротиворечивости какого-либо формализма, или же предположение о верифицируемоети какой-либо формулы, что, согласно определению, означает, что эта формула при любой замене свободных переменных цифрами оказывается истинной. Любое высказывание, содержащее такого рода предположение, представляет трудности и для финитного понимания. Как известно, финитное допущение всегда относится к какой-либо наглядно характеризуемой ситуации. Но истинность всеобщего предложения не может считаться таковой. Правда, вместо предположения, что рассматриваемое всеобщее предложение истинно, можно взять предположение о том, что истинность этого предложения установлена. [21]
Тем самым установлена непротиворечивость той части формализма ( Z), которая получается путам ограничения схемы индукции такими формулами Я ( с), в которых переменная с не попадает в область действия каких-либо кванторов или к символов. [22]
Все такие доказательства непротиворечивости, полученные строго элементарными методами, должны остановиться перед непротиворечивостью арифметического формализма с неограниченной схемой индукции, как это вытекает из знаменитой Второй теоремы Геделя 11931, теорема 30 § 42 ], согласно которой непротиворечивость этой системы не может быть установлена методами, формализуемыми в ней самой. [23]
Никаких трудностей в доказательстве не возникает и в том случае, если мы дополним данный формализм некоторыми естественными обобщениями схем индукции и рекурсии в том виде, как они были рассмотрены нами в гл. [24]
Нижние формулы схем индукции нам рассматривать не нужно, так как операцию вычисления значений термов мы применяем только к таким выводам, в которых нет применений схемы индукции, примыкающих к концевому фрагменту. [25]
И все-таки эта формула вместе с формулой lndx ( A ( x), 0) еще не позволяет применить в рамках формализма ( Z) схему индукции. [26]
В системе теоремы 55 класс доказуемых формул ( или формул, выводимых из данных исходных формул) не уменьшится, если наложить на А ( х) схемы индукции дальнейшее ограничение, состоящее в том, чтобы А ( х) вовсе не содержала кванторов. [27]
Если мы теперь зададимся вопросом о том, может ли система ( Z) служить объектом применения нашей нп-теоремы, то обнаружим, что из-за наличия в ( Z) схемы индукции применение этой теоремы ( во всяком случае, прямое) оказывается невозможным. Аксиома индукции, естественно, приводит к тем же самым трудностям, так как она не является собственной аксиомой. [28]
Тем самым мы попадаем в сферу действия того арифметического формализма, который получается из рекурсивной арифметики в результате присоединения исчисления предикатов ( в полном объеме), а также распространения на расширенную область формул схемы индукции и добавления ц-символа с относящимися к нему формулами ( iij), ( ц2) и ( мз) 2) - Этот формализм равносилен рассмотренному в гл. [29]
А теперь, прежде чем приступить к доказательству того, что операции устранения квантора существования и индукции в определенном смысле дают действительные упрощения, мы должны еще рассмотреть случай, когда к концевому фрагменту вывода не примыкает ни одна схема индукции, а также не выполнено и предварительное условие проведения операции устранения квантора существования. В этом глучае у нас имеется фигура вывода, в которой к концевому фрагменту не примыкает ни одна схема индукции, а в самом этом фрагменте после вычисления нумери-ческих термов и разделения связанных переменных любая экзистенциальная формула, к которой относится какая-либо аксиома для квантора существования, отлична от всех экзистенциальных формул, к которым относятся какие-либо ( граничащие с концевым фрагментом) схемы для квантора существования. Заметим также, что в соответствии о нашими соглашениями, касающимися разделения связанных переменных, эта операция делает различными только такие формулы, которые нигде внутри рассматриваемого нами концевого фрагмента ( где имеются лишь формулы, истинные в логике высказываний, и схемы заключения) не играют роли одной общей молекулы. [30]