Discernment is all you need

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.