“School of Mathematics”

Back to Papers Home
Back to Papers of School of Mathematics

Paper   IPM / M / 529
School of Mathematics
  Title:   Some weak fragments of HA and certain closure properties
1.  Mor. Moniri
2.  Moj. Moniri
  Status:   Published
  Journal: J. Symbolic Logic
  No.:  1
  Vol.:  67
  Year:  2002
  Pages:   91-103
  Publisher(s):   Assoc. Symbol. Logic
  Supported by:  IPM
We show that Intuitionistic Open Induction iop is not closed under the rule DNS(∃1). This is established by constructing a Kripke model of iopLy(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, i1 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
scroll left or right