“School of Mathematics”
Back to Papers HomeBack to Papers of School of Mathematics
| Paper IPM / M / 529 |
|
||||
| Abstract: | |||||
|
We show that Intuitionistic Open Induction iop is not closed
under the rule DNS(∃1−). This is established by
constructing a Kripke model of iop+¬Ly(2y > x), where
Ly(2y > x) is universally quantified on x. On the other hand,
we prove that iop is equivalent with the intuitionistic theory
axiomatized by PA− plus the scheme of weak ¬¬LNP for
open formulas, where universal quantification on the parameters
precedes double negation. We also show that for any open formula
φ(y), (PA−)i\vdash Lyφ(y). We observe
that the theories iop, i∀1 and iΠ1 are closed
under Friedman's translation by negated formulas and so under VR
and IP. We include some remarks on the classical worlds in
Kripke models of iop.
Download TeX format |
|||||
| back to top | |||||
