unofficial copies [PDF],

by Wojciech Moczydlowski

Proceedings of Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007.

**Abstract**

Set theories are traditionally based on first-order logic. We
show that in a constructive setting, basing a set theory on a dependent logic
yields many benefits. To this end, we introduce a dependent impredicative
constructive set theory which we call IZFD.
Using realizability, we prove that* *the underlying lambda calculus weakly
normalizes, thus enabling program extraction from IZFD
proofs. We also show that IZFD
can interpret IZF with Collection. By a well
known result of Friedman, this establishes IZFD
as a remarkably strong theory, with
proof-theoretical power equal to that of ZFC. We further demonstrate that IZFD
provides a natural framework to interpret
first-order definitions, thus removing a longstanding barrier to implementing
constructive set theories. Finally, we prove that IZFD
extended with excluded middle is consistent,
thus paving the way to using our framework in the classical setting as well.