Theorem
Gödel's completeness theorem
Statement
Let \(L\) be a first-order language and let \(\Sigma\) be a set of \(L\)-sentences. If \(\Sigma \models \varphi\) (every \(L\)-structure \(\mathcal{M}\) satisfying all sentences of \(\Sigma\) also satisfies \(\varphi\)), then \(\Sigma \vdash \varphi\) (there is a finite formal derivation of \(\varphi\) from \(\Sigma\) in a sound first-order proof calculus, e.g. a Hilbert system with modus ponens and generalisation, or an equivalent natural-deduction / sequent system). Equivalently, in the special case \(\Sigma = \varnothing\): every logically valid \(L\)-formula (true in every \(L\)-structure under every assignment) is a formal theorem. The standard route to this, and the form actually proved below, is the equivalent statement: every syntactically consistent set of sentences \(\Sigma\) (one from which no contradiction \(\vdash \bot\) is derivable) has a model. This equivalence is itself a short argument: apply it to \(\Sigma \cup \{\neg\varphi\}\), which is inconsistent iff \(\Sigma \vdash \varphi\) (by the deduction theorem and reductio), and inconsistency transfers to unsatisfiability by soundness, contrapositively giving \(\Sigma \models \varphi \Rightarrow \Sigma \vdash \varphi\).
Why it matters
Completeness is the theorem that makes first-order logic a well-behaved foundation for the rest of mathematics: it says the syntactic notion of proof (finite, checkable, purely symbol-pushing) exactly captures the semantic notion of logical truth (a global, in general uncheckable, statement about all structures in the universe of set theory). Without it, "provable" and "true in every model" could diverge, and formal proof would be a merely partial approximation to validity.
It is also the engine behind the compactness theorem, which is the single most-used tool in model theory (nonstandard models of arithmetic and analysis, ultraproducts, saturated models) and which follows from completeness essentially for free, as shown in the Corollaries section.
Hypotheses
The language \(L\) is first-order (quantifiers range only over individuals, not over subsets or relations).
For second-order logic, with quantification over subsets, the analogous completeness theorem is false: the second-order sentence characterising \((\mathbb{N},+,\times)\) up to isomorphism has full second-order semantic consequences (e.g. its own consistency statement, via Gödel's incompleteness argument transplanted to the standard model) that no effective proof system can derive from it, since second-order validity is not even recursively enumerable.
The underlying proof calculus is sound and has the deduction theorem, together with the usual structural rules (finite proofs, weakening/monotonicity of \(\vdash\), reductio ad absurdum).
Drop soundness (e.g. allow modus ponens on false material-conditional readings but keep an unsound extra axiom scheme) and one can derive sentences that fail in some models, so provability no longer implies validity and the "only if" direction collapses; the theorem is stated for a fixed calculus known independently to be sound, and completeness supplies the converse inclusion \(\models\ \subseteq\ \vdash\).
Equality, if present in \(L\), is governed by the standard equality axioms (reflexivity, substitution into atomic formulas).
Without axioms forcing \(=\) to be interpreted as genuine identity, a "model" could interpret \(=\) as an arbitrary equivalence relation, and sentences that are valid under real equality (e.g. \(\forall x\, x = x\) forcing reflexivity of the equality symbol under the intended reading) would fail to be provable from a calculus that never pins the symbol down; the Henkin construction below builds equality classes precisely using these axioms.
\(\Sigma\) is a set of sentences in a language of arbitrary (possibly infinite) cardinality \(\kappa\), and the axiom of choice (or a fragment such as the ultrafilter/Boolean prime ideal theorem) is available in the metatheory.
The construction below performs a transfinite enumeration of all formulas and a language expansion by \(|L|\)-many new constants; for uncountable \(L\) this expansion and the fixed-point closure genuinely need choice to well-order the formulas being processed, and without any choice principle the completeness theorem is known to fail for some infinite languages (it remains provable in ZF for countable \(L\), where the enumeration is explicit).
Proof
We prove the model-existence form: every consistent set of \(L\)-sentences \(\Sigma\) has a model. This is Henkin's method (1949), which builds a model directly out of the syntax rather than arguing by a compactness/ultraproduct route.
1
\text{Add a countably (or } |\Sigma|\text{-)infinite set of new constant symbols } C = \{c_0,c_1,c_2,\dots\} \text{ to } L, \text{ forming } L^+ = L \cup C.
Pure syntax: introducing new nonlogical symbols does not change consistency of \(\Sigma\) over the old language, since any derivation of \(\bot\) in \(L^+\) from \(\Sigma\) can be converted to one in \(L\) by replacing each new constant occurring in the (finite) derivation by a distinct old variable not otherwise used and universally generalising — this is the standard "constants can be replaced by fresh variables" lemma for proof systems with generalisation on variables not free in premises. B
2
\text{For every } L^+\text{-formula } \varphi(x) \text{ with one free variable, fix a "witness" constant } c_\varphi \in C \text{ (distinct for distinct } \varphi\text{), and let}
\Theta = \{\, \exists x\,\varphi(x) \to \varphi(c_\varphi) \;:\; \varphi(x) \text{ an } L^+\text{-formula with one free variable} \,\}.
Definition of a set of Henkin axioms: this is possible because \(C\) is chosen large enough (cardinality \(|L|\)) to index every formula-with-one-free-variable of \(L^+\), which itself has cardinality \(|L|\); a bijective enumeration exists by the axiom of choice for general \(|L|\), explicitly for countable \(L\). B
3
\Sigma \cup \Theta \text{ is consistent.}
Henkin's lemma. Adjoin the witnessing axioms one at a time in the enumeration order \(\varphi_0,\varphi_1,\dots\) of one-free-variable formulas; suppose \(\Sigma \cup \Theta_n\) (the first \(n\) axioms) is consistent but \(\Sigma \cup \Theta_n \cup \{\exists x\,\varphi_n(x) \to \varphi_n(c_{\varphi_n})\}\) is not. Since \(c_{\varphi_n}\) does not occur in \(\Sigma \cup \Theta_n\) or in \(\varphi_n\)'s quantifier prefix binding, inconsistency here forces \(\Sigma \cup \Theta_n \vdash \exists x\,\varphi_n(x)\) and \(\Sigma \cup \Theta_n \vdash \neg\varphi_n(c_{\varphi_n})\); by generalisation on the constant \(c_{\varphi_n}\) (legal exactly because it is fresh — does not occur in \(\Sigma \cup \Theta_n\)) the second gives \(\Sigma \cup \Theta_n \vdash \forall x\,\neg\varphi_n(x)\), contradicting the first. So each finite stage stays consistent, and by the finiteness of derivations (any inconsistency in the union uses only finitely many axioms, hence lives at some finite stage) the whole increasing union \(\Sigma \cup \Theta\) is consistent. C
4
\Sigma \cup \Theta \text{ extends to a maximal consistent set } \Sigma^* \text{ of } L^+\text{-sentences (a "complete theory"): for every sentence } \psi, \text{ either } \psi \in \Sigma^* \text{ or } \neg\psi \in \Sigma^*.
Lindenbaum's lemma: well-order (enumerate, using choice if \(L^+\) is uncountable) all \(L^+\)-sentences \(\psi_0,\psi_1,\dots\) and build an increasing chain \(\Sigma_0 = \Sigma\cup\Theta \subseteq \Sigma_1 \subseteq \cdots\), at stage \(n\) adding \(\psi_n\) if \(\Sigma_n \cup \{\psi_n\}\) is consistent and \(\neg\psi_n\) otherwise. At least one of \(\psi_n,\neg\psi_n\) keeps consistency, else \(\Sigma_n \vdash \neg\psi_n\) and \(\Sigma_n \vdash \psi_n\) would give \(\Sigma_n \vdash \bot\) by modus ponens against consistency of \(\Sigma_n\) (proved by induction using step 3 as the base case). Take \(\Sigma^* = \bigcup_n \Sigma_n\); consistency of the union again follows because any purported contradiction is a finite derivation using finitely many members, hence lying inside some \(\Sigma_n\). B
5
\text{Define, on the set } C \text{ of new constants, } c \sim c' \iff (c = c') \in \Sigma^*. \text{ This is an equivalence relation, and } \Sigma^* \text{ decides, for each closed atomic formula, whether it holds.}
\(\sim\) is reflexive/symmetric/transitive because \(\Sigma^*\) is a maximal consistent set containing the equality axioms (hypothesis above: reflexivity \(\vdash \forall x\, x=x\) puts \(c=c\) in every such theory; symmetry and transitivity are themselves valid equality-axiom consequences, hence provable from \(\Sigma^*\), hence — since \(\Sigma^*\) is deductively closed by maximality plus step 4's completeness — members of \(\Sigma^*\)). Deductive closure of \(\Sigma^*\): if \(\Sigma^* \vdash \chi\) then \(\Sigma^* \cup \{\chi\}\) is consistent (soundness/monotonicity would be violated otherwise), so by maximality \(\chi \in \Sigma^*\). A
6
\text{Build the term model: let } |\mathcal{M}| = C/\!\sim, \text{ the set of } \sim\text{-classes } [c]. \text{ Interpret each constant } c \in C \text{ as } [c]; \text{ for each function symbol } f \text{ and relation symbol } R \text{ of } L, \text{ set}
f^{\mathcal{M}}([c_1],\dots,[c_n]) = [c] \iff (f(c_1,\dots,c_n) = c) \in \Sigma^*, \qquad R^{\mathcal{M}}([c_1],\dots,[c_n]) \iff R(c_1,\dots,c_n) \in \Sigma^*.
Well-definedness (independence of representatives) is checked using the equality axioms' substitution schema together with maximal consistency: if \(c_i \sim c_i'\) for each \(i\), then \((c_i = c_i')\in\Sigma^*\) for each \(i\), and substitution into atomic formulas is derivable from the equality axioms, so \(R(c_1,\dots,c_n)\in\Sigma^* \iff R(c_1',\dots,c_n')\in\Sigma^*\), and similarly for \(f\); totality of \(f^{\mathcal{M}}\) uses that \(\exists x\,(f(c_1,\dots,c_n)=x)\) is logically valid (a term always denotes) hence in \(\Sigma^*\), and then the Henkin witnessing axiom (step 2) for that formula supplies a witnessing constant \(c\) with \((f(c_1,\dots,c_n)=c)\in\Sigma^*\). C
7
\text{Truth Lemma: for every } L^+\text{-sentence } \chi, \qquad \mathcal{M} \models \chi \iff \chi \in \Sigma^*.
Induction on the structure of \(\chi\). Atomic case: immediate from the definitions in step 6. Negation: \(\mathcal{M}\models\neg\chi \iff \mathcal{M}\not\models\chi \iff \chi\notin\Sigma^*\) (inductive hypothesis) \(\iff \neg\chi\in\Sigma^*\) (by maximal consistency, step 4: exactly one of \(\chi,\neg\chi\) is in \(\Sigma^*\)). Conjunction/disjunction: routine from closure of \(\Sigma^*\) under provable consequence and the propositional behaviour of a maximal consistent set (a Boolean-algebra-style argument: \(\chi_1\wedge\chi_2\in\Sigma^*\) iff both \(\chi_1,\chi_2\in\Sigma^*\), by soundness/completeness of \(\Sigma^*\) for propositional consequence). Existential case, the one step that genuinely needs Henkin witnesses: if \(\exists x\,\varphi(x)\in\Sigma^*\), then since \(\exists x\,\varphi(x)\to\varphi(c_\varphi)\in\Theta\subseteq\Sigma^*\) and \(\Sigma^*\) is deductively closed, \(\varphi(c_\varphi)\in\Sigma^*\); by inductive hypothesis \(\mathcal{M}\models\varphi(c_\varphi)\), i.e. \(\mathcal{M}\models\varphi([c_\varphi])\), so \(\mathcal{M}\models\exists x\,\varphi(x)\); conversely if \(\mathcal{M}\models\exists x\,\varphi(x)\) some class \([c]\) satisfies \(\varphi\), so by inductive hypothesis \(\varphi(c)\in\Sigma^*\), and \(\vdash \varphi(c)\to\exists x\,\varphi(x)\) (existential generalisation, an axiom/rule of the calculus) forces \(\exists x\,\varphi(x)\in\Sigma^*\) by deductive closure. Universal quantifiers are dual to existential via \(\forall x\,\varphi \equiv \neg\exists x\,\neg\varphi\). C
8
\mathcal{M} \models \Sigma \qquad \text{(the } L\text{-reduct of } \mathcal{M}\text{, forgetting the interpretation of the constants in } C\text{, is a model of } \Sigma\text{).}
\(\Sigma \subseteq \Sigma^*\) by construction (step 4 extends \(\Sigma\cup\Theta\)), so by the Truth Lemma every \(\sigma\in\Sigma\) has \(\mathcal{M}\models\sigma\); since every sentence of \(\Sigma\) is an \(L\)-sentence, satisfaction of \(\Sigma\) by \(\mathcal{M}\) is the same as satisfaction by its \(L\)-reduct \(\mathcal{M}|_L\), which is the \(L\)-structure asserted to exist. A
9
\text{Conclude: consistency of } \Sigma \implies \text{ satisfiability of } \Sigma, \text{ and hence, via the contrapositive/deduction-theorem argument sketched in the Statement, } \Sigma \models \varphi \implies \Sigma \vdash \varphi \text{ for every sentence } \varphi.
Steps 1–8 constructed a model of \(\Sigma\) whenever \(\Sigma\) is consistent, proving Consistent \(\Rightarrow\) Satisfiable; contrapositively, Unsatisfiable \(\Rightarrow\) Inconsistent. Apply this to \(\Sigma\cup\{\neg\varphi\}\): if \(\Sigma\models\varphi\) then \(\Sigma\cup\{\neg\varphi\}\) has no model (any model of \(\Sigma\) satisfies \(\varphi\), hence not \(\neg\varphi\)), so by the contrapositive \(\Sigma\cup\{\neg\varphi\}\) is inconsistent, i.e. \(\Sigma,\neg\varphi\vdash\bot\); by reductio ad absurdum (a structural rule of the calculus, hypothesis above) \(\Sigma\vdash\varphi\). B
Result
\Sigma \models \varphi \;\iff\; \Sigma \vdash \varphi
Reading. A first-order sentence is derivable from a set of axioms by finite, purely syntactic proof precisely when it is true in every conceivable structure that satisfies those axioms. Provability (a notion you can in principle check symbol-by-symbol) and validity (a notion quantifying over a proper-class-sized universe of structures) are the same relation.
Scope. Holds for first-order logic over a language of any cardinality, with or without equality (given the equality axioms), for any set \(\Sigma\) of sentences including the empty set (pure logical validity) and infinite \(\Sigma\). It requires the language to be genuinely first-order — quantifying only over individuals — and a sound calculus with the structural rules used above. It does not by itself say anything about which sentences are true in one fixed intended structure (e.g. \((\mathbb{N},+,\times)\)); that question is the domain of Gödel's incompleteness theorems, which are compatible with completeness because they concern a single structure's theory, not the class of all models of an axiom set.
Corollaries & converses
- Compactness theorem (free corollary): if every finite subset of \(\Sigma\) is satisfiable, then \(\Sigma\) is satisfiable. Proof: if every finite subset is satisfiable, no finite subset derives \(\bot\) (by soundness), so by the finiteness of derivations \(\Sigma\) itself is consistent, hence by completeness (model-existence form) satisfiable.
- Löwenheim–Skolem (downward) falls out of the construction itself: the term model built in the proof has cardinality \(\leq |L^+| = |L| + \aleph_0\), so any satisfiable countable \(\Sigma\) has a countable model.
- The soundness theorem \(\Sigma\vdash\varphi \Rightarrow \Sigma\models\varphi\) is the converse direction and is a separate, easier fact (induction over derivations checking each axiom is valid and each rule preserves validity); the two together give the biconditional stated above. Soundness does not follow from completeness, so it must be established independently for whichever calculus is fixed — the theorem as usually invoked already assumes it (see Hypotheses).
- Completeness does not extend to full second-order logic (no complete effective calculus exists), and it does not say every true sentence about \(\mathbb{N}\) is provable from a fixed r.e. axiom set — that is precisely what Gödel's first incompleteness theorem rules out, for a different reason (arithmetical self-reference), and the two "Gödel theorems" are not in tension because completeness quantifies over all models of \(\Sigma\), while incompleteness fixes one model.
Fails without
- Dropping first-orderness (moving to full second-order logic): the second-order sentence \(\mathrm{PA}_2\) categorically axiomatising \((\mathbb{N},+,\times,0,1)\) has, among its second-order semantic consequences, the (arithmetised) statement "\(\mathrm{PA}_2\) is consistent" and indeed every true arithmetical sentence, none of which is provable from \(\mathrm{PA}_2\) in any recursively axiomatised proof system, by Gödel's first incompleteness theorem applied to the (unique, standard) model. So \(\models\) strictly exceeds \(\vdash\) for any effective calculus: no completeness theorem can hold.
- Dropping soundness of the calculus (e.g. adding an unsound extra rule that lets any sentence be derived from \(x \neq x\)): then \(\vdash\) can certify sentences that are false in some models of \(\Sigma\), e.g. contradictory-looking derivations become "provable" while being falsified by an actual model, breaking the \(\vdash \Rightarrow \models\) half; the theorem as stated silently assumes a specific known-sound calculus, and swapping in an unsound one make the equivalence meaningless (both directions can fail for different reasons).
- Working in a language without the equality axioms while still using \(=\) as a logical symbol interpreted as identity: the valid sentence \(\forall x\forall y\,(x=y \to \forall z(R(x,z)\leftrightarrow R(y,z)))\) is true in every structure where \(=\) is interpreted as genuine equality, but is not derivable from a calculus that treats \(=\) as an uninterpreted binary relation symbol with no governing axioms, since one can build a "model" with \(=\) reinterpreted as an arbitrary equivalence relation making the sentence false — completeness for such a stripped calculus would relate \(\vdash\) to a wrong semantics.
Common errors
- Conflating Gödel's completeness theorem with his incompleteness theorems — they are about different things (all-models validity vs. one fixed structure's true arithmetic) and are not in contradiction; students often think completeness was later "overturned" by incompleteness.
- Believing completeness says every true sentence of arithmetic is provable from Peano axioms — it says every sentence true in every model of the Peano axioms (including wild nonstandard ones) is provable; a sentence true only in the standard model \(\mathbb{N}\) need not be a semantic consequence of \(\mathrm{PA}\) at all, so completeness says nothing about it.
- Forgetting that the theorem is about a language with possibly infinitely many sentences \(\Sigma\), and misapplying finite-proof intuition: the derivation \(\Sigma \vdash \varphi\) is always finite (uses finitely many members of \(\Sigma\)), even when \(\Sigma\) itself is infinite — this finiteness is exactly what powers the compactness corollary and is often overlooked.
- Thinking the Henkin constants "already exist" in \(L\) — they are new symbols adjoined purely for the proof and the theorem produces a model of the original language \(L\) only after taking the reduct in step 8; the term-model elements are equivalence classes of these new constants, not literally elements the student can point to independent of the construction.
- Assuming the term model constructed is "the" model, or is countable/canonical in a stronger sense than stated — different enumerations in Lindenbaum's lemma give different (non-isomorphic, in general) maximal consistent extensions and hence different models; completeness only guarantees existence of some model, not uniqueness.
Discussion
Gödel proved completeness in his 1929 doctoral dissertation (published 1930), before the incompleteness theorems (1931); historically the two results are often taught together and confused precisely because they share an author, a year, and the word "complete/incomplete", while addressing orthogonal questions: completeness is a fact about the relationship between a fixed proof calculus and the class of all structures, whereas incompleteness is a fact about what can be derived, in any one recursively axiomatised sound theory, about one particular structure (or any structure interpreting enough arithmetic).
Henkin's 1949 proof, reproduced above, replaced Gödel's original approach (closer to Skolem's normal-form and satisfiability methods) with a more algebraic, syntax-driven construction: instead of analysing truth directly, one manufactures "enough" constants to name witnesses for every existential claim that consistency does not rule out, then reads a model straight off the syntax. This method generalises smoothly (Henkin's own proof of completeness for type theory, model-theoretic forcing constructions, and omitting-types theorems all reuse the same skeleton: extend to a maximal consistent set with witnessing properties, then build a canonical model from syntactic objects).
The compactness theorem, obtained as an immediate corollary, is in a precise sense equivalent in strength to completeness over the base theory ZF plus a weak choice principle (the Boolean Prime Ideal theorem suffices for compactness in general, and is in fact equivalent to it); this is worth flagging because it shows completeness/compactness sit strictly below full AC in consistency strength for many applications, even though the cleanest textbook proof (as given here) reaches for full AC to enumerate an arbitrary-cardinality language.
A common deeper misconception is to think completeness makes first-order logic "as good as" being able to decide truth: it does not. Completeness gives a semi-decision procedure for validity (systematically enumerate all proofs; a valid sentence will eventually be found) but says nothing computational about invalid sentences, and indeed first-order validity is undecidable (Church/Turing 1936) even though it is recursively enumerable — a fact that is itself an immediate consequence of completeness (enumerate proofs) combined with the existence of an undecidable r.e. set.
Worked examples
1
\text{Show, using completeness, that if every finite subset of an infinite set of sentences } \Sigma \text{ is satisfiable, then } \Sigma \text{ is satisfiable (compactness), and use this to build a nonstandard model of arithmetic.}
Let \(\Sigma = \mathrm{Th}(\mathbb{N}) \cup \{c \gt \underline{0}, c \gt \underline{1}, c \gt \underline{2}, \dots\}\) in the language of arithmetic plus a new constant \(c\), where \(\mathrm{Th}(\mathbb{N})\) is the full first-order theory of the standard naturals and \(\underline{n}\) is the numeral for \(n\). B
2
\text{Every finite subset } \Sigma_0 \subseteq \Sigma \text{ is satisfiable.}
\(\Sigma_0\) mentions only finitely many of the constraints \(c\gt\underline{n}\), say up to \(n=N\); interpret \(c\) as \(N+1\) in the standard model \(\mathbb{N}\), which already satisfies all of \(\mathrm{Th}(\mathbb{N})\) by definition, so \(\mathbb{N}\) with this interpretation of \(c\) satisfies \(\Sigma_0\). A
3
\text{By the compactness corollary of completeness (Corollaries), } \Sigma \text{ is satisfiable: there is a model } \mathcal{M} \models \Sigma.
Direct application of compactness proved above via completeness + step 9's finiteness-of-derivations argument. B
4
\mathcal{M} \text{ satisfies every first-order sentence true of } \mathbb{N}, \text{ yet contains an element } c^{\mathcal{M}} \text{ larger than every standard numeral} \Longrightarrow \mathcal{M} \not\cong \mathbb{N}.
\(\mathcal{M}\models\mathrm{Th}(\mathbb{N})\) by construction; \(\mathcal{M}\models c\gt\underline{n}\) for every \(n\) means \(c^{\mathcal{M}}\) sits above the image of every standard natural number, which is impossible in \(\mathbb{N}\) itself (every element of \(\mathbb{N}\) is some standard \(\underline{n}\)), so \(\mathcal{M}\) is elementarily equivalent to but not isomorphic to \(\mathbb{N}\): a genuine nonstandard model. B
\text{A nonstandard model of true arithmetic exists, as a direct corollary of completeness.}
Reading. Completeness (via compactness) shows first-order arithmetic cannot pin down \(\mathbb{N}\) up to isomorphism — there are "numbers" bigger than every finite numeral in some models satisfying exactly the same first-order sentences as the true naturals.
1
\text{Show } \{\forall x\,(P(x)\to Q(x)),\ \forall x\,(Q(x)\to R(x))\} \models \forall x\,(P(x)\to R(x)) \text{ has a genuine finite formal proof (as guaranteed to exist by completeness), and exhibit it.}
By completeness, since the semantic entailment plainly holds (chain the implications pointwise in any model), a finite derivation \(\Sigma\vdash\forall x\,(P(x)\to R(x))\) must exist; we now produce one explicitly rather than merely invoking the existence guarantee, to show completeness' promise is not vacuous. A
2
\text{From } \forall x\,(P(x)\to Q(x)) \text{ and } \forall x\,(Q(x)\to R(x)), \text{ instantiate at a fresh variable } y: \quad P(y)\to Q(y), \quad Q(y)\to R(y).
Universal instantiation ( \(\forall x\,\varphi(x) \vdash \varphi(y)\) for any term \(y\), an axiom/rule of the calculus). A
3
P(y) \to R(y) \quad \text{by propositional (hypothetical syllogism) reasoning from the two conditionals in step 2.}
Hypothetical syllogism is derivable from modus ponens plus the deduction theorem: assume \(P(y)\), derive \(Q(y)\) by modus ponens on the first conditional, then \(R(y)\) by modus ponens on the second; discharge the assumption via the deduction theorem to get \(P(y)\to R(y)\). A
4
\forall x\,(P(x)\to R(x)) \quad \text{by generalising on } y.
Generalisation is legal because \(y\) is a fresh variable, not free in either premise \(\forall x(P(x)\to Q(x))\) or \(\forall x(Q(x)\to R(x))\) — exactly the side-condition required for the generalisation rule. B
\{\forall x(P(x)\to Q(x)),\ \forall x(Q(x)\to R(x))\} \;\vdash\; \forall x(P(x)\to R(x))
Reading. The syntactic derivation matches exactly what completeness promised on purely semantic grounds: a finite chain of legal rule-applications reproduces the obvious semantic fact that "if \(P\Rightarrow Q\) and \(Q\Rightarrow R\) everywhere, then \(P\Rightarrow R\) everywhere."
Problems
- State precisely what it would mean for first-order logic to fail completeness, and explain in one sentence why the failure of completeness for full second-order logic is not itself a counterexample to Gödel's theorem.
Solution
Failure of completeness for first-order logic would mean there exists a set \(\Sigma\) and sentence \(\varphi\) with \(\Sigma\models\varphi\) (true in every model of \(\Sigma\)) but \(\Sigma\not\vdash\varphi\) (no finite formal derivation exists in the fixed sound calculus) — i.e. \(\models\) strictly larger than \(\vdash\). This is not a counterexample to Gödel's theorem because the theorem's hypothesis restricts explicitly to first-order logic (Hypotheses, first bullet); second-order logic is a different logical system with a different, non-first-order semantics (quantifiers ranging over all subsets of the domain, not just elements), so the theorem simply does not apply to it and its failure there is expected, not contradictory. - Use completeness (via the model-existence form) to show: if a set of sentences \(\Sigma\) is such that every finite subset has a model of size \(\geq n\) for every \(n\), then \(\Sigma\) has an infinite model.
Solution
Consider \(\Sigma' = \Sigma \cup \{\theta_n : n\geq 2\}\) where \(\theta_n\) is the sentence "there exist at least \(n\) distinct elements" (expressible in first-order logic with equality as \(\exists x_1\cdots\exists x_n \bigwedge_{i\lt j} x_i\neq x_j\)). Any finite subset of \(\Sigma'\) mentions only finitely many \(\theta_n\), say up to \(\theta_N\); by hypothesis some finite subset of \(\Sigma\) already occurring in this finite subset has a model of size \(\geq N\), and (since \(\Sigma\) is presumably being checked against models of the relevant finite piece — more carefully: take the model of size \(\geq N\) guaranteed for the \(\Sigma\)-part of this finite subset, which then also satisfies \(\theta_2,\dots,\theta_N\)) so the finite subset is satisfiable. By compactness (a corollary of completeness), \(\Sigma'\) is satisfiable; any model of \(\Sigma'\) satisfies every \(\theta_n\) for all \(n\), hence has infinite domain, and satisfies \(\Sigma\) since \(\Sigma\subseteq\Sigma'\). - Explain why the completeness theorem, applied with \(\Sigma=\varnothing\), gives precisely: "every logically valid formula is provable" and identify which direction of the biconditional \(\Sigma\models\varphi\iff\Sigma\vdash\varphi\) is doing the work.
Solution
With \(\Sigma=\varnothing\), "\(\varnothing\models\varphi\)" unwinds to "\(\varphi\) is true in every structure" — i.e. \(\varphi\) is logically valid — and "\(\varnothing\vdash\varphi\)" unwinds to "\(\varphi\) is a formal theorem (provable from no premises, i.e. purely from the logical axioms/rules)". The forward direction \(\models\Rightarrow\vdash\) (completeness proper, proved via steps 1–9 above) is exactly what is needed to go from "valid" to "provable"; the reverse \(\vdash\Rightarrow\models\) is soundness, a separate and comparatively easy fact, needed only to know that provable formulas really are valid (not used in deriving the one-line-summary claim itself, but needed for the biconditional to be meaningful/non-vacuous). - A student claims: "By completeness, since \(\mathrm{PA}\) (Peano Arithmetic) does not prove its own consistency statement \(\mathrm{Con}(\mathrm{PA})\) [Gödel's second incompleteness theorem], there must be a model of \(\mathrm{PA}\) in which \(\mathrm{Con}(\mathrm{PA})\) is false." Evaluate this claim.
Solution
The claim is correct, and is in fact a nice illustration of completeness (not a tension with it). Since \(\mathrm{PA}\not\vdash\mathrm{Con}(\mathrm{PA})\), by completeness (contrapositive of \(\models\Rightarrow\vdash\), i.e. if not provable then not a semantic consequence) it follows \(\mathrm{PA}\not\models\mathrm{Con}(\mathrm{PA})\), meaning some model of \(\mathrm{PA}\) fails to satisfy \(\mathrm{Con}(\mathrm{PA})\); note this model is necessarily nonstandard (the true standard model \(\mathbb{N}\) does satisfy \(\mathrm{Con}(\mathrm{PA})\), since \(\mathrm{PA}\) really is consistent by Gentzen's proof / by existence of the standard model itself), illustrating exactly how completeness and incompleteness cohabit: incompleteness is a fact about what \(\mathrm{PA}\) proves, completeness translates "not proved" into "false in some (necessarily exotic) model". - Prove the deduction-theorem-based equivalence used in the Statement section in full: show carefully that \(\Sigma,\neg\varphi\vdash\bot\) implies \(\Sigma\vdash\varphi\), stating exactly which structural rule of the calculus (reductio ad absurdum) is invoked and why it is a legitimate rule to assume.
Solution
Suppose \(\Sigma,\neg\varphi\vdash\bot\). The rule of reductio ad absurdum (RAA) — a standard structural/derived rule present in every complete first-order calculus (Hilbert-style via \(\neg\neg\)-elimination axioms, natural deduction as a primitive rule, or sequent calculus via cut plus \(\neg\)-introduction) — states: if assuming \(\neg\varphi\) alongside \(\Sigma\) allows a derivation of \(\bot\) (an explicit contradiction, e.g. \(\psi\wedge\neg\psi\) for some \(\psi\), or a designated falsum constant), then \(\Sigma\vdash\varphi\) outright, discharging the assumption \(\neg\varphi\). Concretely in a Hilbert system this is proved from the axiom scheme \((\neg\varphi\to\bot)\to\varphi\) (or \((\neg\varphi\to\psi)\to((\neg\varphi\to\neg\psi)\to\varphi)\)) combined with the deduction theorem: \(\Sigma,\neg\varphi\vdash\bot\) gives, by the deduction theorem, \(\Sigma\vdash\neg\varphi\to\bot\), and then \(\Sigma\vdash\varphi\) follows by modus ponens against the RAA axiom scheme instantiated at \(\varphi\). This rule is legitimate to assume because it is sound (an easy semantic check: in any structure where \(\neg\varphi\) leads by valid steps to something false in every structure, \(\varphi\) must itself be true there) and is part of the fixed, independently-verified-sound calculus the Hypotheses section requires.