No Cover Image

Book chapter 339 views

Predicativity of the Mahlo Universe in type theory

Anton Setzer Orcid Logo

Pillars of enduring strength: learning from Hermann Weyl

Swansea University Author: Anton Setzer Orcid Logo

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

Full description

Published in: Pillars of enduring strength: learning from Hermann Weyl
Published: Oxford, UK Oxford University Press
URI: https://cronfa.swan.ac.uk/Record/cronfa69298
first_indexed 2025-04-16T14:06:28Z
last_indexed 2025-05-30T06:09:38Z
id cronfa69298
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2025-05-29T14:10:22.2802912</datestamp><bib-version>v2</bib-version><id>69298</id><entry>2025-04-16</entry><title>Predicativity of the Mahlo Universe in type theory</title><swanseaauthors><author><sid>5f7695285397f46d121207120247c2ae</sid><ORCID>0000-0001-5322-6060</ORCID><firstname>Anton</firstname><surname>Setzer</surname><name>Anton Setzer</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2025-04-16</date><deptcode>MACS</deptcode><abstract>We present a constructive, predicative justification of Setzer&#x2019;s Mahlo universe in type theory. Our approach is closely related to Kahle and Setzer&#x2019;s axiomatization of an extended predicative Mahlo universe in Feferman&#x2019;s Explicit Mathematics, a framework with direct access to the collection of partial functions. However, we here work directly in Martin-L&#xF6;f type theory, a theory where all functions are total. We analyze Setzer&#x2019;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&#xF6;f&#x2019;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&#xF6;del&#x2019;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.</abstract><type>Book chapter</type><journal>Pillars of enduring strength: learning from Hermann Weyl</journal><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher>Oxford University Press</publisher><placeOfPublication>Oxford, UK</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords/><publishedDay>0</publishedDay><publishedMonth>0</publishedMonth><publishedYear>0</publishedYear><publishedDate>0001-01-01</publishedDate><doi/><url/><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2025-05-29T14:10:22.2802912</lastEdited><Created>2025-04-16T09:39:49.7684247</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Anton</firstname><surname>Setzer</surname><orcid>0000-0001-5322-6060</orcid><order>1</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2025-05-29T14:10:22.2802912 v2 69298 2025-04-16 Predicativity of the Mahlo Universe in type theory 5f7695285397f46d121207120247c2ae 0000-0001-5322-6060 Anton Setzer Anton Setzer true false 2025-04-16 MACS 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. Book chapter Pillars of enduring strength: learning from Hermann Weyl Oxford University Press Oxford, UK 0 0 0 0001-01-01 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2025-05-29T14:10:22.2802912 2025-04-16T09:39:49.7684247 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Anton Setzer 0000-0001-5322-6060 1
title Predicativity of the Mahlo Universe in type theory
spellingShingle Predicativity of the Mahlo Universe in type theory
Anton Setzer
title_short Predicativity of the Mahlo Universe in type theory
title_full Predicativity of the Mahlo Universe in type theory
title_fullStr Predicativity of the Mahlo Universe in type theory
title_full_unstemmed Predicativity of the Mahlo Universe in type theory
title_sort Predicativity of the Mahlo Universe in type theory
author_id_str_mv 5f7695285397f46d121207120247c2ae
author_id_fullname_str_mv 5f7695285397f46d121207120247c2ae_***_Anton Setzer
author Anton Setzer
author2 Anton Setzer
format Book chapter
container_title Pillars of enduring strength: learning from Hermann Weyl
institution Swansea University
publisher Oxford University Press
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 0
active_str 0
description 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.
published_date 0001-01-01T05:26:35Z
_version_ 1851369555588284416
score 11.089572

Similar Items