Logic in Computer Science, Symposium on (2007)
July 10, 2007 to July 14, 2007
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2007.7
Wojciech Moczydlowski , Cornell University, USA
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.
W. Moczydlowski, "A Dependent Set Theory," 2007 22nd Annual IEEE Symposium on Logic in Computer Science(LICS), Wroclaw, 2007, pp. 23-34.