After the 1930s, the research into the foundations of mathematics changed.None of its main directions (logicism, formalism and intuitionism) had any longer the pretension to be the only true mathematics.Usually, the determining factor in the change is considered to be Gödel?s work, while Heyting?s role is neglected.In contrast, in this paper I first describe how Heyting directly suggested the abandonment of the big foundational questions and the putting forward of a new kind of foundational research consisting in the isolation of (...) formal, intuitive, logical and platonistic elements within classical mathematics.Furthermore, I describe how Heyting indirectly influenced the abandon?ment of the old directions of foundational research by making out some lists of degrees of evidence that exist within intuitionism. (shrink)

Although the work of G.F.C. Griss is commonly understood as a program of negationless mathematics, close examination of Griss’s work suggests a more fundamental feature is its executability, a requirement that mental constructions are possible only if corresponding mental activity can be actively carried out. Emphasizing executability reveals that Griss’s arguments against negation leave open several types of negation—including D. Nelson’s strong negation—as compatible with Griss’s intuitionism. Reinterpreting Griss’s program as one of executable mathematics, we iteratively develop a pair of (...) bilateral constructive logics and argue for their adequacy as accounts of the propositional basis of Griss’s work. We conclude by observing connexive features exhibited by the two bilateral logics and by investigating the difficulties connexive principles reveal for the development of executable mathematics. (shrink)

The mathematician G.F.C. Griss is known for his program of negationless intuitionistic mathematics. Although Griss’s rejection of negation is regarded as characteristic of his philosophy, this is a consequence of an executability requirement that mental constructions presuppose agents’ executing corresponding mental activity. Restoring Griss’s executability requirement to a central role permits a more subtle characterization of the rejection of negation, according to which D. Nelson’s strong constructible negation is compatible with Griss’s principles. This exposes a ‘holographic’ theory of negation in (...) negationless mathematics, in which a full theory of negation is ‘flattened’ in a putatively negationless setting. (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.