Abstract

The present work contains an axiomatic treatment of some parts of the restricted version of intuitionistic mathematics advocated by G. F. C. Griss, also known as negationless intuitionistic mathematics.Formal systems NPC, NA, and FIMN for negationless predicate logic, arithmetic, and analysis are proposed. Our Theorem 4 in Section 2 asserts the translatability of Heyting's arithmetic HAinto NA. The result can in fact be extended to a large class of intuitionistic theories based on HAand their negationless counterparts. For instance, in Section 3 this is shown for Kleene's system of intuitionistic analysis FIMand our FIMN.