## Paper: A Dependent Set Theory (at LICS 2007)

**Wojciech Moczydlowski**

### 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 IZF_D. Using realizability, we prove that the underlying lambda calculus weakly normalizes, thus enabling program extraction from IZF_D proofs. We also show that IZF_D can interpret IZF with Collection. By a wellknown result of Friedman, this establishes IZF_D as a remarkably strong theory, with proof-theoretical power equal to that of ZFC. We further demonstrate that IZF_D provides a natural framework to interpret first-order definitions, thus removing a longstanding barrier to implementing constructive set theories. Finally, we prove that IZF_D extended with excluded middle is consistent, thus paving the way to using our framework in the classical setting as well.

### BibTeX

@InProceedings{Moczydlowski-ADependentSetTheory, author = {Wojciech Moczydlowski}, title = {A Dependent Set Theory}, booktitle = {Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)}, year = {2007}, month = {July}, pages = {23--34}, location = {Wroclaw, Poland}, publisher = {IEEE Computer Society Press} }