Cтраница 2
Гудстейн в предисловии к монографии РА утверждает, что рекурсивный анализ ( так он называет разрабатываемый им вариант конструктивного математического анализа) формализуем в исчислении равенств, однако нигде в тексте РА не поясняет, какой смысл он вкладывает здесь в термин формализация. Конкретный материал, содержащийся в РА, свидетельствует о том, что это утверждение Гудстейна нельзя понимать в том смысле, что все теоремы рекурсивного анализа допускают запись в виде равенств и эти равенства выводимы в исчислении равенств. [16]
Там нет никаких аксиом, кроме равенств, вводящих функциональные знаки, и нет никакого обращения к логике, причем работа системы определяется просто правилами преобразования для математических знаков. Показывается, что некоторая часть логики определима в исчислении равенств, а логические знаки и теоремы вводятся как удобные сокращения для некоторых функций и формул. [17]
Имеется несколько систем конструктивной теории функций; некоторые из них, как, например, интуиционистский анализ, основаны на новой логике, другие изучают конструктивные объекты, например, рекурсивные вещественные числа, методами классического анализа, а третьи пытаются выразить с помощью функционалов часть классического анализа в виде формул со свободными переменными. Система, описанная в этой книге, отличается от всех этих систем. Она основана на примитивно рекурсивной арифметике, и в ней делается попытка построить теорию функций в поле рациональны чисел, напоминающую в одних отношениях классический анализ, а в других - интуиционистский анализ. Все доказательства в рекурсивном анализе формализуемы в исчислении равенств) - системе рекурсивной арифметики, описанной в моей книге Рекурсивная теория чисел, но настоящую работу можно читать без детального знания рекурсивной арифметики. [18]