Wojciech Moczydlowski - Normalization of IZF with Replacement

lmcs:1235 - Logical Methods in Computer Science, April 8, 2008, Volume 4, Issue 2 - https://doi.org/10.2168/LMCS-4(2:1)2008
Normalization of IZF with ReplacementArticle

Authors: Wojciech Moczydlowski

    ZF is a well investigated impredicative constructive version of Zermelo-Fraenkel set theory. Using set terms, we axiomatize IZF with Replacement, which we call \izfr, along with its intensional counterpart \iizfr. We define a typed lambda calculus $\li$ corresponding to proofs in \iizfr according to the Curry-Howard isomorphism principle. Using realizability for \iizfr, we show weak normalization of $\li$. We use normalization to prove the disjunction, numerical existence and term existence properties. An inner extensional model is used to show these properties, along with the set existence property, for full, extensional \izfr.


    Volume: Volume 4, Issue 2
    Published on: April 8, 2008
    Imported on: January 2, 2007
    Keywords: Computer Science - Logic in Computer Science,F.4.1
    Funding:
      Source : OpenAIRE Graph
    • Integrating Security and Fault Tolerance in Distributed Systems; Funder: National Science Foundation; Code: 0430161
    • Enabling Large-Scale Coherency Among Mathematical Texts in the NSDL; Funder: National Science Foundation; Code: 0333526

    3 Documents citing this article

    Consultation statistics

    This page has been seen 927 times.
    This article's PDF has been downloaded 412 times.