Derived rules for predicative set theory: an application of sheaves

DOI10.1016/J.APAL.2012.01.010MaRDI QIDQ448333zbMATH OpenOpenAlexFDO

Authors Benno van den Berg, Ieke Moerdijk

Publication date 6 September 2012

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1009.3553

zbMATH Keywords

Baire spacesheavesconstructive set theoryderived rules

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Metamathematics of constructive systems (03F50) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20)

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.

Recommendations

• The axiom of multiple choice and models for constructive set theory
• Aspects of predicative algebraic set theory. III: Sheaves
• scientific article; zbMATH DE number 2172973
• Aspects of predicative algebraic set theory. I: Exact completion
• The disjunction and related properties for constructive Zermelo-Fraenkel set theory

Cites work

• scientific article; zbMATH DE number 2184445 (Why is no real title available?)
• scientific article; zbMATH DE number 3839951 (Why is no real title available?)
• scientific article; zbMATH DE number 3853067 (Why is no real title available?)
• scientific article; zbMATH DE number 3811561 (Why is no real title available?)
• scientific article; zbMATH DE number 3916267 (Why is no real title available?)
• scientific article; zbMATH DE number 3918365 (Why is no real title available?)
• scientific article; zbMATH DE number 4012604 (Why is no real title available?)
• scientific article; zbMATH DE number 3664922 (Why is no real title available?)
• scientific article; zbMATH DE number 3754682 (Why is no real title available?)
• scientific article; zbMATH DE number 3787631 (Why is no real title available?)
• A note on Bar Induction in Constructive Set Theory
• Aspects of general topology in constructive set theory
• Aspects of predicative algebraic set theory. I: Exact completion
• Aspects of predicative algebraic set theory. II: Realizability
• Constructivism in mathematics. An introduction. Volume I
• Derived rules related to a constructive theory of metric spaces in intuitionistic higher order arithmetic without countable choice
• Forcing in intuitionistic systems without power-set
• Heine-Borel does not imply the Fan Theorem
• Heyting-valued interpretations for constructive set theory
• Inductive types and exact completion
• Inductively generated formal topologies.
• Principles of continuous choice and continuity of functions in formal systems for constructive mathematics
• Sheaves in geometry and logic: a first introduction to topos theory
• Some points in formal topology.
• The axiom of multiple choice and models for constructive set theory
• The disjunction and related properties for constructive Zermelo-Fraenkel set theory
• Type theories, toposes and constructive set theory: Predicative aspects of AST
• W-types in homotopy type theory
• Wellfounded trees in categories

Cited in

(4)

• Non-deterministic inductive definitions
• Formally continuous functions on Baire space
• THE FIRST-ORDER LOGIC OF CZF IS INTUITIONISTIC FIRST-ORDER LOGIC
• The axiom of multiple choice and models for constructive set theory

This page was built for publication: Derived rules for predicative set theory: an application of sheaves

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q448333)