Derived rules for predicative set theory: An application of sheaves

作者：van den Berg Benno^*; Moerdijk Ieke

来源：Annals of Pure and Applied Logic, 2012, 163(10): 1367-1383.

DOI：10.1016/j.apal.2012.01.010

• Constructive set theory
• Derived rules
• Sheaves
• Baire space

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.

• 出版日期2012-10