JavaScript is disabled for your browser. Some features of this site may not work without it.
A Normalizing Intuitionistic Set Theory with Inaccessible Sets

Author
Moczydlowski, Wojciech
Abstract
We propose a set theory strong enough to interpret powerful type
theories underlying proof assistants such as LEGO and also possibly Coq, which at the same time enables program extraction from constructive proofs. For this purpose, we axiomatize impredicative constructive version of Zermelo-Fraenkel set theory IZF with Replacement and $\omega$-many inaccessibles, which we call IZF_{R\omega}. Our axiomatization of IZF_{R\omega} utilizes set terms, an inductive definition of inaccessible sets and mutually recursive nature of equality and membership relations. It allows us to define a weakly-normalizing typed lambda calculus \lambda Z_\omega corresponding to proofs in IZF_{R\omega} according to the Curry-Howard isomorphism principle. We use realizability to prove the normalization theorem, which provides basis for extracting programs from IZF_{R\omega} proofs.
Date Issued
2006-10-11Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2006-2051
Type
technical report