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.
| 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.
