
TL;DR
This paper investigates the expressive capabilities of higher-order logic (HOL), emphasizing discernment as a key primitive, and demonstrates HOL's potential as a unifying framework for various logical systems including modal and non-classical logics.
Contribution
It introduces the concept of discernment as a primitive in HOL, enhancing its expressivity and theoretical robustness, and explores HOL's capacity to encode diverse logical systems.
Findings
HOL can encode a wide range of logical systems
Discernment as a primitive enhances HOL's expressivity
HOL serves as a unifying logical framework
Abstract
We explore the expressive power of HOL, a system of higher-order logic, and its relationship to the simply-typed lambda calculus and Church's simple theory of types, arguing for the potential of HOL as a unifying logical framework, capable of encoding a broad range of logical systems, including modal and non-classical logics. Along the way, we emphasize the essential role of discernment, the ability to tell things apart, as a language primitive; highlighting how it endows HOL with practical expressivity superpowers while elegantly enriching its theoretical properties.
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 · Logic, Reasoning, and Knowledge · Philosophy and Theoretical Science
