TL;DR
The paper introduces the Herbrand topos, a new mathematical structure inspired by realizability concepts, and explores its properties, including the category of Herbrand assemblies and their relation to double-negation separation.
Contribution
It defines the Herbrand topos, characterizes Herbrand assemblies, and establishes their relation to double-negation-separated objects and the category of sets.
Findings
Herbrand topos is a new topos inspired by realizability.
Herbrand assemblies are characterized as double-negation-separated objects.
The category of sets embeds into the Herbrand topos as double-negation-sheaves.
Abstract
We define a new topos, the Herbrand topos, inspired by the modified realizability topos and our earlier work on Herbrand realizability. We also introduce the category of Herbrand assemblies and characterise these as the double-negation-separated objects in the Herbrand topos. In addition, we show that the category of sets is included as the category of double-negation-sheaves and prove that the inclusion functor preserves and reflects validity of first-order formulas.
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
TopicsHomotopy and Cohomology in Algebraic Topology · Logic, programming, and type systems · Constraint Satisfaction and Optimization