Independence results for variants of sharply bounded induction (Q716498)

The paper opens with a brief but informative survey of results and techniques concerning separation of fragments of Buss's bounded arithmetic theory \(S_2\). The rest is devoted to independence results for the theory \(T^0_2\) (\(= \mathrm{BASIC} + \Sigma^b_0\)-IND) and its extensions. \textit{A. J. Wilkie} proved in [``Some results and problems on weak systems of arithmetic'', Logic colloquium '77, Proc., Wrocław 1977, Stud. Logic Found. Math. Vol. 96, 285--296 (1978; Zbl 0449.03076)] that every \({\mathbb Z}\)-ring can be extended to a model of Open Induction. Kołodziejczyk modifies Wilkie's construction by replacing \({\mathbb Z}\) with a suitable nonstandard cut \(J\) in a model of Peano arithmetic. For a model \(N_0\), a cut \(J\) of \(N_0\), and an elementary extension \(N_0\prec N\) end extending \(J\), a notion of \(J\)-ring is defined for subrings of the real closure of \(N\). It is shown that if a \(J\)-ring is a model of IOpen then it is a model of \(T^0_2\). By an iteration argument it follows that every countable \(J\)-ring can be extended to a model of \(T^0_2\). As a corollary, it is shown that Sheperdson's model of IOpen can be extended to a model of \(T^0_2\), which implies that \(T^0_2\) is rather weak. It cannot prove that a power of 2 is not divisible by 3, that \(\sqrt{2}\) is irrational, and that there are no positive integers \(x\), \(y\), and \(z\) such that \(x^3+y^3=z^3\). The last section of the paper is devoted to the extension of \(T^0_2\) obtained by adding the axiom LeastBit: ``for each positive \(x\) there is a smallest power of 2 which does not divide \(x\)''. It is shown that \(T^0_2 + \mathrm{LeastBit}\) proves that a power of 2 has no non-trivial odd divisors, and that \(\sqrt{2}\) is irrational. In the last result, Kołodziejczyk constructs a model of \(T^0_2 + \mathrm{LeastBit}\) in which the set of primes is bounded. The proof also shows that \(T^0_2 + \mathrm{LeastBit}\) does not prove Matiyasevich's Theorem: there is no \(\Sigma^b_1\)-formula defining primality in all models of \(T^0_2 + \mathrm{LeastBit}\). The paper concludes with three interesting open problems.