Predicative foundations of the Mahlo universe in Martin-Löf type theory
Anton Setzer
Swansea University
Hilbert’s original program had the aim to prove the consistency of mathematical theories using finitary methods. However, due to Gödel’s incompleteness theorems, finitary methods are insufficient, requiring stronger approaches. A revised version of Hilbert’s program involves reducing the consistency of strong theories to theories with some form of justification of their consistency, in particular predicative justifications.
Extensions of Martin-Löf Type Theory (MLTT) are candidates for predicatively justified theories. In particular, MLTT extended with a collection of inductive-recursive definitions can be seen as predicatively justified.
To achieve greater proof-theoretic strength, and following the developments of ordinal-theoretic proof theory, the author added the Mahlo Universe [4] to Martin-Löf Type Theory, obtaining the proof-theoretic strength KPM+. However, it is controversial, whether it can be regarded as predicatively justified. Palmgren’s paradox, which shows the inconsistency of the Mahlo Universe when extended with naive elimination rules, raises significant concerns. This talk explores approaches to establish a more robust predicative justification, which indicate that Palmgren’s elimination rules are not the correct ones.
One such approach is the extended predicative Mahlo Universe in Explicit Mathematics, developed jointly with Reinhard Kahle [3]. Explicit Mathematics is an alternative to MLTT which provides direct access to partial functions. In collaboration with Peter Dybjer [1], we implemented this extended universe within MLTT, which amounted to an extended form of inductive-recursive definitions. This construction relied on a set of terms representing partial functions.
In [2] (joint work with Peter Dybjer), we followed a different approach using a set-theoretic meta-theory. Starting with a set-theoretic Mahlo Universe, we constructed a model of the type theoretic Mahlo universe closed under functions from families of its sets of the set theoretic Mahlo universe into itself. In several steps, we replaced this impredicative reliance on the total functions from the set theoretic Mahlo universe into itself by elements of the set theoretic Mahlo universe. These sets are the set theoretic analogue of the partial functions used in the previous versions.
In the final part of this talk, we investigate the construction of models for the extended predicative Mahlo Universe in Explicit Mathematics, based on monotone inductive definitions over families of sets.
[1] Peter Dybjer and Anton Setzer, The extended predicative Mahlo universe in
Martin-Löf type theory, Journal of Logic and Computation, vol. 34 (2023), no. 6,
pp. 1032–1063.
[2] Peter Dybjer and Anton Setzer, Predicativity of the Mahlo Universe in type
theory, Accepted for Publication in Laura Crosilla and Michael Rathjen (eds.)
Pillars of enduring strength: learning from Hermann Weyl, Oxford University
Press, 2025
[3] Reinhard Kahle and Anton Setzer, An extended predicative definition of the
Mahlo universe, Ralf Schindler (Ed) Ways of proof theory, Ontos Series in
Mathematical Logic, De Gruyter, 2010
[4] —————, Extending Martin-Löf Type Theory by one Mahlo-universe, Archive for
Mathematical Logic vol. 39 (2000), no. 3, pp. 155–181.