We put together several observations on constructive negation. First, Russell anticipated intuitionistic logic by clearly distinguishing propositional principles implying the law of the excluded middle from remaining valid principles. He stated what was later called Peirce’s law. This is important in connection with the method used later by Heyting for developing his axiomatization of intuitionistic logic. Second, a work by Dragalin and his students provides easy embeddings of classical arithmetic and analysis into intuitionistic negationless systems. In the last section, we (...) present in some detail a stepwise construction of negation which essentially concluded the formation of the logical base of the Russian constructivist school. Markov’s own proof of Markov’s principle (different from later proofs by Friedman and Dragalin) is described. (shrink)

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. (shrink)

This work is a sequel to our [16]. It is shown how Theorem 4 of [16], dealing with the translatability of HA(Heyting's arithmetic) into negationless arithmetic NA, can be extended to the case of intuitionistic arithmetic in higher types.