Paper: A Dependent Set Theory (at LICS 2007)

Authors: 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}
  }