Derived rules for predicative set theory: an application of sheaves
classification
🧮 math.LO
math.CT
keywords
rulespacetheoryapplicationbairecantorcompactnessconstructing
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.