Эта публикация цитируется в
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