Structures interpretable in models of bounded arithmetic (Q2570136)

\(S^i_0\) is a theory in the language \(\{+,\times, | \;| ,0,1,2\}\) corresponding to Buss' \(S^1_2\), but aiming at properties of models of arithmetic wit a top (with \(+\) and \(\times\) considered as relations). A typical model of \(S^1_0\) is an initial segment with a top of a model of \(S^1_2\). In ``A model-theoretic characterization of the weak pigeonhole principle'' [Ann. Pure Appl. Logic 118, 175--195 (2002; Zbl 1008.03024)], \textit{N. Thapen} proved that if \(K\) is a model of \(S^1_0\) of the form \([0,a^\varepsilon)\) for some \(a,\varepsilon\in K\), and a form of the Weak Pigeonhole Principle for \(a^2\) and \(a\) fails in \(K\), then \(K\) has an end extension to a model \(J\) of \(S^1_0\) of the form \([0,a^{\varepsilon^l})\). Furthermore, this extension is \(\overline\Sigma^b_1\) interpreted in \(K\) below \(a\). Here \(\overline\Sigma^b_1\) is a class of formulas corresponding to Buss' \(\Sigma^b_1\) in the context of \(S^1_0\). While, due to Friedman's Embedding Theorem, there is no full converse to this result, Thapen proves an ``almost converse.'' The result is too technical to quote here. It follows from a theorem which states that if \(K\models S^1_0\) is of the form \([0,b)\), \(J\) is a model of the BASIC axioms for \(S^1_0\) and \(J\) is \(\overline\Sigma^b_1\) defined in \(K\) below \(a\), then, with some additional assumptions on the size of \(a\), there is a \(\overline\Sigma^b_1\) isomorphism either from all of \(K\) onto an initial segment of \(J\), or from an initial segment of \(K\) onto all of \(J\). The last section of the paper is devoted to a proof of the result of Wilkie on \(\forall \Sigma^b_1\) formulas witnessed in probabilistic polynomial time.