The generalised type-theoretic interpretation of constructive set theory

Nicola Gambino, Nicola Gambino, Peter Aczel

Risultato della ricerca: Articlepeer review

15 Citazioni (Scopus)

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.
Lingua originaleEnglish
pagine (da-a)67-103
Numero di pagine36
RivistaTHE JOURNAL OF SYMBOLIC LOGIC
Volume71
Stato di pubblicazionePublished - 2006

All Science Journal Classification (ASJC) codes

  • Philosophy
  • Logic

Fingerprint Entra nei temi di ricerca di 'The generalised type-theoretic interpretation of constructive set theory'. Insieme formano una fingerprint unica.

Cita questo