Cтраница 4
На основании этого результата и со ссылкой на одно проведенное в гл. Действительно, для этого достаточно показать что в любом выводе нумерической формулы, осуществляемом средствами рассмотренного формализма с добавлением ограниченной схемы индукции, после исключения формульных переменных результирующие формулы всех применений схемы индукции являются верифицируемыми. [46]
Эта непротиворечивость доказывается с помощью теоремы, аналогичной теореме 51 ( Ь) ( Гильберт - Бернайс [ 1939, сноска на стр. При наличии формулы - i а 0гэ ( pd ( a)) а1), вытекающей из рекурсивных равенств для pd ( a) ( см. § 45, ф5), е-формулы позволяют заменить схему индукции схемой А ( а) Э - iexA ( x) a ( Гильберт - Бернайс [ 1939, стр. [47]
Действительно, если бы нам удалось произвести соответствующее обобщение, то тем самым мы получили бы способ, который позволял бы исключить из вывода любой формулы, не содержащей связанных переменных, не только связанные переменные, но и применения схемы индукции. [48]
Теперь допустим, что из этого вывода можно так устранить применение схемы индукции, что вместо нее всякий раз будут применяться только формулы ( J2) и а Ф 0 - - 6 ( а) а Тогда мы получим вывод формулы й Фа из указанных двух аксиом Пеано в рамках одного только элементарного исчисления со свободными переменными. [49]