“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
S21 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 | |
