Book chapter 19 views
Predicativity of the Mahlo Universe in type theory
Anton Setzer 
Pillars of enduring strength: learning from Hermann Weyl
Swansea University Author:
Anton Setzer
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 extended predicative Mahlo universe in Feferman’s Explicit Mathematics, a framework with direct access to the collection of parti...
| Published in: | Pillars of enduring strength: learning from Hermann Weyl |
|---|---|
| Published: |
Oxford, UK
Oxford University Press
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa69298 |
| 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 extended 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 original 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 universe 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 longstanding 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 overcome 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. |
|---|---|
| College: |
Faculty of Science and Engineering |