The strength of Martin-Löf type theory with a superuniverse. I
type: Item
instance of: scholarly article
title: The strength of Martin-Löf type theory with a superuniverse. I
zbMATH Open document ID: 0953.03065
author: Michael Rathjen
published in: Archive for Mathematical Logic
publication date: 2001-01-23T00:00:00Z
review text: Martin-Löf introduced the notion of universes in type theory motivated, in part, by the discovery of a paradox with a type of all types [see \textit{P. Martin-Löf}, ``An intuitionistic theory of types'', in: G. Sambin (ed.) et al., Twenty-five years of constructive type theory, Oxford Logic Guides 36, 127-172 (1998; Zbl 0931.03070)]. This is a natural reflection principle, which can be seen as an intuitionistic version of the notion of Grothendieck universes in set theory. Palmgren, motivated by his domain model of universes, introduced in his Ph.D. thesis, the notion of next universe operator and of superuniverse, which is a universe closed by the universe operator. He introduced also an higher-order version of this notion, which can be seen as an intuitionistic version of Mahlo cardinals. In the absence of generalised inductive definitions, all these systems can be called predicative. This paper provides an ordinal analysis of type theory with a superuniverse. Hancock found the lower bound \(\phi_{\epsilon_0}(0)\) (where \(\phi_{\alpha}(\beta)\) is the usual Veblen hierarchy) for one universe, and the lower bound \(\Gamma_0\) for a sequence of universes (these bounds were proved optimal by, respectively, Aczel and Feferman [see \textit{S. Feferman}, in G. Metakides (ed.), Patras Logic Symp., Proc., Patras, Greece 1980, Stud. Log. Found. Math. 109, 171-196 (1982; Zbl 0522.03045)]). The ordinal of type theory with a superuniverse is \(\Phi_{\Gamma_0}(0)\), where \(\Phi_{\alpha}(\beta)\) is similar to the Veblen hierachy but starts with \(\Phi_0(\xi) = \Gamma_{\xi}\) where \(\Gamma_{\alpha}\) is the \(\alpha^{th}\) ordinal \(\rho>0\) such that \(\phi_{\delta}(\xi)<\rho\) for all \(\xi,\delta<\rho\). This ordinal is below the Howard ordinal (the ordinal of one generalised inductive definition) but bigger than \(\Gamma_0\). This is quite interesting because it has been argued previously (following the work of Schütte and Feferman in the 60s) that \(\Gamma_0\) is an upp…
reviewed by: Thierry Coquand
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03F15
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03E70
zbMATH DE Number: 1443411
zbMATH Keywords: type theory
zbMATH Keywords: ordinal analysis
zbMATH Keywords: Kripke-Platek set theory
zbMATH Keywords: predicative systems
MaRDI profile type: Publication
full work available at URL: s001530050001
OpenAlex ID: W4236196131
DOI: 10.1007/S001530050001
Recommended article: The strength of Martin-Löf type theory with a superuniverse. II
Recommended article: Q4715478
Recommended article: Q4944921
Recommended article: Supercompilation for Martin-Lof's type theory
Recommended article: Extending Martin-Löf type theory by one Mahlo-universe
Recommended article: An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe
Recommended article: Certifying Supercompilation for Martin-Löf’s Type Theory
Recommended article: Q4247308
Recommended article: A construction of type: type in Martin-Löf's partial type theory with one universe
Recommended article: Q5457304
description: scientific article; zbMATH DE number 1443411