Конструктивная формализация теоремы Тенненбаума и ее применения

Пусть $\mathrm{HA}$ – формальная система интуиционистской арифметики, $\mathrm{HA}'$ – теория, полученная из нее стандартной процедурой элиминации функциональных символов и заменой $=$ на другой двуместный предикатный символ. Рассматривается теория $\mathrm{HA}^2$ в объединении языков теорий $\mathrm{HA}$ и $\mathrm{HA}'$, постулатами которой являются схемы аксиом и правила вывода интуиционистского исчисления предикатов, аксиомы систем $\mathrm{HA}$ и $\mathrm{HA}'$, аксиомы равенства для предикатных символов, схема аксиом индукции, формальный тезис Чёрча $\mathrm{CT}$ и принцип Маркова $\mathrm{M}$. Путем формализации доказательства теоремы Тенненбаума о несуществовании рекурсивных нестандартных моделей арифметики доказывается, что для любой замкнутой арифметической формулы $F$ в $\mathrm{HA}^2$ выводима эквивалентность $F\equiv F'$, где $F'$ – перевод формулы $F$ в язык системы $\mathrm{HA}'$. Эта теорема находит применения при исследовании логик конструктивных теорий. А именно, пусть $T$ – конструктивная теория, т.е. множество арифметических формул, замкнутое относительно выводимости в $\mathrm{HA}+\mathrm{CT}+\mathrm{M}$, и пусть $L(T)$ – логика этой теории, т.е. множество предикатных формул, все арифметические примеры которых принадлежат $T$. Тогда $T\leqslant_1L(T)$.
Библиогр. 9 назв.