A Model of $\widehat{R}^2_3$ inside a Subexponential Time Resource
Eugenio Chinchilla · Notre Dame Journal of Formal Logic · 1998
Using nonstandard methods we construct a model of an induction scheme called $\hat{R}^2_3$ inside a "resource" of the form $\{M(a) : M $ is a Turing machine of code $ \leq r , \mbox{ and } M(a)$ is calculated in less than $2^{\vert\vert a\vert\vert^r}\mbox{ steps}\}$, where $\vert x\vert$ means the length of the binary expansion of $x$ and $a,r$ are nonstandard parameters in a model of $S^1_3$. As a consequence we obtain a model theoretic proof of a witnessing theorem for this theory by functions computable in time $2^{\vert n\vert^{O(1)}}$, a result first obtained by Buss, Krajícek, and Takeuti using proof theory.