[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
The Nordic Online Logic Seminar (NOL Seminar) is organised monthly over Zoom,
with expository talks on topics of interest for the broader logic community.
The seminar is open for professional or aspiring logicians and logic
aficionados worldwide.
See the announcement for the next talk below. If you wish to receive the Zoom
ID and password for it, as well as further announcements, please subscribe
here:
https://urldefense.com/v3/__https://listserv.gu.se/sympa/subscribe/nordiclogic__;!!IBzWLUs!TxzFxNGscG-WvBTStbsyOSXM7A0C2MckruxZNnt8K8rFNqJCk2fPt8dcnl354_fSreP9ZPxQ2wXVzmQSrokzP0ebQDINl06DzfM$
.
Val Goranko and Graham Leigh
NOL seminar organisers
Nordic Online Logic Seminar
Date Monday, 18 December 2023 at 16:00 CET (UTC+1) on Zoom
Speaker Göran Sundholm (Professor of Logic (em.), Leiden University)
Title Curry-Howard: a meaning explanation or just another realizability
interpretation?
Abstract
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.
