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

Пусть $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 назв.