2026/27 Format schedule

Abstract: This talk shall focus on the formal proof-theoretic analysis of a weak, semi-intuitionistic third-order system of arithmetic and the capabilities of developing mathematics within it. The system is proposed by Nik Weaver, an analyst-turned-philosopher, in order to fulfil his ideals of mathematical conceptualism — essentially a modern refurbishment of Weylian predicativism. We shall explore the intuitionistic and constructive perks of this theory through a realisability interpretation and exploit the ordinal analysis paradigm to assess whether it has accomplished Weaver's goal of characterising the predicative mathematical domain.

The talk is based on the speaker's PhD work and the survey essay Recent Developments on Predicative Foundations, joint work with Michael Rathjen, in the latest collection Pillars of Enduring Strength: Learning from Hermann Weyl. 

Abstract: This is based on joint work with Nikolay Bazhenov, Ivan Georgiev, Dariusz Kalociński and Stefan Vatev.

We work within the recently widely studied framework of punctual (or fully primitive recursive) structure theory, introduced by Kalimullin, Melnikov and Ng. Using the mainland-island technique, they showed that there exists a punctual copy $\mathcal{A}$ of $\mathcal{S}=(\mathbb{N},Succ)$ -- natural numbers with successor, such that no primitive recursive isomorphism from $\mathcal{A}$ to $\mathcal{S}$ exists. 

A refinement of this argument yields a punctual copy of $\mathcal{S}$ with a primitive recursive predecessor but still not punctually isomorphic to $\mathcal{S}$. This raises a natural question: how far can this method be pushed?

 In our work, we call a class of primitive recursive functions $\mathcal{F}$ \textbf{a basis for punctual standardness} if, for every punctual copy $\mathcal{A}$ of $\mathcal{S}$ where all functions from $\mathcal{F}$ are primitive recursive, the structure $\mathcal{A}$ has the standard class of primitive recursive functions, or equivalently, a punctual isomorphism between $\mathcal{A}$ and $\mathcal{S}$ exists. We call such copies \textbf{punctually standard}, otherwise a copy is \textbf{non-standard}.

We prove a general theorem, using a mainland-archipelago method (a stronger version of mainland-island technique) : If an $L$-family $(\mathcal{Q},\mathcal{F})$ has a set of normal forms, then $\mathcal{F}$ is not a basis for punctual standardness.

Abstract: TBA

Abstract: TBA

Abstract: TBA

Abstract: TBA