Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Discernment is all you need

David Fuenmayor

TL;DR

This work argues 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, and emphasizes the essential role of discernment, the ability to tell things apart, as a language primitive.

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.

Discernment is all you need

TL;DR

This work argues 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, and emphasizes the essential role of discernment, the ability to tell things apart, as a language primitive.

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.
Paper Structure (11 sections, 38 equations, 1 figure)

This paper contains 11 sections, 38 equations, 1 figure.

Table of Contents

  1. Funktionenkalkül and Logical Incompatibility
  2. Logic in Typed $\lambda$-Calculi
  3. The Simple Theory of Types
  4. The Simply-Typed Lambda Calculus
  5. Equality as Primitive and the System $\mathcal{Q}_0$
  6. HOL as an Universal (Meta-)Language
  7. What is HOL?
  8. On Completeness
  9. Modal and Non-classical Logics in HOL
  10. A Recipe for Encoding Logics in HOL
  11. Discernment and Duality: Prospects

Figures (1)

  • Figure 1: Informal grammar for STT types and terms.