Cтраница 1
Схема индукции получается из аксиомы индукции в качестве производного правила. [1]
I обобщения схемы индукции, дающие частичную компенсацию за ограничения, наложенные на эту схему, тоже согласуются с нашей нп-теоремой, потому что они, как мы уже установили1), сводятся при помощи примитивных рекурсий к обычной схеме индукции нашей рекурсивной арифметики. [2]
Нижние формулы схем индукции нам рассматривать не нужно, так как операцию вычисления значений термов мы применяем только к таким выводам, в которых нет применений схемы индукции, примыкающих к концевому фрагменту. [3]
Остается проверить схему индукции и принцип ЕСТ. [4]
Если же схему индукции опустить, то, как легко убедиться, нп-теорема становится применимой. Действительно, постоянные элементарные формулы системы ( Z) представляют собой равенства между постоянными термами. Но эти термы либо сами являются цифрами, либо строятся из цифр с помощью знаков сложения и умножения. Как известно, для таких термов имеется процедура рекурсивного вычисления их значений ( она основывается на использовании рекурсивных равенств для сложения и умножения в качестве финитно понимаемых инструкций для выполнения соответствующих действий) и эта процедура всегда дает в качестве значения такого терма некоторую цифру. [5]
Аналогия между схемой индукции для высказываний ( определение 1.2.2) и схемой индукции для семантических таблиц очевидна. [6]
Следовательно, применение схемы индукции во всяком таком доказательстве равносильно добавлению к аксиомам системы ( Z) некоторого числа верифицируемых формул. Отсюда, согласно сделанному выше замечанию, получается, что если в рассматриваемый формализм включить аксиому индукции, применяемую к формулам без связанных переменных, то условия применимости нп-теоремы к этому формализму будут выполнены. [7]
Остается только вывести схему индукции и аксиому равенства / 2 - Это сделано ниже соответственно в 7 2 и 7.4. Окончательный результат заключается в 7.6. 7.1. Теорема. [8]
Как мы помним, схема индукции в формализме ( Z) является производной. [9]
Во-первых, при добавлении схемы индукции возникают трудности с выполнением одной из операций, подготавливающих процедуру устранения е-символов. Именно, после возвратного переноса подстановок в исходные формулы нельзя будет произвести полное исключение свободных переменных, так как в результате этой операции схемы индукции теряют свой вид. [10]
Теперь мы переходим к некоторым схемам индукции. [11]
При замене выделенной переменной каким-либо постоянным термом схема индукции в любом случае теряет свой вид. Поэтому исключение свободных переменных с сохранением структуры доказательства может быть произведено только в отношении формульных, но никак не индивидных переменных. [12]
Это обстоятельство позволяет включить в наш результат схему индукции - по крайней мере частично, а именно при условии, что эта схема будет применяться лишь к формулам без связанных переменных. В самом деле, чтобы убедиться в этом, нам достаточно повторить рассуждение, проведенное в гл. [13]
Причины, препятствующие распространению процедуры устранения е-символов на неограниченную схему индукции. [14]
Причины, препятствующие распространению процедуры устранения е-символов на неограниченную схему индукции. [15]