A deep embedding of HOL in HOL: soundness, completeness, consistency

This entry presents a minimal, machine-checked deep embedding of classical higher-order logic (HOL) in Isabelle/HOL, following the article Higher-Order Semantics and Extensionality by Benzmüller, Brown and Kohlhase (Journal of Symbolic Logic 69(4), 2004; henceforth BKK). Throughout, HOL means Church's simple theory of types: it is the embedded object logic, while Isabelle/HOL serves as the ambient meta-logic. The language of BKK §2 is formalised in a locally nameless representation, which makes BKK's identification of α-equivalent terms literally true; no α-conversion or bound-variable renaming is ever needed. The semantics of BKK §3 is rendered abstractly, up to the class M_βfb of Σ-Henkin models; standard models arise as the full special case.

On this basis the natural-deduction calculus NK of BKK §7 is proved sound (Theorem 7.3) and Henkin-complete, via the model-existence method of BKK §6, with the term model realised as a term evaluation. Completeness holds in a form stronger than BKK's Corollary 7.7: at every infinite value carrier, for every signature with infinitely many parameters, and for open formulas. It also holds relative to hypotheses. For derivability from hypotheses in Andrews' sense — some finite part of the hypothesis set (the context) derives the conclusion — any context of open formulas is admitted, at any signature cardinality (any parameter type of the meta-logic), once the carrier is at least as large as the signature; semantic compactness of the Henkin consequence follows. For the calculus itself, a finite context needs nothing beyond well-formedness, and a pure context of open formulas is admitted over a countable signature at every infinite carrier. Consistency — that ⊥ is not derivable — follows from a concrete Σ-standard model with finite domains: a single individual and finitely many non-logical constants suffice, so no axiom of infinity is assumed for the embedded logic. Model existence is likewise concrete: from the consistency of a sentence over a countable signature, a countable Henkin (general) model of it is defined outright in plain HOL — non-effectively, via a maximal-consistent extension, but with consistency as the only premise. The signature includes BKK's optional primitive equality (Remark 7.9) and — going beyond BKK, following Andrews' General Models, Descriptions, and Choice in Type Theory (1972) — typed description operators. As an illustration, Cantor's theorem is derived inside NK, in surjective and injective form and at every type. Finally, by compactness over arbitrarily large finite models, NK is shown consistent with a schematic diagram forcing infinitely many individuals — no infinite model is constructed (Andrews' route) — and the single Dedekind-style axiom of infinity is shown not to follow from that scheme: no finite part of the scheme derives it, and a countable Henkin model of the whole scheme refutes it. To the best of our knowledge, this is the first machine-checked completeness proof for a deep embedding of HOL in HOL. This contribution is part of the LogiKEy project.