RUS  ENG
Полная версия
ЖУРНАЛЫ // Записки научных семинаров ПОМИ // Архив

Зап. научн. сем. ЛОМИ, 1976, том 60, страницы 93–102 (Mi znsl2073)

Эта публикация цитируется в 2 статьях

Что можно сделать в ПРА

Г. Е. Минц


Аннотация: Пусть $S^+$ обозначает систему $JR\Pi^\circ_2+AC^\circ_1$ классической арифметики 2 порядка, в которой правило индукции разрешается применять лишь к бескванторным формулам и $\Pi^\circ_2$-формулам, не содержащим функциональных переменных, а аксиому свертывания – лишь к $\Pi_1^\circ$-формулам без функциональных переменных. Постулирована также замкнутость рассматриваемого класса функций относительно примитивно рекурсивных операций. Система $S^+$ оказывается достаточно богатой: в ней можно развить теорию рекурсии, элементарный рекурсивный анализ, доказать теорему о непрерывности эффективных операторов, теорему об устранимости сечения из $\omega$-выводов, провести (с незначительными изменениями) обычные аналитические доказательства многих теоретико-числовых теорем, включая асимптотический закон распределения простых чисел. (В заметке описывается формализация в $S^+$ доказательства леммы Кенига о путях в бинарных деревьях и теоремы Геделя о полноте.) С другой стороны, система допускает интерпретацию в примитивно рекурсивной арифметике ПРА. В частности, бескванторные теоремы $S^+$ выводимы в ПРА, а теоремы вида $\forall x\exists yR(x,y)$ c бескванторной формулой $R$ имеют выводимые в ПРА усиления $R(x,\varphi(x))$ с примитивно рекурсивной функцией $\varphi$. Таким образом, подавляющая часть работающего конструктивного анализа может быть развита уже на конечных этажах мажорантной иерархии Н. А. Шанина. Кроме того, имеется чисто механический способ получения элементарных теоретико-числовых доказательств по многим аналитическим доказательствам. Библ. 6 назв.

УДК: 51.01:164


 Англоязычная версия: Journal of Soviet Mathematics, 1980, 14:5, 1487–1492

Реферативные базы данных:


© МИАН, 2024