Gödel's Completeness Theorem

MiniSat decides the satisfiability of formulas with millions of variables. Z3 verifies that a Microsoft kernel driver is bug-free. Prolog answers queries by searching for proofs. Each of these tools relies on a single 1929 theorem by a 23-year-old: every truth has a finite proof. Without that guarantee, automated reasoning would be a guessing game. The lesson dissects why this works - and why arithmetic itself escapes the same guarantee.

• **SAT solvers (CDCL):** complete for propositional logic. MiniSat handles millions of variables - hardware verification at Intel, AMD
• **Z3 SMT (Microsoft):** complete for linear arithmetic, arrays, bitvectors. Powers Dafny, F* for correctness proofs in production code
• **TLA+ (Lamport):** finite-state model checking - complete verification. Amazon uses it for Dynamo, S3 protocol validation

Предварительные знания

• Formal systems and the notion of derivation (⊢)
• Semantics: models, truth of a formula in an interpretation (⊨)

• Formal Systems

Soundness and Completeness: two different questions

Gödel proved two theorems with similar names but opposite meanings. The COMPLETENESS theorem (1929, age 23): first-order logic is complete - everything true is provable. The INcompleteness theorems (1931, age 25): Peano Arithmetic is incomplete - there exist truths that are unprovable. One name, two years, two theorems. The confusion between them is the most common error when reading logic.

**Soundness:** if provable, then true ⊢ φ ⟹ ⊨ φ **Completeness:** if true in all models, then provable ⊨ φ ⟹ ⊢ φ Gödel's Completeness Theorem (1929): both directions hold for first-order logic: ⊢ φ ⟺ ⊨ φ

A CDCL SAT solver is a complete algorithm for propositional logic: if a formula is satisfiable it finds a witness; if unsatisfiable it proves it. Prolog (SLD-resolution) is complete for Horn clauses but not for full first-order logic. Z3 SMT is complete for many theories (linear arithmetic, arrays, bitvectors). All of them are practical implementations of Gödel's completeness theorem in specific fragments.

**To keep them straight:** soundness looks left (from syntax to semantics), completeness looks right. They sound similar, but the arrows point opposite ways. Most systems are sound by construction. Completeness is rare and usually expensive - undecidable for rich enough theories.

Gödel's Completeness Theorem: statement and consequences

1929. Kurt Gödel. Age 23. His dissertation in Vienna: first-order logic is complete - if a formula is true in every model, it is provable from the axioms. Two years later - the incompleteness theorems. One person, two years, two results that changed mathematics and computer science permanently. And they are not the same result.

**Gödel's Completeness Theorem (1929):** For a formula φ in first-order logic: ⊢ φ if and only if ⊨ φ **Equivalent formulation via consistency:** Theory T is consistent ⟺ T has a model **Consequence for automated reasoning:** If φ logically follows from axioms T (T ⊨ φ), a finite derivation T ⊢ φ exists. Robinson's resolution algorithm (1965) will find it - in finite time.

Completeness is not the same as decidability. First-order logic is complete (every tautology is provable) but only semi-decidable: an algorithm will halt and say yes for any true formula, but for a false one it may run forever. This is why automated theorem provers (Lean, Coq, Isabelle) require human guidance: completeness guarantees that a proof exists, not that it will be found in reasonable time.

Completeness for Propositional Logic: SAT solvers

For propositional logic, completeness is not an abstraction - it is deployed software. The DPLL algorithm (1960) and its descendant CDCL (Conflict-Driven Clause Learning, 1990s) are complete: for any propositional formula they either return SAT with a witness or UNSAT with a refutation proof. MiniSat demonstrated in 2003 that this scales to millions of variables.

The Compactness Theorem follows from completeness. An infinite set of formulas is satisfiable if and only if every finite subset is satisfiable. In practice this allows constructing non-standard models of arithmetic: add a constant c and infinitely many axioms c > 0, c > 1, c > 2, ... Every finite subset is satisfiable (interpret c as a sufficiently large natural number in the standard model). By compactness the whole set is satisfiable - a model containing an element larger than every standard natural number.

Completeness (1929) vs Incompleteness (1931): a sharp distinction

First-order logic is complete. Peano Arithmetic is incomplete. There is no contradiction here - these are two different objects. The completeness theorem talks about logic as a derivation mechanism. The incompleteness theorems talk about a specific theory (PA) as a set of axioms. Understanding the difference means understanding the structure of mathematics.

The Löwenheim-Skolem theorem adds another layer. If a countable first-order theory has an infinite model it has a countable model. ZFC proves the existence of uncountable sets. But ZFC has a countable model - Skolem's model. In it, the 'uncountable' set (say R) is externally countable - the bijection with the naturals simply does not exist inside the model. The concepts 'countable' and 'uncountable' depend on which model one is looking from.

Key Ideas

• **Soundness:** ⊢ φ ⟹ ⊨ φ. Provable implies true. Checked by induction on the derivation
• **Completeness:** ⊨ φ ⟹ ⊢ φ. True in all models implies provable. Gödel's theorem 1929
• **Model-theoretic equivalent:** T is consistent if and only if T has a model. The key consequence for SAT solvers
• **In practice:** CDCL SAT - complete for PL; SLD-resolution - complete for Horn clauses; Z3 SMT - complete for its theories
• **Completeness ≠ Incompleteness:** FOL is complete as a derivation mechanism; PA is incomplete as a theory. Different objects, different claims
• **Löwenheim-Skolem:** the natural numbers escape FOL - any axiomatization with model N also has non-standard models of every infinite cardinality

Toward the Incompleteness Theorems

The completeness theorem is a positive result for FOL as a whole. For specific theories Gödel proved something fundamentally different:

• First Incompleteness Theorem — There exists φ such that PA ⊭ φ and PA ⊭ ¬φ - true but unprovable
• Second Incompleteness Theorem — PA cannot prove its own consistency (if it is consistent)

Вопросы для размышления

• If first-order logic is complete, why do automated theorem provers (Lean, Coq) require human guidance?
• What is the meaning of Skolem's paradox? Why is it not a genuine contradiction?
• TypeScript does not have a complete type system: there are programs that will not crash but fail to type-check. Which term from this lesson describes that property?

Связанные уроки

• ml-04 — Formal systems and the notion of derivation - without these the completeness theorem cannot be stated
• ml-06 — First incompleteness theorem - the main contrast: completeness (1929) vs incompleteness (1931)
• dm-05 — Combinatorics of model spaces: countable vs uncountable, birthday problem for logical structures
• prob-04-bayes — Bayesian update as semantic consequence: prior + evidence = posterior; axioms + derivation = theorem
• fl-22-decidability