Open Access
Spring 1998 Intuitionistic Open Induction and Least Number Principle and the Buss Operator
Mohammad Ardeshir, Mojtaba Moniri
Notre Dame J. Formal Logic 39(2): 212-220 (Spring 1998). DOI: 10.1305/ndjfl/1039293063

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 ${\cal H}(T)$ for which he gave an r.e. axiomatization. In the language of arithmetic $\mathit{Iop}$ and $\mathit{Lop}$ denote PA$^{-}$ plus Open Induction or Open LNP, $\mathit{iop}$ and $\mathit{lop}$ are their intuitionistic deductive closures. We show $\mathcal{H}\mathit{(Iop)}$ $=\mathit{lop}$ is recursively axiomatizable and $\mathit{lop}\vdash_{i\ c}\dashv \mathit{iop}$, while $i\forall_{1}\not\vdash \mathit{lop}$. If $iT$ proves PEM $_{\mathrm{atomic}}$ but not totality of a classically provably total Diophantine function of $T$, then $\mathcal{H}(T)\not\subseteq iT$ and so $iT\not\in \mathrm{range({\cal H})}$. A result due to Wehmeier then implies $i\Pi_{1}\not\in\mbox{range}({\cal H})$. We prove $\mathit{Iop}$ is not $\forall_{2}$-conservative over $i\forall_{1}$. If $\mathit{Iop}\subseteq T\subseteq I\forall_{1}$, then $iT$ is not closed under MR $_{\mathrm{open}}$ or Friedman's translation, so $iT\not\in$ range (${\cal H}$). Both $\mathit{Iop}$ and $I\forall_{1}$ are closed under the negative translation.

Citation

Download Citation

Mohammad Ardeshir. Mojtaba Moniri. "Intuitionistic Open Induction and Least Number Principle and the Buss Operator." Notre Dame J. Formal Logic 39 (2) 212 - 220, Spring 1998. https://doi.org/10.1305/ndjfl/1039293063

Information

Published: Spring 1998
First available in Project Euclid: 7 December 2002

zbMATH: 0968.03074
MathSciNet: MR1714956
Digital Object Identifier: 10.1305/ndjfl/1039293063

Subjects:
Primary: 03F55
Secondary: 03B20 , 03F30

Rights: Copyright © 1998 University of Notre Dame

Vol.39 • No. 2 • Spring 1998
Back to Top