HOL in HOL over a set-theoretic universe: consistency of NK with infinity and choice

This companion to the entry A deep embedding of HOL in HOL certifies the natural-deduction calculus NK of that entry consistent with a genuine Dedekind-style axiom of infinity — an injective, non-surjective self-map of the individuals — and, because its standard model has full function spaces, with the relational axiom of choice as well. Such an axiom has no finite models, so the compactness argument of the main entry — which lifts arbitrarily large finite models to an infinity scheme — does not apply: a genuinely infinite model is required. We construct one over Paulson's ZFC_in_HOL: the individuals are interpreted as the finite ordinals ω, with full function spaces at every type, yielding a standard Σ-model of NK over the set-theoretic universe V. As this meta-theory is stronger and non-conservative, the guarantee is relative consistency at ZF strength; the machine-checked formalisation lives in Isabelle/HOL with Paulson's ZFC_in_HOL (the ZF reading is metatheoretic, made precise in the introduction). Because NK already provides extensionality and typed description (after Andrews), this certifies the consistency of full classical higher-order logic in Church's sense, choice included as a separate relational scheme.

The infinity axiom and the weaker infinity scheme of the main entry turn out to be logically independent. That the scheme does not entail the axiom is shown in the main entry; the present entry settles the other direction, since the axiom does not entail any of the scheme's individual inequalities: its set-theoretic model interprets all individual constants alike, so those inequalities fail while the axiom holds. Neither sentence, then, implies the other.

The plain-HOL results — soundness, Henkin completeness, and finite-model consistency, including the compactness route to the infinity scheme — are proved in the main entry and imported here unchanged. What the present entry adds is the set-theoretic route to axioms that plain HOL alone cannot model.

This contribution is part of the LogiKEy project.