Independence results for variants of sharply bounded induction

The theory , axiomatized by the induction scheme for sharply bounded formulae in Buss’ original language of bounded arithmetic (with ⌊x/2⌋ but not ⌊x/2^y⌋), has recently been unconditionally separated from full bounded arithmetic S₂. 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 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 , which immediately implies some independence results for ; (ii) extended by an axiom which roughly states that every number has a least 1 bit in its binary notation, while significantly stronger than plain , does not prove the infinity of primes.