The extended predicative Mahlo universe in Martin-Löf type theory

Dybjer, Peter; Setzer, Anton

doi:10.1093/logcom/exad022

Journal article 653 views 59 downloads

The extended predicative Mahlo universe in Martin-Löf type theory

Peter Dybjer, Anton Setzer

Journal of Logic and Computation, Volume: 34, Issue: 6, Pages: 1032 - 1063

Swansea University Author: Anton Setzer

PDF | Version of Record

Distributed under the terms of a Creative Commons Attribution 4.0 License (CC BY 4.0).
Download (3.56MB)

Check full text

DOI (Published version): 10.1093/logcom/exad022

Abstract

This paper addresses the long-standing question of the predicativity of the Mahlo universe. A solution, called the extended predicative Mahlo universe, has been proposed by Kahle and Setzer in the context of explicit mathematics. It makes use of the collection of untyped terms (denoting partial func...

Full description

Published in:	Journal of Logic and Computation
ISSN:	0955-792X 1465-363X
Published:	Oxford University Press (OUP) 2024
Online Access:	Check full text
URI:	https://cronfa.swan.ac.uk/Record/cronfa63064
Tags:	Add Tag No Tags, Be the first to tag this record!

first_indexed	2023-04-03T13:47:23Z
last_indexed	2023-04-20T03:23:33Z
id	cronfa63064
recordtype	SURis
fullrecord	<?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>63064</id><entry>2023-04-03</entry><title>The extended predicative Mahlo universe in Martin-Löf 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>2023-04-03</date><deptcode>MACS</deptcode><abstract>This paper addresses the long-standing question of the predicativity of the Mahlo universe. A solution, called the extended predicative Mahlo universe, has been proposed by Kahle and Setzer in the context of explicit mathematics. It makes use of the collection of untyped terms (denoting partial functions) which are directly available in explicit mathematics but not in Martin-Löf type theory. In this paper we overcome the obstacle of not having direct access to untyped terms in Martin-Löf type theory by formalizing explicit mathematics with an extended predicative Mahlo universe in Martin-Löf type theory with certain indexed inductive-recursive definitions. In this way we can relate the predicativity question to the fundamental semantics of Martin-Löf type theory in terms of computation to canonical form. As a result we get the first extended predicative definition of a Mahlo universe in Martin-Löf type theory. To this end we first define an external variant of Kahle and Setzer's internal extended predicative universe in explicit mathematics. This is then formalized in Martin-Löf type theory, where it becomes an internal extended predicative Mahlo universe. Although we make use of indexed inductive-recursive definitions that go beyond the type theory IIRD of indexed inductive-recursive definitions defined in previous work by the authors, we argue that they are constructive and predicative in Martin-Löf's sense. The model construction has been type-checked in the proof assistant Agda.</abstract><type>Journal Article</type><journal>Journal of Logic and Computation</journal><volume>34</volume><journalNumber>6</journalNumber><paginationStart>1032</paginationStart><paginationEnd>1063</paginationEnd><publisher>Oxford University Press (OUP)</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint>0955-792X</issnPrint><issnElectronic>1465-363X</issnElectronic><keywords>Martin-Löf type theory, Mahlo, universes, meaning explanations, extended predicativity, predicativity, explicit mathematics, inductive-recursive definitions, indexed induction-recursion, constructive mathematics, Agda, partial functions</keywords><publishedDay>6</publishedDay><publishedMonth>9</publishedMonth><publishedYear>2024</publishedYear><publishedDate>2024-09-06</publishedDate><doi>10.1093/logcom/exad022</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>SU Library paid the OA fee (TA Institutional Deal)</apcterm><funders>Anton Setzer was supported by STSM grant E-COST-GRANT-CA20111-f6450ef0 “Formalisation of Meaning Explanations in Agda” and by the “Training School: Dedukti school & Women in EuroProofNet” E-COST-TRAINING_SCHOOL-CA20111-240622-53c72694-94240eb3-dc2e-11ec-b8f2-0204f3b8d66d, both through COST Action: CA20111 - European Research Network on Formal Proofs.</funders><projectreference/><lastEdited>2024-09-17T16:27:03.2188047</lastEdited><Created>2023-04-03T14:36:32.2589398</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>Peter</firstname><surname>Dybjer</surname><order>1</order></author><author><firstname>Anton</firstname><surname>Setzer</surname><orcid>0000-0001-5322-6060</orcid><order>2</order></author></authors><documents><document><filename>63064__27582__b47f7914b26646f79988abaa9ec2afa7.pdf</filename><originalFilename>63064.pdf</originalFilename><uploaded>2023-05-23T15:14:08.9078378</uploaded><type>Output</type><contentLength>3733251</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>Distributed under the terms of a Creative Commons Attribution 4.0 License (CC BY 4.0).</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/4.0</licence></document></documents><OutputDurs/></rfc1807>
spelling	v2 63064 2023-04-03 The extended predicative Mahlo universe in Martin-Löf type theory 5f7695285397f46d121207120247c2ae 0000-0001-5322-6060 Anton Setzer Anton Setzer true false 2023-04-03 MACS This paper addresses the long-standing question of the predicativity of the Mahlo universe. A solution, called the extended predicative Mahlo universe, has been proposed by Kahle and Setzer in the context of explicit mathematics. It makes use of the collection of untyped terms (denoting partial functions) which are directly available in explicit mathematics but not in Martin-Löf type theory. In this paper we overcome the obstacle of not having direct access to untyped terms in Martin-Löf type theory by formalizing explicit mathematics with an extended predicative Mahlo universe in Martin-Löf type theory with certain indexed inductive-recursive definitions. In this way we can relate the predicativity question to the fundamental semantics of Martin-Löf type theory in terms of computation to canonical form. As a result we get the first extended predicative definition of a Mahlo universe in Martin-Löf type theory. To this end we first define an external variant of Kahle and Setzer's internal extended predicative universe in explicit mathematics. This is then formalized in Martin-Löf type theory, where it becomes an internal extended predicative Mahlo universe. Although we make use of indexed inductive-recursive definitions that go beyond the type theory IIRD of indexed inductive-recursive definitions defined in previous work by the authors, we argue that they are constructive and predicative in Martin-Löf's sense. The model construction has been type-checked in the proof assistant Agda. Journal Article Journal of Logic and Computation 34 6 1032 1063 Oxford University Press (OUP) 0955-792X 1465-363X Martin-Löf type theory, Mahlo, universes, meaning explanations, extended predicativity, predicativity, explicit mathematics, inductive-recursive definitions, indexed induction-recursion, constructive mathematics, Agda, partial functions 6 9 2024 2024-09-06 10.1093/logcom/exad022 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University SU Library paid the OA fee (TA Institutional Deal) Anton Setzer was supported by STSM grant E-COST-GRANT-CA20111-f6450ef0 “Formalisation of Meaning Explanations in Agda” and by the “Training School: Dedukti school & Women in EuroProofNet” E-COST-TRAINING_SCHOOL-CA20111-240622-53c72694-94240eb3-dc2e-11ec-b8f2-0204f3b8d66d, both through COST Action: CA20111 - European Research Network on Formal Proofs. 2024-09-17T16:27:03.2188047 2023-04-03T14:36:32.2589398 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Peter Dybjer 1 Anton Setzer 0000-0001-5322-6060 2 63064__27582__b47f7914b26646f79988abaa9ec2afa7.pdf 63064.pdf 2023-05-23T15:14:08.9078378 Output 3733251 application/pdf Version of Record true Distributed under the terms of a Creative Commons Attribution 4.0 License (CC BY 4.0). true eng https://creativecommons.org/licenses/by/4.0
title	The extended predicative Mahlo universe in Martin-Löf type theory
spellingShingle	The extended predicative Mahlo universe in Martin-Löf type theory Anton Setzer
title_short	The extended predicative Mahlo universe in Martin-Löf type theory
title_full	The extended predicative Mahlo universe in Martin-Löf type theory
title_fullStr	The extended predicative Mahlo universe in Martin-Löf type theory
title_full_unstemmed	The extended predicative Mahlo universe in Martin-Löf type theory
title_sort	The extended predicative Mahlo universe in Martin-Löf type theory
author_id_str_mv	5f7695285397f46d121207120247c2ae
author_id_fullname_str_mv	5f7695285397f46d121207120247c2ae_***_Anton Setzer
author	Anton Setzer
author2	Peter Dybjer Anton Setzer
format	Journal article
container_title	Journal of Logic and Computation
container_volume	34
container_issue	6
container_start_page	1032
publishDate	2024
institution	Swansea University
issn	0955-792X 1465-363X
doi_str_mv	10.1093/logcom/exad022
publisher	Oxford University Press (OUP)
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	1
active_str	0
description	This paper addresses the long-standing question of the predicativity of the Mahlo universe. A solution, called the extended predicative Mahlo universe, has been proposed by Kahle and Setzer in the context of explicit mathematics. It makes use of the collection of untyped terms (denoting partial functions) which are directly available in explicit mathematics but not in Martin-Löf type theory. In this paper we overcome the obstacle of not having direct access to untyped terms in Martin-Löf type theory by formalizing explicit mathematics with an extended predicative Mahlo universe in Martin-Löf type theory with certain indexed inductive-recursive definitions. In this way we can relate the predicativity question to the fundamental semantics of Martin-Löf type theory in terms of computation to canonical form. As a result we get the first extended predicative definition of a Mahlo universe in Martin-Löf type theory. To this end we first define an external variant of Kahle and Setzer's internal extended predicative universe in explicit mathematics. This is then formalized in Martin-Löf type theory, where it becomes an internal extended predicative Mahlo universe. Although we make use of indexed inductive-recursive definitions that go beyond the type theory IIRD of indexed inductive-recursive definitions defined in previous work by the authors, we argue that they are constructive and predicative in Martin-Löf's sense. The model construction has been type-checked in the proof assistant Agda.
published_date	2024-09-06T16:27:01Z
_version_	1810457502977884160
score	11.037056

The extended predicative Mahlo universe in Martin-Löf type theory

Similar Items