Moczydlowski, Wojciech - A Normalizing Intuitionistic Set Theory with Inaccessible Sets

lmcs:837 - Logical Methods in Computer Science, August 16, 2007, Volume 3, Issue 3
A Normalizing Intuitionistic Set Theory with Inaccessible Sets

Authors: Moczydlowski, Wojciech

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 its constructive proofs. For this purpose, we axiomatize an impredicative constructive version of Zermelo-Fraenkel set theory IZF with Replacement and $\omega$-many inaccessibles, which we call \izfio. Our axiomatization utilizes set terms, an inductive definition of inaccessible sets and the mutually recursive nature of equality and membership relations. It allows us to define a weakly-normalizing typed lambda calculus corresponding to proofs in \izfio according to the Curry-Howard isomorphism principle. We use realizability to prove the normalization theorem, which provides a basis for program extraction capability.


Source : oai:arXiv.org:0707.1981
DOI : 10.2168/LMCS-3(3:6)2007
Volume: Volume 3, Issue 3
Published on: August 16, 2007
Submitted on: October 13, 2006
Keywords: Computer Science - Logic in Computer Science,F.4.1


Share

Consultation statistics

This page has been seen 60 times.
This article's PDF has been downloaded 77 times.