“School of Mathematics”

Back to Papers Home
Back to Papers of School of Mathematics

Paper   IPM / M / 45
School of Mathematics
  Title:   Intuitionistic open induction and least number principle and the Buss operator
1.  M Ardeshir
2.  Moj. Moniri
  Status:   Published
  Journal: Notre Dame J. Formal Logic
  No.:  2
  Vol.:  39
  Year:  1998
  Pages:   212-220
  Supported by:  IPM
Buss asked in [1] whether every intuitionistic theory is, for some classical theory T, that of all T-normal Kripke structures H (T) for which he gave an r.e. axiomatization. In the language of arithmetic Iop and Lop denote PA plus Open Induction or Open LNP, iop and lop are their intuitionistic deductive closures. We show H (Iop)=lop is recursively axiomatizable and lop \vdashi  c \dashv iop, while i1 \not\vdash lop. If iT proves PEMatomic but not totality of a classically provably total Diophantine function of T, then H(T) ⊄ eq i T and so iT ∉ range (H). A result due to Wehmeier then implies iΠ1 ∉ range (H). We prove Iop is not ∀2-conservative over i1. If IopTI1, then iT is not closed under MRopen or Friedman's translation, so iT ∉ range (H). Both Iop and I1 are closed under the negative translation.

Download TeX format
back to top
scroll left or right