The Journal of Symbolic Logic

Research Article

The generalised type-theoretic interpretation of constructive set theory

Nicola Gambinoa1 and Peter Aczela2

a1 Laboratoire de Combinatoire et Informatique Mathématique, Université du Québec à Montréal, Case Postale 8888, Succursale Centre-Ville, Montréal (Québec) H3C 3P8, Canada. E-mail:

a2 Schools of Mathematics and Computer Science, University of Manchester, Manchester M13 9Pl, England. E-mail:


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.

(Received June 17 2005)

(Accepted October 20 2005)

Key Words:

  • Key words and phrases. Constructive Set Theory;
  • Dependent Type Theory