Derived rules for predicative set theory: an application of sheaves

TL;DR

This paper demonstrates how to establish proof-theoretic results for constructive Zermelo-Fraenkel set theory using sheaf models, highlighting their preservation properties for rules like compactness and Bar Induction.

Contribution

It introduces a novel application of sheaf models to prove key results in constructive set theory, bridging model theory and proof theory.

Findings

Sheaf models preserve proof-theoretic properties in constructive set theory.

Proof of compactness rule for Cantor space using sheaf models.

Validation of Bar Induction rule for Baire space via sheaf constructions.

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.