A note on a extension of Kreisel's conjecture

V. P. Orevkov

Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part 4, Tome 176 (1989), pp. 118-126

Résumé

Given a theory $\mathfrak{R}$, let $\mathfrak{R}\vdash_lA$ means that $A$ is provable in $\mathfrak{R}$ in $l$ steps. Let $L^*$ be the first order language with a constant symbol $O$, a unary function symbol $'$, a binary predicate symbol $=$, ternary predicate symbols $P$ and $Q$. The theory in $L^*$ with the axioms $\mathbb{R}^*.1$–$\mathbb{R}^*.13$ defined in §1 of this paper is denoted by $\mathbb{R}^*$. The Robinson arithmetic is obtained from $\mathbb{R}^*$ by replacing the predicate symbols $P$ and $Q$ by the function symbols $+$ and $\cdot$. Define $t^{(n)}$ as $n$-times iteration of $'$ starting with $t$. THEOREM. There is a natural number $c_1$ such that for any consistent extension $\mathfrak{A}$ of $\mathbb{R}^*$ there are a formula $A(a)$ and natural number $c_2$ with the following properties: 1) $\mathfrak{A}\not\vdash\forall x\,A(x)$, 2) for any natural number $n$ $$ \mathbb{R}^*\vdash_{c_1[\log_2(n+1)+c_2]}A(O^{(n)}). $$