Realizing Mahlo set theory in type theory

Archive for Mathematical Logic 42 (1):89-101 (2003)
  Copy   BIBTEX

Abstract

After introducing the large set notion of Mahloness, this paper shows that constructive set theory with an axiom asserting the existence of a Mahlo set has a realizability interpretation in an extension of Martin-Löf type theory developed by A. Setzer

Categories

Keywords

Reprint years

DOI

10.1007/s00153-002-0159-6

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,247

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Characterizing the interpretation of set theory in Martin-Löf type theory.Michael Rathjen & Sergei Tupailo - 2006 - Annals of Pure and Applied Logic 141 (3):442-471.
The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
Realization of constructive set theory into explicit mathematics: a lower bound for impredicative Mahlo universe.Sergei Tupailo - 2003 - Annals of Pure and Applied Logic 120 (1-3):165-196.
Induction–recursion and initial algebras.Peter Dybjer & Anton Setzer - 2003 - Annals of Pure and Applied Logic 124 (1-3):1-47.
The axiom of multiple choice and models for constructive set theory.Benno van den Berg & Ieke Moerdijk - 2014 - Journal of Mathematical Logic 14 (1):1450005.
The strength of Martin-Löf type theory with a superuniverse. Part II.Michael Rathjen - 2001 - Archive for Mathematical Logic 40 (3):207-233.
Extensionality Versus Constructivity.Silvio Valentini - 2002 - Mathematical Logic Quarterly 48 (2):179-187.
The Recursively Mahlo Property in Second Order Arithmetic.Michael Rathjen - 1996 - Mathematical Logic Quarterly 42 (1):59-66.
The strength of Martin-Löf type theory with a superuniverse. Part I.Michael Rathjen - 2000 - Archive for Mathematical Logic 39 (1):1-39.
On the regular extension axiom and its variants.Robert S. Lubarsky & Michael Rathjen - 2003 - Mathematical Logic Quarterly 49 (5):511.

Analytics

Added to PP
2013-11-23

Downloads
73 (#287,407)

6 months
15 (#206,160)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Michael Rathjen
University of Leeds

Citations of this work

Set theory: Constructive and intuitionistic ZF.Laura Crosilla - 2010 - Stanford Encyclopedia of Philosophy.

Add more citations

References found in this work

The Higher Infinite.Akihiro Kanamori - 2000 - Studia Logica 65 (3):443-446.

Add more references