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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,628

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

Extending Martin-Löf Type Theory by one Mahlo-universe.Anton Setzer - 2000 - Archive for Mathematical Logic 39 (3):155-181.
The Recursively Mahlo Property in Second Order Arithmetic.Michael Rathjen - 1996 - Mathematical Logic Quarterly 42 (1):59-66.
An interpretation of Martin-löf's type theory in a type-free theory of propositions.Jan Smith - 1984 - Journal of Symbolic Logic 49 (3):730-753.
The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
The inconsistency of higher order extensions of Martin-löf's type theory.Bart Jacobs - 1989 - Journal of Philosophical Logic 18 (4):399 - 422.
The strength of Martin-Löf type theory with a superuniverse. Part II.Michael Rathjen - 2001 - Archive for Mathematical Logic 40 (3):207-233.
A general formulation of simultaneous inductive-recursive definitions in type theory.Peter Dybjer - 2000 - Journal of Symbolic Logic 65 (2):525-549.
The strength of Martin-Löf type theory with a superuniverse. Part I.Michael Rathjen - 2000 - Archive for Mathematical Logic 39 (1):1-39.
The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Power-like models of set theory.Ali Enayat - 2001 - Journal of Symbolic Logic 66 (4):1766-1782.
Are There Enough Injective Sets?Peter Aczel, Benno Berg, Johan Granström & Peter Schuster - 2013 - Studia Logica 101 (3):467-482.
Twenty-five years of constructive type theory: proceedings of a congress held in Venice, October 1995.Giovanni Sambin & Jan M. Smith (eds.) - 1998 - New York: Oxford University Press.
Propositions as [Types].Steve Awodey & Andrej Bauer - unknown
The Friedman‐Translation for Martin‐Löf's Type Theory.Erik Palmgren - 1995 - Mathematical Logic Quarterly 41 (3):314-326.
Upper Bounds for metapredicative mahlo in explicit mathematics and admissible set theory.Gerhard Jäger & Thomas Strahm - 2001 - Journal of Symbolic Logic 66 (2):935-958.

Analytics

Added to PP
2013-11-23

Downloads
44 (#359,296)

6 months
10 (#261,739)

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