| |
VOLUME 3, ISSUE 3, PAPER 6
|
A Normalizing Intuitionistic Set Theory with Inaccessible Sets
|
©Wojciech Moczydłowski, Cornell University
|
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 ω-many inaccessibles, which we
call IZFRω. Our axiomatization 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 corresponding to proofs in IZFRω
according to the Curry-Howard isomorphism principle. We use realizability to
prove the normalization theorem, which provides a basis for program extraction
capability.
|
Publication date: August 16, 2007
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-3(3:6)2007
Hit Counts: 2006 |
 Creative Commons | |
