Intuitionistic open induction and least number principle and the buss operator

Abstract

In “Intuitionistic validity in T-normal Kripke structures,” Buss asked 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 ⊢i c⊣ iop, while i∀1 ⊬ lop. If iT proves PEMatomic but not totality of a classically provably total Diophantine function of T, then H (T) ⊈ iT and so iT ∉ range(H). A result due to Wehmeier then implies iᴨ1 ∉ range(H).We prove Iop is not∀2-conservative over i∀1. If Iop ⊆ T ⊆ I∀1, then iT is not closed under MRopen or Friedman’s translation, so iT ∉ range (H). Both Iop and I∀1 are closed under the negative translation. © 1998 by the University of Notre Dame. All rights reserved.