The Herbrand Topos
classification
🧮 math.CT
math.LO
keywords
herbrandtoposcategoryrealizabilityadditionassembliescharacterisedefine
read the original 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.
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.