Strong and Weak Completeness in Classical Higher-Order Logic

1. Why This Matters

In first-order logic (FOL), Gödel’s Completeness Theorem guarantees harmony between truth and proof: anything true in every model is derivable. Step into higher-order logic (HOL)—where we quantify over predicates, functions, and higher-type objects—and that harmony breaks. This post explains why, and how different semantics change the picture.

2. What Counts as “Classical” HOL? (Syntax)

We use a simple typed setup. Base types: e for individuals, t for truth values. If α and β are types, then α → β is a function type (arrow is right-associative).

• Terms: variables xα, constants cα, application (MN), abstraction (λxα.M).
• Logical symbols: ¬, ∧, ∨, → at type t; quantifiers ∀α, ∃α for each type α.

Intuition: HOL is “FOL with more places to point quantifiers”—not just at objects, but at sets of objects, sets of sets, functions on functions, and so on up the type ladder.

3. Two Ways to Read the Quantifiers (Semantics)

The meaning of HOL depends on what the higher-type quantifiers range over:

1. Standard (full) semantics: a type α → β ranges over all functions from Dα to Dβ (e.g., e → t ranges over the full powerset of individuals).
2. Henkin (general) semantics: quantifiers range over a designated collection of relations/functions at each type—large enough for comprehension, but not necessarily the full set.

Standard semantics are maximally expressive; Henkin semantics are intentionally modest—and that modesty will restore completeness.

4. Completeness: Strong vs. Weak

Let Γ be a set of sentences and φ a sentence.

• Strong completeness: if Γ ⊨ φ (every model of Γ satisfies φ), then Γ ⊢ φ (there is a derivation from Γ to φ).
• Weak completeness: if ⊨ φ (valid in all models), then ⊢ φ.

In FOL, Gödel gives both at once. In HOL, under standard semantics, both fail. Under Henkin semantics, both are recovered.

5. Why Completeness Breaks in Standard HOL

• Expressive strength: standard HOL can define a truth predicate for arithmetic. By Tarski’s undefinability theorem, no effective proof system can capture all such validities (they aren’t even recursively enumerable).
• Non-compactness: there exist HOL theories where every finite subset has a model, but the full set does not. No finitary system can be strongly complete for a non-compact logic.

6. The Henkin Escape Route

Henkin’s 1950 insight: treat HOL with general (Henkin) models so higher-type quantifiers range over designated collections. Then HOL behaves like many-sorted FOL: compactness and both strong and weak completeness are restored.

7. The Big Picture

8. Closing Thoughts

Completeness in HOL isn’t a single switch. The strong and weak forms measure how tightly proof tracks truth; standard HOL breaks both, while Henkin’s general models restore them by tempering quantifier ranges. It’s the classic trade-off: expressiveness vs. meta-theoretic guarantees.