Independence results for variants of sharply bounded induction

The theory T20, axiomatized by the induction scheme for sharply bounded formulae in Buss' original language of bounded arithmetic (with ⌊x/2⌋ but not ⌊x/2y⌋), has recently been unconditionally separated from full bounded arithmetic S2. The method used to prove the separation is reminiscent of those known from the study of open induction.We make the connection to open induction explicit, showing that models of T20 can be built using a “nonstandard variant” of Wilkie's well-known technique for building models of IOpen. This makes it possible to transfer many results and methods from open to sharply bounded induction with relative ease.We provide two applications: (i) the Shepherdson model of IOpen can be embedded into a model of T20, which immediately implies some independence results for T20; (ii) T20 extended by an axiom which roughly states that every number has a least 1 bit in its binary notation, while significantly stronger than plain T20, does not prove the infinity of primes.

► We study sharply bounded induction as originally defined by Buss. ► Techniques from open induction are transferred to sharply bounded induction. ► Shepherdson's model is embeddable in a model of sharply bounded induction. ► We also consider the axiom 'every number has a least 1 bit'. ► Sharply bounded induction with that axiom does not prove cofinality of primes.