A Dependent Set Theory

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.