Derived rules for predicative set theory: an application of sheaves
Logic
2011-11-17 v2 Category Theory
Abstract
We show how one may establish proof-theoretic results for constructive Zermelo-Fraenkel set theory, such as the compactness rule for Cantor space and the Bar Induction rule for Baire space, by constructing sheaf models and using their preservation properties.
Cite
@article{arxiv.1009.3553,
title = {Derived rules for predicative set theory: an application of sheaves},
author = {Benno van den Berg and Ieke Moerdijk},
journal= {arXiv preprint arXiv:1009.3553},
year = {2011}
}