A negationless interpretation of intuitionistic theories (Q1841006)

The paper introduces systems which are intended to formalize Griss' so-called negationless mathematics and studies their relation to corresponding systems of intuitionistic mathematics. The author first introduces a natural deduction-style calculus for negationless first-order predicate calculus and then moves on to define -- based on this calculus -- systems of negationless arithmetic \textbf{NA}, negationless primitive recursive analysis \textbf{PrAn}\(^N\) and negationless higher-order arithmetic \textbf{NAH}. He constructs translations \(F_1\) of these systems into intuitionistic (`Heyting') arithmetic \textbf{HA}, intuitionistic primitive recursive analysis \textbf{PrAn} and intuitionistic higher-order arithmetic \textbf{HAH} respectively as well as translations \(F_2\) the other way round. The main results state that \(F_1(F_2(A))\) and \(A\) are intuitionistically equivalent and that \(F_2(F_1(A))\) and \(A\) are equivalent in the sense of the corresponding negationless systems. Thus the intuitionistic systems and their negationless counterparts are essentially equivalent. The author also briefly discusses the relation of his formalization of Griss' ideas with D. Nelson's sequent-style systems. No proofs are given but it is referred to two technical reports which, however, meanwhile appeared as journal articles [\textit{N. Krivtsov}, ``A negationless interpretation of intuitionistic theories. I, II'', Stud. Logica 64, 323-344 (2000; Zbl 0964.03065), 65, 155-179 (2000; Zbl 0968.03073)].