Замечание об усилении гипотезы Г. Крайзеля

Г. Крайзель в конце 60-тых годов предположил, что в формальной арифметике допустимо правило бесконечной индукции, если длины доказательств его посылок равномерно ограничены одним и тем же числом. Длиной доказательства называется число применений в нем аксиом и правил вывода. В статье построена теория $\mathbb{R}^*$ с конечным числом специфических аксиом. В языке $\mathbb{R}^*$ содержится константа $O$, одноместный функциональный знак $'$, равенство и трехместные предикаты сложения и умножения. Доказано, что для любого непротиворечивого аксиоматизируемого расширения $\mathfrak{A}$ теории $\mathbb{R}^*$ можно указать формулу $A(a)$, удовлетворяющую условиям: а) $\forall x\, A(x)$ не выводимо в $\mathfrak{A}$; б) для любого $n$ длина доказательства формулы $A(O^{(n)})$ не превосходит $c_1[\log_2(n+1)]+c_2$, где константы $c_1$ и $c_2$ не зависят от $n$. Здесь выражение $O^{(n)}$ обозначает $O$ с $n$ штрихами. Библ. – 11 назв.