A negationless interpretation of intuitionistic theories. I (Q1577359)

The present paper provides a definitive and remarkably simple answer to the problem of axiomatizing Griss's negationless intuitionistic mathematics. There have been several such attempts, the last and most successful one being \textit{D. Nelson}'s [J. Symb. Log. 31, 562-572 (1966; Zbl 0148.24404)] sequent calculus \(P_1\). Even though \(P_1\) did provide a satisfactory formalization for negationless predicate logic, both its logical constants and its rules of inference needed to be simplified to allow for proof-theoretical analyses. The natural deduction system presented here, called NPC, contains as logical constants only \(\exists\) and \(\rightarrow_{\overline{x}}\) (quantified implication, \(\overline{x}\) standing for a finite sequence of variables \(x_1, \ldots, x_n\)) -- the logical constants \(\forall\) and \(\&\) may be used for convenience but are not needed -- and a small number of short and perfectly clear inference rules. (As shown in part II of this paper the system is equivalent to a slight modification of the \(\Sigma\)-free fragment of Nelson's \(P_1\).) The author defines a translation operation \(^*\), which associates with each formula \(\alpha\) of NPC a formula \(\alpha^*\) of the conventional intuitionistic predicate calculus IQC, and proves the corresponding conservativity result. Using arithmetic and Kleene's system of intuitionist analysis as examples, the author introduces translations from the intuitionistic theory (Heyting Arithmetic and Kleene's FIM [cf. \textit{S. C. Kleene} and \textit{R. E. Vesley}, The foundations of intuitionistic mathematics, North-Holland, Amsterdam (1965; Zbl 0133.24601)]) to the negationless one and vice-versa, and then proves strong conservativity results for both. These two examples make it plain how to proceed with axiomatizing in a negationless intuitionistic manner any given intuitionistic theory.