The Generalised Type-Theoretic Interpretation of Constructive Set Theory

Journal of Symbolic Logic 71 (1):67 - 103 (2006)
  Copy   BIBTEX

Abstract

We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,150

External links

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

Through your library

Similar books and articles

The inconsistency of higher order extensions of Martin-löf's type theory.Bart Jacobs - 1989 - Journal of Philosophical Logic 18 (4):399 - 422.
Godel's interpretation of intuitionism.William Tait - 2006 - Philosophia Mathematica 14 (2):208-228.
Syntactic calculus with dependent types.Aarne Ranta - 1998 - Journal of Logic, Language and Information 7 (4):413-431.
Implicit epistemic aspects of constructive logic.Göran Sundholm - 1997 - Journal of Logic, Language and Information 6 (2):191-212.

Analytics

Added to PP
2010-08-24

Downloads
63 (#257,343)

6 months
23 (#120,318)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

A minimalist two-level foundation for constructive mathematics.Maria Emilia Maietti - 2009 - Annals of Pure and Applied Logic 160 (3):319-354.
The axiom of choice.John L. Bell - 2008 - Stanford Encyclopedia of Philosophy.
The associated sheaf functor theorem in algebraic set theory.Nicola Gambino - 2008 - Annals of Pure and Applied Logic 156 (1):68-77.
Rudimentary and arithmetical constructive set theory.Peter Aczel - 2013 - Annals of Pure and Applied Logic 164 (4):396-415.

View all 8 citations / Add more citations

References found in this work

The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Inductively generated formal topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - Annals of Pure and Applied Logic 124 (1-3):71-106.
Wellfounded trees in categories.Ieke Moerdijk & Erik Palmgren - 2000 - Annals of Pure and Applied Logic 104 (1-3):189-218.
Independence results around constructive ZF.Robert S. Lubarsky - 2005 - Annals of Pure and Applied Logic 132 (2-3):209-225.

View all 10 references / Add more references