No Cover Image

Journal article 398 views 25 downloads

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

Peter Dybjer, Anton Setzer Orcid Logo

Journal of Logic and Computation

Swansea University Author: Anton Setzer Orcid Logo

  • 63064.pdf

    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)
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!
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.
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
College: Faculty of Science and Engineering
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.

Similar Items