A Dependent Set Theory
by Wojciech Moczydlowski
Proceedings of Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007).
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.