Cтраница 4
S - таким образом, что выводимость в S суждения УхЗуЯ ( х, у) с бескванторной формулой Н влечет выводимость в S - формулы R ( х, f ( x)) для подходящего ср. Если S - арифметика без индукции, то S - примитивно рекурсивная арифметика; если S - гейтннговская арифметика, то S - - система геделев-ских примитивно рекурсивных функционалов. [46]
Возвращаясь к примитивно рекурсивным функциям, заметим, что о многих определяющих схемах, которые по виду очень отличны от примитивной рекурсии, известно, что они определяют только примитивно рекурсивные функции. Различные виды рекурсивных определений приведены в книге автора Рекурсивная теория чисел, где показано, что рекурсивную арифметику можно формализовать в системе, в которой доказуемы аксиомы исчисления высказываний и все перечисленные выше схемы вывода. [47]
Можно считать, что надежный финитный смысл могут иметь только арифметические суждения ограниченной сложности. Особенно интересно рассмотреть здесь крайний случай, когда приемлемыми считаются лишь бескванторные арифметические формулы. В качестве формальной теории тогда следует рассмотреть теорию PRA - примитивно рекурсивную арифметику, бескванторный фрагмент теории НА. С другой стороны, можно пытаться расширять НА, сохраняя ее финитный и нейтральный характер, например, таким образом, чтобы иметь возможность вывести непротиворечивость НА в расширенной теории. Однако в этом параграфе мы будем считать базисными именно выводы в НА, отождествляя такие выводы с финитными выводами. [48]
Имеется несколько систем конструктивной теории функций; некоторые из них, как, например, интуиционистский анализ, основаны на новой логике, другие изучают конструктивные объекты, например, рекурсивные вещественные числа, методами классического анализа, а третьи пытаются выразить с помощью функционалов часть классического анализа в виде формул со свободными переменными. Система, описанная в этой книге, отличается от всех этих систем. Она основана на примитивно рекурсивной арифметике, и в ней делается попытка построить теорию функций в поле рациональны чисел, напоминающую в одних отношениях классический анализ, а в других - интуиционистский анализ. Все доказательства в рекурсивном анализе формализуемы в исчислении равенств) - системе рекурсивной арифметики, описанной в моей книге Рекурсивная теория чисел, но настоящую работу можно читать без детального знания рекурсивной арифметики. [49]
Имеется несколько систем конструктивной теории функций; некоторые из них, как, например, интуиционистский анализ, основаны на новой логике, другие изучают конструктивные объекты, например, рекурсивные вещественные числа, методами классического анализа, а третьи пытаются выразить с помощью функционалов часть классического анализа в виде формул со свободными переменными. Система, описанная в этой книге, отличается от всех этих систем. Она основана на примитивно рекурсивной арифметике, и в ней делается попытка построить теорию функций в поле рациональны чисел, напоминающую в одних отношениях классический анализ, а в других - интуиционистский анализ. Все доказательства в рекурсивном анализе формализуемы в исчислении равенств) - системе рекурсивной арифметики, описанной в моей книге Рекурсивная теория чисел, но настоящую работу можно читать без детального знания рекурсивной арифметики. [50]