Fwd: Nordic Online Logic Seminar: next talk by Peter LeFanu Lumsdaine on 29 September
Joao Marcos
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://listserv.gu.se/sympa/subscribe/nordiclogic .
Val Goranko and Graham Leigh
NOL seminar organisers
--------------------------------------
Nordic Online Logic Seminar
Next talk: Monday, 29 September 2025, at 16:00 CEST (UTC+2) on Zoom (details provided to seminar subscribers)
Title: Getting rich but staying weak: Usable foundational systems for finitistic mathematics
Speaker: Peter LeFanu Lumsdaine (Associate Professor of Logic, Stockholm University)
Abstract:
There is a long tradition of distinguishing finistic methods of reasoning, for both philosophical and mathematical motivations. Typically, this is made precise by reducing arguments to some theory of arithmetic – usually Peano or Heyting Arithmetic, or weaker fragments thereof. However, working directly in such systems requires encoding all objects as numbers; it is easy to get the impression that such coding is an inherent and inevitable aspect of the topic. On the contrary, most major foundational logics – in particular, ZF-style set theory and dependent type theories – admit finitistic variants, equivalent in strength to suitable systems of arithmetic. These allow us to work rigorously in a finististic foundation, while keeping the richly expressive language we’re used to from everyday mathematics.
I will survey various finitistic systems, and then focus in more detail on the categorical Arithmetic Universes of Joyal, and type theories for these, following Maietti.