Independence results for variants of sharply bounded induction

The theory T 2 0 , 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 2 . The method used to prove the separation is reminiscent of those known from the study of open induction. e the connection to open induction explicit, showing that models of T 2 0 can be built using a “nonstandard variant” of Wilkie’s well-known technique for building models of I O p e n . This makes it possible to transfer many results and methods from open to sharply bounded induction with relative ease. vide two applications: (i) the Shepherdson model of I O p e n can be embedded into a model of T 2 0 , which immediately implies some independence results for T 2 0 ; (ii) T 2 0 extended by an axiom which roughly states that every number has a least 1 bit in its binary notation, while significantly stronger than plain T 2 0 , does not prove the infinity of primes.