The Generalised Type-Theoretic Interpretation of Constructive Set Theory

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

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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2178/jsl/1140641163
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: 39,024
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

Inductively Generated Formal Topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - Annals of Pure and Applied Logic 124 (1-3):71-106.
The Strength of Some Martin-Löf Type Theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Heyting-Valued Interpretations for Constructive Set Theory.Nicola Gambino - 2006 - Annals of Pure and Applied Logic 137 (1):164-188.
Independence Results Around Constructive ZF.Robert S. Lubarsky - 2005 - Annals of Pure and Applied Logic 132 (2-3):209-225.

View all 8 references / Add more references

Citations of this work BETA

A Minimalist Two-Level Foundation for Constructive Mathematics.Maria Emilia Maietti - 2009 - Annals of Pure and Applied Logic 160 (3):319-354.
The Associated Sheaf Functor Theorem in Algebraic Set Theory.Nicola Gambino - 2008 - Annals of Pure and Applied Logic 156 (1):68-77.
Lawvere-Tierney Sheaves in Algebraic Set Theory.S. Awodey, N. Gambino & M. A. Warren - 2009 - Journal of Symbolic Logic 74 (3):861 - 890.
Rudimentary and Arithmetical Constructive Set Theory.Peter Aczel - 2013 - Annals of Pure and Applied Logic 164 (4):396-415.
Classical Predicative Logic-Enriched Type Theories.Robin Adams & Zhaohui Luo - 2010 - Annals of Pure and Applied Logic 161 (11):1315-1345.

Add more citations

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.


Added to PP index

Total views
32 ( #229,244 of 2,320,210 )

Recent downloads (6 months)
10 ( #104,594 of 2,320,210 )

How can I increase my downloads?

Monthly downloads

My notes

Sign in to use this feature