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

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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2178/jsl/1140641163
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 53,742
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.
Independence Results Around Constructive ZF.Robert S. Lubarsky - 2005 - Annals of Pure and Applied Logic 132 (2-3):209-225.
Heyting-Valued Interpretations for Constructive Set Theory.Nicola Gambino - 2006 - Annals of Pure and Applied Logic 137 (1):164-188.

View all 10 references / Add more references

Citations of this work BETA

The Axiom of Choice.John L. Bell - 2008 - Stanford Encyclopedia of Philosophy.
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.
Rudimentary and Arithmetical Constructive Set Theory.Peter Aczel - 2013 - Annals of Pure and Applied Logic 164 (4):396-415.

View all 7 citations / 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.

Analytics

Added to PP index
2010-08-24

Total views
33 ( #298,937 of 2,349,843 )

Recent downloads (6 months)
1 ( #511,368 of 2,349,843 )

How can I increase my downloads?

Downloads

My notes