Curry-Howard: a meaning explanation or just another realizability interpretation?
Göran Sundholm, Leiden University
Around 1930 a major paradigm shift occurred in the foundations of mathematics; we may call it the METAMATHEMATICAL TURN. Until then the task of a logician had been to design and explain a full-scale formal language that was adequate for the practice of mathematical analysis in such a way that the axioms and rules of inference of the theory were rendered evident by the explanations.
The metamathematical turn changed the status of the formal languages: now they became (meta)mathematical objects of study. We no longer communicate with the aid of the formal systems – we communicate about them. Kleene’s realizability (JSL 1945) gave a metamathematical (re-)interpretation of arithmetic inside arithmetic. Heyting and Kolmogorov (1931-2), on the other hand, had used “proofs” of propositions, respectively “solutions” to problems, in order to explain the meaning of the mathematical language, rather than reinterpret it internally.
We now have the choice to view the Curry-Howard isomorphism, say, as a variant of realizability, when it will be an internal mathematical re-interpretation, or to adopt an atavistic, Frege-like, viewpoint and look at the language as being rendered meaningful. This perspective will be used to discuss another paradigm shift, namely that of distinguishing constructivism and intuitionism. The hesitant attitude of Gödel, Kreisel, and Michael Dummett, will be spelled out, and, at the hand of unpublished source material, a likely reason given.