We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Lof type theory The original interpretation treated logic in Martin-Lof type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Lof 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.

ACZEL, P., GAMBINO, N. (2006). The generalised type-theoretic interpretation of constructive set theory. THE JOURNAL OF SYMBOLIC LOGIC, 71(1), 67-103 [10.2178/jsl/1140641163].

The generalised type-theoretic interpretation of constructive set theory

GAMBINO, Nicola
2006-01-01

Abstract

We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Lof type theory The original interpretation treated logic in Martin-Lof type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Lof 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.
2006
ACZEL, P., GAMBINO, N. (2006). The generalised type-theoretic interpretation of constructive set theory. THE JOURNAL OF SYMBOLIC LOGIC, 71(1), 67-103 [10.2178/jsl/1140641163].
File in questo prodotto:
File Dimensione Formato  
TheGeneralisedTypeTheoreticInterpretationOfConstructiveSetTheory.pdf

Solo gestori archvio

Dimensione 2.33 MB
Formato Adobe PDF
2.33 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10447/40057
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 20
  • ???jsp.display-item.citation.isi??? 18
social impact