# 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.