Abstract
This entry presents a 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 a literal equality, so that no α-conversion or bound-variable renaming is 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. The signature includes BKK's optional primitive equality (Remark 7.9) and — following Andrews' General Models, Descriptions, and Choice in Type Theory (1972), beyond BKK — typed description operators.
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, over any infinite signature, 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 over a countable signature a context of open formulas that leaves infinitely many parameters unused is admitted 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 Henkin (general) model of it with countable total domain is defined in plain HOL — non-effectively, via a maximal-consistent extension, but with consistency as the only premise.
As an illustration, Cantor's theorem is derived inside NK, in surjective and injective form and at every type. Finally, two syntactic renderings of infinity are compared with each other and with semantic infinitude. The constant-free first-order sentences "there are at least n individuals" — the axiomatisation of "the domain is infinite" in the language of equality — are consistent with NK, by compactness over arbitrarily large finite models: the consistency proof constructs no infinite model. The single Dedekind-style axiom of infinity derives each of these sentences, but they do not derive the axiom: no finite part of them does, and a Henkin model of them all, countable over a countable signature, refutes it. To the best of our knowledge, this is the first machine-checked completeness proof for a deep embedding of HOL over plain HOL. This contribution is part of the LogiKEy project.
License
Note
Parts of this formalisation and its documentation were drafted interactively with a generative AI assistant (Anthropic's Claude), used under continuous human direction. All proofs are machine-checked by Isabelle; the entire development, including all comments and references, was subsequently reviewed, revised and simplified by the authors, who take full responsibility for its content.
History
- September 29, 2026
- Major extension. Completeness is strengthened to derivation from hypotheses: up to arbitrary pure contexts of open formulas over countable signatures at every infinite carrier, and, by a transfinite extension lemma, to arbitrary signature cardinalities, with the carrier at least as large as the signature and purity scaled to it. A finitary hypothesis relation in the style of Andrews (some finite sub-context derives the conclusion) is introduced, for which completeness needs no purity condition at all; semantic compactness of the Henkin consequence follows as a corollary. Further additions (theory NK_Infinity): consistency of NK with a scheme of inequations between new individual constants, by compactness over finite models, also in the finitary form; the Dedekind axiom of infinity DInf with its satisfaction conditions in any general model; the axiom derives every constant-free sentence 'there are at least n individuals' inside NK, these sentences are consistent with NK, and neither the constant scheme nor these sentences derive the axiom: a Henkin model of them all, countable over a countable signature, refutes it; model existence as a concrete countable Henkin model; a footprint audit (theory Footprint_Checks). Derived rules for conjunction, the named binders and cut are added to Calculus. The published exports (including cantor_surjective and cantor_injective) are preserved; the document gained an introduction section.
Topics
Related publications
- Benzmüller, C., Brown, C. E., & Kohlhase, M. (2004). Higher-order semantics and extensionality. Journal of Symbolic Logic, 69(4), 1027–1088. https://doi.org/10.2178/jsl/1102022211
Session HOL_in_HOL_Deep
- Syntax
- Semantics
- Calculus
- Soundness
- Completeness
- Consistency
- NK_Infinity
- Cantor
- Main_Results
- Footprint_Checks