Completeness of the first-order natural deduction calculus (OPEN in this ledger)

Identifier: F:fo-completeness-henkin
Proof route: Not assigned
External status: proved
Axiom footprint: Empty

Recorded description

If every structure and valuation satisfying a context satisfies a formula, then the formula is derivable from that context in FO.Provable. NOT ESTABLISHED HERE. The converse -- soundness -- IS established (F:fo-soundness), together with the substitution lemma the quantifier rules rest on (F:fo-substitution-lemma) and the consistency corollary soundness buys (F:fo-consistency). What is missing is the Henkin/Lindenbaum construction: a maximal consistent extension of the context in a language with witnesses, and the term model built over it. Two obstructions are recorded rather than estimated. (1) Lindenbaum's lemma extends a consistent set to a MAXIMAL consistent one by deciding each formula in an enumeration, which is a use of excluded middle at every step; this kernel has no Classical.em, no propext and no Quot.sound (measured: crates/axeyum-lean-kernel/src/prelude.rs), so the classical completeness theorem is not the statement to aim at without first adding an axiom the project's axiom-freedom metric would then have to report. (2) The construction needs an enumeration of FO.Formula and a decidable equality on it, neither of which exists in the kernel; FO.Formula is an inductive with nine constructors over two carriers (AxNat and FO.Term), so a decidable equality is a nested recursion over both types, and no such decision procedure was built by the lane that landed the syntax.

Formal statement

theorem FO.completeness : ((x0 : FO.Context) -> ((x1 : FO.Formula) -> ((x2 : ((x3 : Sort (1)) -> ((x4 : FO.Structure x3) -> ((x5 : ((x6 : AxNat) -> x3)) -> ((x7 : FO.ctxSat x3 x4 x0 x5) -> FO.sat x3 x4 x1 x5))))) -> FO.Provable x0 x1)))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

4 direct dependencies 0 direct dependents

Evidence

Provenance

{
  "date": "2026-09-05",
  "curation": "curated",
  "established_by": "not established in this ledger",
  "source": "Goedel's completeness theorem (1929); this row records the measured remaining gap after lane model-theory landed the syntax, the semantics, the calculus and soundness (W3-6, ADR-1636)",
  "prior_art": [
    {
      "who": "Kurt Goedel; Leon Henkin",
      "what": "the completeness theorem for first-order logic, and the maximal-consistent-set proof that is now standard",
      "year": 1949,
      "where": "Goedel 1929 (dissertation); Henkin, 'The completeness of the first-order functional calculus', JSL 14 (1949)",
      "attribution": "standard textbook attribution; this lane did not consult the primary sources"
    }
  ]
}