A categorical semantic for the Typed Epsilon Calculus
Fabio Pasquali
TL;DR
This paper demonstrates that boolean categories satisfying the axiom of choice can serve as a categorical semantics for the typed epsilon calculus, linking category theory with logic.
Contribution
It establishes a new semantic foundation for the typed epsilon calculus using boolean categories with AC, bridging logic and category theory.
Findings
Boolean categories with AC provide semantics for typed epsilon calculus
Categorical semantics connects logic and category theory
New foundation for typed epsilon calculus
Abstract
We show that every boolean category satisfying AC provides a categorical semantic of the typed Epsilon calculus.
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
TopicsLogic, programming, and type systems · Advanced Algebra and Logic · Logic, Reasoning, and Knowledge