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.

翻译：本文探讨了高阶逻辑系统HOL的表达能力及其与简单类型lambda演算和Church简单类型论的关系，论证了HOL作为统一逻辑框架的潜力，该框架能够编码包括模态逻辑和非经典逻辑在内的广泛逻辑系统。在此过程中，我们强调辨别力——区分事物的能力——作为语言原语的核心作用；阐明它如何既赋予HOL实用的超强表达能力，又优雅地丰富了其理论性质。