FYI:Usable foundational systems for finitistic mathematics

[Alex Shkotin]

It is quite possible that finitian ideas are close to some formal ontologists.

Alex

---------- Forwarded message ---------
От: Graham Leigh <graham...@gu.se>
Date: сб, 27 сент. 2025 г. в 19:30
Subject: [FOM] Nordic Online Logic Seminar: next talk on 29 September by Peter Lumsdaine
To: FOM Mailing List <f...@lists.ugent.be>

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