Predicativity of the Mahlo universe in type theory
Peter Dybjer
Chalmers University of Technology
Abstract:
We present a constructive, predicative justification of Setzer’s Mahlo universe in type
theory. Our approach is closely related to Kahle and Setzer’s axiomatization of an ex-
tended predicative Mahlo universe in Feferman’s Explicit Mathematics, a framework with
direct access to the collection of partial functions. However, we here work directly in
Martin-Löf type theory, a theory where all functions are total. We analyze Setzer’s orig-
inal version of the Mahlo universe, as opposed to the version derived in previous work
through the modeling of Explicit Mathematics with an extended predicative Mahlo uni-
verse in type theory. We provide meaning explanations which extend and adapt those in
Martin-Löf’s article Constructive Mathematics and Computer Programming to cover the
proof-theoretically much stronger Mahlo universe. In this way, we aim to resolve a long-
standing discussion on whether the Mahlo universe is predicatively justifiable. We also
construct four models in set-theoretic metalanguage that provide mathematical support
for the meaning explanations. We prove that they are indeed models of the type theory
in question and discuss their relationship to the meaning explanations. This research is
a substantial step in the predicative justification of the consistency of proof-theoretically
strong theories. Our work thus contributes to a revised Hilbert program, aiming to over-
come the limitations implied by Gödel’s incompleteness theorem, namely that there is no
mathematical proof of the consistency of mathematical theories based on finitary methods,
except for very weak theories.
Joint work with Anton Setzer, Swansea.