NOL Seminar with Peter LeFanu Lumsdaine
published: 2025-09-10
event date:
2025-09-29
The Nordic Online Logic 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. 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
Date Monday, 29 September 2025 at 16:00 CEST (UTC+2) on Zoom
Speaker Peter LeFanu Lumsdaine (Associate Professor of Logic, Stockholm University)
Title Getting rich but staying weak: Usable foundational systems for finitistic mathematics
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.