Archive for Mathematical Logic 40 (3):207-233 (2001)

Authors
Michael Rathjen
University of Leeds
Abstract
Universes of types were introduced into constructive type theory by Martin-Löf [3]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say ?. The universe then “reflects”?.This is the second part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf.[4–6]).It is proved that Martin-Löf type theory with a superuniverse, termed MLS, is a system whose proof-theoretic ordinal resides strictly above the Feferman-Schütte ordinal Γ0 but well below the Bachmann-Howard ordinal. Not many theories of strength between Γ0 and the Bachmann-Howard ordinal have arisen. MLS provides a natural example for such a theory. In this second part of the paper the concern is with the with upper bounds
Keywords Legacy
Categories (categorize this paper)
DOI 10.1007/s001530000051
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 50,342
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Wellordering Proofs for Metapredicative Mahlo.Thomas Strahm - 2002 - Journal of Symbolic Logic 67 (1):260-278.
Universes Over Frege Structures.Reinhard Kahle - 2003 - Annals of Pure and Applied Logic 119 (1-3):191-223.

Add more citations

Similar books and articles

The Strength of Some Martin-Löf Type Theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Extending Martin-Löf Type Theory by One Mahlo-Universe.Anton Setzer - 2000 - Archive for Mathematical Logic 39 (3):155-181.
An Ordinal Analysis of Stability.Michael Rathjen - 2004 - Archive for Mathematical Logic 44 (1):1-62.
Ptykes in GödelsT Und Definierbarkeit von Ordinalzahlen.Peter Päppinghaus - 1989 - Archive for Mathematical Logic 28 (2):119-141.
Proof-Theoretic Analysis of KPM.Michael Rathjen - 1991 - Archive for Mathematical Logic 30 (5-6):377-403.
The Friedman‐Translation for Martin‐Löf's Type Theory.Erik Palmgren - 1995 - Mathematical Logic Quarterly 41 (3):314-326.

Analytics

Added to PP index
2013-11-23

Total views
21 ( #461,931 of 2,326,062 )

Recent downloads (6 months)
1 ( #650,227 of 2,326,062 )

How can I increase my downloads?

Downloads

My notes