Derived rules for predicative set theory: an application of sheaves

DOI10.1016/J.APAL.2012.01.010zbMATH Open1432.03128arXiv1009.3553OpenAlexW2143931279MaRDI QIDQ448333FDOQ448333

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)

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.

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

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

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)

Cites Work

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

Cited In (4)

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

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)