Non-deterministic inductive definitions
Benno van den Berg
TL;DR
This paper introduces non-deterministic inductive definitions as a new proof principle within constructive set theory, with applications to formal topology and a predicative justification.
Contribution
It presents a novel proof principle called non-deterministic inductive definitions and explores its applications and justification in constructive set theory.
Findings
Application to formal topology demonstrated
Provides a predicative justification for the principle
Establishes a new proof method in constructive set theory
Abstract
We study a new proof principle in the context of constructive Zermelo-Fraenkel set theory based on what we will call "non-deterministic inductive definitions". We give applications to formal topology as well as a predicative justification of this principle.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Topology and Set Theory · Homotopy and Cohomology in Algebraic Topology · Philosophy and Theoretical Science