“School of Mathematics”
Back to Papers HomeBack to Papers of School of Mathematics
Paper IPM / M / 7881  


Abstract:  
In this paper we apply some new and some old methods in order to
construct classical and intuitionistic models for theories of
bounded arithmetic. We use these models to obtain proof theoretic
consequences. In particular, we construct an ωchain of
models of BASIC such that the union of its worlds satisfies
S_{2}^{1} but none of its worlds satisfies the sentence ∀x∃y (x=0∨ x=y+1). Interpreting this chain as a Kripke model shows
that double negation of the above mentioned sentence is not provable
in the intuitionistic theory of BASIC plus polynomial
induction on coNP formulas.
Download TeX format 

back to top 