Intentionality, Intuition, and Proof in Mathematics

In the late nineteen twenties and early nineteen thirties Arend Heyting, following Oskar Becker, identified proofs with fulfillments of mathematical intentions (in the sense of intentionality). The idea of proofs as fulfillment of intentions was then used by Heyting and Becker to interpret the intutionistic logical constants, and in this use it played an important historical role in the formulation of what is now called the BHK interpretation of the intuitionistic logical constants. The idea was that proofs in the sense of intuitionistic constructions are just forms of intuition, where intuitions are understood as fulfillments of mathematical intentions. A variant of this interpretation was formulated by Kolmogorov at around the same time, in terms of problems (in place of intentions) and solutions (in place of fulfillments). In recent times, Martin-Löf has again used the language of intention and fulfillment in some presentations of his work on intutionistic type theory. By association, there are also relationships to the Curry-Howard idea of formulae-as-types, and to other technical developments.

In my talk I will examine the idea of proofs as fulfillments of intentions, propose a related account of mathematical intuition, and consider the question whether the ideas of intentionality and proof as fulfillment (= intuition) in mathematics have applications that extend beyond constructive foundations.