42.01.06 · mathematical-logic / first-order-logic-completeness

Gödel's Completeness Theorem and the Henkin Construction

shipped3 tiersLean: none

Anchor (Master): Enderton 2001 *A Mathematical Introduction to Logic* 2e §2.5-2.6 (the full completeness theorem with the Henkin term model, the truth lemma, the equality quotient to a normal model, the countable and uncountable cases and the cardinality of the model, and the deduction of compactness and Löwenheim-Skolem); Henkin 1949 *The completeness of the first-order functional calculus* (J. Symbolic Logic 14) (the constants-and-maximal-consistent-set proof that replaced Gödel's original argument); Chang and Keisler 1990 *Model Theory* 3e (North-Holland) Ch. 1-2 (the model existence theorem, consistency properties, the method of constants, and the role of choice); Hodges 1993 *Model Theory* (Cambridge) Ch. 6 (the Henkin construction as a special case of building models by approximation); Shoenfield 1967 *Mathematical Logic* (Addison-Wesley) Ch. 4 (the reduction theorem and the completeness theorem with the term model)

Intuition Beginner

The previous units left two notions sitting side by side. One is true in every world: pick any world, fix what the symbols mean, check that the sentence comes out true there, and confirm it never fails anywhere. The other is provable: reach the sentence by the rule-pushing chain game that never looks at any world. The earlier unit showed the game is safe — anything you can prove really is true everywhere. This unit settles the reverse and far harder direction: anything true in every world can also be reached by the game. The two notions, one about meaning and one about pure shape, name exactly the same sentences.

It is easier to attack a disguised version of the question. Instead of asking "is every truth provable," ask: "if a batch of assumptions never lets the game grind out a flat contradiction, must there be a single world that makes them all true at once?" The striking answer is yes, and the proof is constructive in a surprising way. You do not go searching the universe for a suitable world. You build one out of the words of the language itself. The objects of the new world are just the names you can write down.

The one clever move handles claims of the form "something has this property." Whenever the assumptions allow such a claim, you simply invent a fresh name and declare it to be the thing. Do this for every such claim, settle every yes-or-no question one way or the other without contradiction, and the pile of names becomes a working world in which every assumption holds. Truth and provability meet because a world can always be assembled from language.

Visual Beginner

The picture is a world built from words. You start with assumptions the proof game cannot turn into a contradiction. Every time the assumptions say "something exists with a property," you mint a brand-new name and appoint it the witness. The objects of the finished world are exactly these names, and a basic claim is true there precisely when it sits in your settled pile of assumptions.

   BUILDING A WORLD OUT OF NAMES

   assumptions (no contradiction reachable):
        "something is red"
        "something is round"

   STEP 1  mint a fresh name for each "something exists":
        "something is red"    ->  invent  c1 ,  declare  "c1 is red"
        "something is round"  ->  invent  c2 ,  declare  "c2 is round"

   STEP 2  the objects of the new world are just the names:
        world = {  c1 ,  c2 ,  ... all the names you can write  }

   STEP 3  a basic claim is true in this world
           exactly when it is in the settled pile:
        "c1 is red"     ->  in the pile     ->  TRUE  in the world
        "c1 is round"   ->  not in the pile ->  FALSE in the world

   RESULT  every assumption comes out true in this hand-built world.

Read it top to bottom. The assumptions never let the game derive a contradiction, so they can be settled into a consistent pile that answers every basic yes-or-no question. The witnesses guarantee that whenever something is claimed to exist, an actual name in the world does the job. The world is made of language, and it satisfies everything you started with.

ingredient	what it is	role
the assumptions	a batch the game cannot contradict	the input
a fresh name $c$	invented per "something exists" claim	the witness
the objects	the names you can write	the universe
the settled pile	every claim decided, no contradiction	reads off truth

Change nothing about the meaning of symbols in advance; the pile of decided claims supplies all the meaning the world needs.

Worked example Beginner

We build a tiny world out of names for one specific batch of assumptions and check that it makes them all true. The batch: "something is happy," together with "everyone who is happy is lucky." We will show a single hand-built world satisfies both.

Step 1. Look for "something exists" claims. The first assumption, "something is happy," is exactly that. So we mint a fresh name — call it $c$ — and declare " $c$ is happy." The name $c$ is now an object of our world, appointed to witness the existence claim.

Step 2. Settle the remaining yes-or-no questions without contradiction. We have " $c$ is happy" in the pile. The second assumption says everyone happy is lucky, so to keep the pile consistent we must also put " $c$ is lucky" in. We do. Nothing forces a contradiction: no claim and its opposite both appear.

Step 3. Fix the world. Its single named object so far is $c$ (more names may exist but are unused here). A basic claim is true in this world exactly when it is in the settled pile. So " $c$ is happy" is true, and " $c$ is lucky" is true.

Step 4. Check the first assumption, "something is happy." The world contains $c$ , and " $c$ is happy" is true there, so "something is happy" holds. The witness did its job.

Step 5. Check the second assumption, "everyone happy is lucky." The only object we must inspect is $c$ . Since " $c$ is happy" and " $c$ is lucky" are both in the pile, the object $c$ does not break the rule. So the universal claim holds in this world.

What this tells us: starting from assumptions the proof game cannot contradict, we manufactured a world purely from a minted name, and both assumptions came out true. The "something exists" claim was handled by appointing a fresh name as its witness — the one move that makes the whole construction run. The next sections turn "mint a witness for every existence claim, then settle everything consistently" into the precise Henkin construction.

Check your understanding Beginner

Exercise (easy, multiple choice).

To build a world from words, what do you do each time the assumptions claim "something has a certain property"?

A. Check every existing object until one happens to fit.

B. Mint a fresh name and appoint it the witness — declare that name to have the property.

C. Delete the claim, since names cannot have properties.

D. Pick a number and hope it works.

Hint

The whole point is that you never search for a witness; you create one.

Answer

B. For every "something exists with this property" claim you invent a brand-new name and declare that name to have the property, so an actual object of the hand-built world witnesses the claim. Feedback-correct: minting witnesses is the single move that makes the construction succeed. Feedback-wrong: you do not search existing objects, you do not discard the claim, and the witnesses are names from the language, not guessed numbers.

Formal definition Intermediate+

Fix a first-order language $L$ with equality and the deductive calculus, the turnstile $⊢$ , and the syntactic notion of consistency of 42.01.05 pending, over the semantics $⊨$ of 42.01.04 pending. The completeness theorem asserts the converse of soundness.

Completeness (Gödel 1930). For every set $Γ$ of formulas and formula $φ$ , if $Γ ⊨ φ$ then $Γ ⊢ φ$ .

Equivalently, in the form on which the proof is built, the model existence theorem: every consistent set of formulas has a model. The two are interderivable. From model existence: if $Γ ⊨ φ$ but $Γ \neq ⊢ φ$ , then $Γ \cup {\neg φ}$ is consistent (a deduction of a contradiction from it would, by the deduction theorem, give $Γ ⊢ φ$ ), so it has a model, contradicting $Γ ⊨ φ$ . Conversely, soundness 42.01.05 pending and model existence give that consistency and satisfiability coincide. Combined with soundness, completeness yields $⊢ = ⊨$ : the syntactic and semantic consequence relations are extensionally identical.

The proof is Henkin's. Three constructions carry it ^{[Henkin 1949]}.

A set $Δ$ of $L^{'}$ -sentences (in an expanded language $L^{'}$ ) is maximal consistent if it is consistent and for every $L^{'}$ -sentence $σ$ either $σ \in Δ$ or $\neg σ \in Δ$ . Maximal consistency forces deductive closure ( $Δ ⊢ σ \Leftrightarrow σ \in Δ$ ) and the membership-respects-connectives clauses: $\neg σ \in Δ \Leftrightarrow σ \in / Δ$ and $(σ \to τ) \in Δ \Leftrightarrow (σ \in / Δ or τ \in Δ)$ .

A set $Δ$ has Henkin witnesses if for every formula $\exists x φ$ with one free variable $x$ there is a closed term $t$ (a witnessing constant) with $(\exists x φ \to φ_{t}^{x}) \in Δ$ ; combined with maximal consistency this gives the existential-witness property $\exists x φ \in Δ \Leftrightarrow φ_{t}^{x} \in Δ$ for some closed $t$ .

The canonical (term) model $A$ of a maximal consistent $Δ$ with witnesses has universe the set $T$ of closed $L^{'}$ -terms modulo the relation $t \approx u \Leftrightarrow (t = u) \in Δ$ , which the equality axioms (A5)–(A6) of 42.01.05 pending make a congruence respecting every function and relation symbol; one interprets $f^{A} ([t_{1}], \dots, [t_{n}]) = [f t_{1} \dots t_{n}]$ and $([t_{1}], \dots, [t_{n}]) \in R^{A} \Leftrightarrow (R t_{1} \dots t_{n}) \in Δ$ . The quotient by $\approx$ makes $=$ genuine identity, so $A$ is a normal model.

Counterexamples to common slips Intermediate+

"Completeness says every sentence is provable or refutable." No — that is the false claim refuted by Gödel incompleteness 42.01.09 pending. Completeness says $Γ ⊢ φ$ whenever $Γ ⊨ φ$ , a statement about the match between provability and semantic consequence, not about deciding every arithmetic sentence from a fixed axiom set.
"The witnessing constants make the model bigger than the language." The universe is closed terms of $L^{'}$ modulo provable equality, so $∣ A ∣ \leq ∣ L ∣ + ℵ_{0}$ . For a countable language the model is countable — the Löwenheim-Skolem phenomenon, not a defect.
"You can skip the quotient and use closed terms directly." Then $=^{A}$ would be syntactic identity of terms, but $(c = d) \in Δ$ can hold for distinct constants $c, d$ . Without quotienting, the equality axioms are satisfied only as a congruence, not as identity, so $A$ is not normal. The quotient is mandatory.
"A consistent set always has a finite model." It has a model, of cardinality at most $∣ L ∣ + ℵ_{0}$ ; the theory of an infinite linear order is consistent with no finite model. Completeness guarantees satisfiability, never finiteness.

Key theorem with proof Intermediate+

The central theorem of the chapter is completeness, and its substance is the model existence theorem proved by the Henkin construction. The hinge is the truth lemma: the canonical structure satisfies exactly the sentences of the maximal consistent set.

Theorem (Model existence; Gödel-Henkin). Every consistent set $Γ$ of $L$ -sentences has a normal model of cardinality at most $∣ L ∣ + ℵ_{0}$ . ^{[Enderton §2.5]}

Proof. Expand $L$ to $L^{'}$ by adjoining a set $C$ of new constant symbols, $∣ C ∣ = ∣ L ∣ + ℵ_{0}$ , indexed so that for each $L^{'}$ -formula $\exists x φ$ there is a dedicated constant $c_{\exists x φ} \in C$ (an enumeration in $∣ L^{'} ∣$ stages assigns the constants, each fresh to the formula it witnesses). Let $H$ be the set of Henkin axioms $\exists x φ \to φ_{c_{\exists x φ}}^{x}$ .

Consistency is preserved by the Henkin axioms. It suffices that adding one Henkin axiom to a consistent set $Σ$ with $c = c_{\exists x φ}$ fresh to $Σ$ keeps it consistent. If $Σ \cup {\exists x φ \to φ_{c}^{x}}$ were inconsistent, the deduction theorem gives $Σ ⊢ \neg (\exists x φ \to φ_{c}^{x})$ , hence $Σ ⊢ \exists x φ$ and $Σ ⊢ \neg φ_{c}^{x}$ . Since $c$ occurs in neither $Σ$ nor $\exists x φ$ , generalization-on-constants 42.01.05 pending turns $Σ ⊢ \neg φ_{c}^{x}$ into $Σ ⊢ \forall x \neg φ$ , i.e. $Σ ⊢ \neg\exists x φ$ , contradicting $Σ ⊢ \exists x φ$ . Iterating over all Henkin axioms (a union of finitely-supported deductions), $Γ \cup H$ is consistent in $L^{'}$ .

Lindenbaum extension. Extend $Γ \cup H$ to a maximal consistent set $Δ$ of $L^{'}$ -sentences. Enumerate the $L^{'}$ -sentences (using a well-ordering of cardinality $∣ L^{'} ∣$ , hence the axiom of choice in general); at each stage adjoin $σ$ if doing so preserves consistency and otherwise adjoin $\neg σ$ , which then preserves it — one of the two always does, since if both $Σ \cup {σ}$ and $Σ \cup {\neg σ}$ were inconsistent the deduction theorem would give $Σ ⊢ \neg σ$ and $Σ ⊢ σ$ , making $Σ$ inconsistent. The union $Δ$ over all stages is consistent (any deduction uses finitely many of its members, all present by some stage) and decides every sentence, so it is maximal consistent. It contains every Henkin axiom, so it has the existential-witness property.

The canonical model. Let $T$ be the closed $L^{'}$ -terms and $t \approx u \Leftrightarrow (t = u) \in Δ$ . By (A5) $\approx$ is reflexive; (A6) with maximal consistency makes it symmetric, transitive, and a congruence for every function and relation symbol. Put $∣ A ∣ = T / \approx$ , $f^{A} ([t_{i}]) = [f t_{1} \dots t_{n}]$ (well defined by congruence), $c^{A} = [c]$ , and $([t_{i}]) \in R^{A} \Leftrightarrow (R t_{1} \dots t_{n}) \in Δ$ (well defined likewise). The universe is nonempty since $L^{'}$ has constants.

Truth lemma. For every $L^{'}$ -sentence $σ$ , $A ⊨ σ \Leftrightarrow σ \in Δ$ . Proof by induction on $σ$ . First, for a closed term $t$ , $\overset{s}{ˉ} (t) = [t]$ in $A$ (induction on $t$ using the interpretations). Atomic $R t_{1} \dots t_{n}$ : $A ⊨ R t_{1} \dots t_{n} \Leftrightarrow ([t_{i}]) \in R^{A} \Leftrightarrow (R t_{1} \dots t_{n}) \in Δ$ by definition; the equality atom $t = u$ holds in $A$ iff $[t] = [u]$ iff $(t = u) \in Δ$ . Negation and implication: immediate from the membership-respects-connectives clauses of $Δ$ and the inductive hypothesis. Existential $\exists x φ$ : if $\exists x φ \in Δ$ , the witness property gives a closed $t$ with $φ_{t}^{x} \in Δ$ , so by induction $A ⊨ φ_{t}^{x}$ , and the substitution lemma of 42.01.04 pending (with $\overset{s}{ˉ} (t) = [t]$ ) gives $A ⊨ \exists x φ$ ; conversely if $A ⊨ \exists x φ$ , some element $[t]$ satisfies $φ$ , so $A ⊨ φ_{t}^{x}$ , hence by induction $φ_{t}^{x} \in Δ$ , and since $φ_{t}^{x} \to \exists x φ$ is provable, $\exists x φ \in Δ$ . (The universal case is dual via $\forall x φ \equiv \neg\exists x \neg φ$ .)

By the truth lemma $A ⊨ Δ \supseteq Γ$ . The reduct $A ↾ L$ is a normal model of $Γ$ of cardinality at most $∣ L ∣ + ℵ_{0}$ . $□$

Corollary (completeness). If $Γ ⊨ φ$ then $Γ ⊢ φ$ . For otherwise $Γ \cup {\neg φ}$ is consistent, so by model existence it has a model, which satisfies $Γ$ but not $φ$ , contradicting $Γ ⊨ φ$ .

Bridge. The truth lemma is the foundational reason a maximal consistent set with witnesses is a structure read in disguise, and this is exactly the converse of the soundness of 42.01.05 pending: where soundness pushed every provable formula into every model, completeness manufactures one model in which the unprovability of $φ$ becomes the truth of $\neg φ$ , so that consistency and satisfiability coincide. The construction builds toward compactness and Löwenheim-Skolem 42.01.07 pending, which fall out of the cardinality bound and the deduction-finiteness, and it appears again in model theory 42.02.01 pending, where the term model is the prototype of building structures from syntax. The central insight is that the only nontrivial demand on the maximal set is the existential-witness property, supplied by the Henkin axioms whose addition is harmless precisely because generalization-on-constants lets a fresh constant be universally generalized away; everything else — atomic truth, connectives — is bookkeeping forced by maximal consistency. Putting these together, the chapter's two halves close: soundness pins $⊢$ below $⊨$ , completeness pins $⊨$ below $⊢$ , and $⊢=⊨$ is the bridge on which compactness, Löwenheim-Skolem, and the whole of classical model theory stand.

Exercises Intermediate+

Exercise 4 (medium, symbolic).

Prove that adding a single Henkin axiom $\exists x φ \to φ_{c}^{x}$ , with $c$ a constant occurring in neither $Σ$ nor $\exists x φ$ , preserves the consistency of $Σ$ .

Hint

Assume inconsistency, apply the deduction theorem, and use generalization-on-constants 42.01.05 pending to remove $c$ .

Answer

Suppose $Σ \cup {\exists x φ \to φ_{c}^{x}}$ is inconsistent. By the deduction theorem $Σ ⊢ \neg (\exists x φ \to φ_{c}^{x})$ . The tautology $\neg (A \to B) \to A$ gives $Σ ⊢ \exists x φ$ , and $\neg (A \to B) \to \neg B$ gives $Σ ⊢ \neg φ_{c}^{x}$ . As $c$ occurs in neither $Σ$ nor $φ$ , generalization-on-constants converts $Σ ⊢ \neg φ_{c}^{x}$ into $Σ ⊢ \forall x \neg φ$ , which is $Σ ⊢ \neg\exists x φ$ . Then $Σ$ proves both $\exists x φ$ and $\neg\exists x φ$ , so $Σ$ is inconsistent — contrary to hypothesis. Hence the Henkin axiom preserves consistency. Rubric: full credit for the deduction-theorem step, the extraction of both conjuncts, and the constants-generalization removing $c$ .

Exercise 6 (medium, symbolic).

Deduce the compactness theorem from completeness: if every finite subset of $Γ$ has a model, then $Γ$ has a model. State precisely where deduction-finiteness is used.

Hint

An unsatisfiable $Γ$ is inconsistent by completeness; a proof of a contradiction uses finitely many premises.

Answer

Suppose every finite subset of $Γ$ has a model but $Γ$ has none. By the model existence theorem (the form of completeness), $Γ$ is then inconsistent, so $Γ ⊢ β$ and $Γ ⊢ \neg β$ for some $β$ . Each deduction is a finite sequence citing finitely many premises; let $Γ_{0} \subseteq Γ$ be the finite union of premises cited in the two deductions. Then $Γ_{0} ⊢ β$ and $Γ_{0} ⊢ \neg β$ , so $Γ_{0}$ is inconsistent, hence by soundness unsatisfiable — contradicting that the finite $Γ_{0}$ has a model. So $Γ$ has a model. Deduction-finiteness is used exactly at the passage from $Γ ⊢ β, \neg β$ to a finite inconsistent $Γ_{0}$ . Rubric: full credit for routing through completeness, the finite-premise extraction, and the contradiction with finite satisfiability.

Exercise 7 (hard, symbolic).

Prove that the provable-equality relation $t \approx u \Leftrightarrow (t = u) \in Δ$ is a congruence on closed terms: it is an equivalence relation, and $t_{i} \approx u_{i}$ for all $i$ implies $f t_{1} \dots t_{n} \approx f u_{1} \dots u_{n}$ and ( $R t_{1} \dots t_{n} \in Δ \Leftrightarrow R u_{1} \dots u_{n} \in Δ$ ).

Hint

Reflexivity is (A5). Symmetry, transitivity, and the congruence clauses follow from the equality axiom (A6) $u = v \to (ψ \to ψ^{'})$ applied to suitable atomic $ψ$ , with deductive closure of $Δ$ .

Answer

Reflexivity: (A5) gives $⊢ t = t$ , so $(t = t) \in Δ$ , i.e. $t \approx t$ . Symmetry: from $(t = u) \in Δ$ , the (A6) instance $t = u \to (t = t \to u = t)$ with $(t = t) \in Δ$ and two modus ponens steps gives $(u = t) \in Δ$ . Transitivity: from $t \approx u$ and $u \approx v$ , the (A6) instance $u = v \to (t = u \to t = v)$ gives $(t = v) \in Δ$ . Function congruence: from $t_{i} \approx u_{i}$ , repeated (A6) on the atomic formula $f t_{1} \dots t_{n} = f t_{1} \dots t_{n}$ , replacing each $t_{i}$ by $u_{i}$ in the right argument tuple, yields $(f t_{1} \dots t_{n} = f u_{1} \dots u_{n}) \in Δ$ . Relation congruence: from $t_{i} \approx u_{i}$ , repeated (A6) on $R t_{1} \dots t_{n}$ replacing $t_{i}$ by $u_{i}$ gives $(R t_{1} \dots t_{n} \to R u_{1} \dots u_{n}) \in Δ$ and its converse, so $R t_{1} \dots t_{n} \in Δ \Leftrightarrow R u_{1} \dots u_{n} \in Δ$ by deductive closure. Rubric: full credit for the four equivalence-and-congruence facts each traced to an (A6) instance and deductive closure.

Exercise 8 (hard, symbolic).

Prove the existential case of the truth lemma in full: assuming the lemma for all subformulas of $\exists x φ$ , show $A ⊨ \exists x φ \Leftrightarrow \exists x φ \in Δ$ . Identify the single step that uses the Henkin witness.

Hint

Forward direction reads off a witness element $[t]$ ; backward direction uses the existential-witness property of $Δ$ , then the substitution lemma of 42.01.04 pending.

Answer

( $\Leftarrow$ ) Suppose $\exists x φ \in Δ$ . By the existential-witness property (from the Henkin axiom $\exists x φ \to φ_{c}^{x} \in Δ$ and modus ponens within $Δ$ ), there is a closed term $t$ with $φ_{t}^{x} \in Δ$ . Since $φ_{t}^{x}$ is a subformula instance, the inductive hypothesis gives $A ⊨ φ_{t}^{x}$ . By the substitution lemma of 42.01.04 pending, using $\overset{s}{ˉ} (t) = [t]$ , this is $A ⊨ φ [s (x ∣ [t])]$ , so the element $[t]$ witnesses $A ⊨ \exists x φ$ . This direction uses the Henkin witness. ( $\Rightarrow$ ) Suppose $A ⊨ \exists x φ$ . Some element of the universe is a class $[t]$ for a closed term $t$ (every element is, by construction), and $A ⊨ φ [s (x ∣ [t])]$ ; the substitution lemma rewrites this as $A ⊨ φ_{t}^{x}$ , so by induction $φ_{t}^{x} \in Δ$ . The formula $φ_{t}^{x} \to \exists x φ$ is provable (an instance dual to (A2)), so deductive closure gives $\exists x φ \in Δ$ . Rubric: full credit for both directions, the explicit appeal to the witness property and the substitution lemma, and the observation that every universe element is a term class.

Advanced results Master

The model existence theorem supports four developments: the equivalent forms of completeness and their interderivability with compactness; the cardinality analysis and the Löwenheim-Skolem theorems read off the term model; the choice principles the construction consumes, sharp in the countable case; and the sharp contrast with Gödel's incompleteness, with which completeness is routinely conflated and is not in tension.

Theorem 1 (equivalent forms). Over the soundness of 42.01.05 pending, the following are interderivable: completeness $Γ ⊨ φ \Rightarrow Γ ⊢ φ$ ; the model existence theorem (consistent $\Rightarrow$ satisfiable); the extended completeness theorem that a theory $T$ is satisfiable iff consistent, with $Th (A)$ -style deductive closure; and, for finitary $⊢$ , the compactness theorem that a finitely satisfiable set is satisfiable ^{[Chang-Keisler Ch. 1]}. Each implication uses only the deduction theorem and the finiteness of deductions. Completeness is thus the assertion that the deductive consistency of a theory is exactly the existence of a model, the single identification from which the model theory of the chapter unfolds.

Theorem 2 (cardinality; Löwenheim-Skolem). The canonical model has universe a quotient of the closed $L^{'}$ -terms, so $∣ A ∣ \leq ∣ L^{'} ∣ = ∣ L ∣ + ℵ_{0}$ ^{[Hodges Ch. 6]}. Hence a satisfiable theory in a countable language has a countable (finite or countably infinite) model — the downward Löwenheim-Skolem theorem in its weak form. Adjoining $κ$ new constants with the axioms $c_{α} \neq = c_{β}$ ( $α \neq = β$ ) to a theory with an infinite model keeps every finite subset satisfiable, so by compactness the theory has a model of cardinality $\geq κ$ — the upward Löwenheim-Skolem theorem. Together they give models in every infinite cardinality $\geq ∣ L ∣$ for any theory with one infinite model, and the Skolem paradox: a countable model of set theory, whose internal "uncountable" sets are countable from outside.

Theorem 3 (choice principles). The Lindenbaum extension well-orders the sentences of $L^{'}$ and so invokes the axiom of choice (equivalently Zorn's lemma) when $L$ is uncountable ^{[Chang-Keisler Ch. 2]}. The completeness theorem for countable languages needs only a weak fragment: the enumeration of the countably many sentences is explicit, and the construction goes through in $ZF$ plus a weak choice principle, with full completeness for arbitrary languages equivalent over a weak base to the Boolean prime ideal theorem — strictly weaker than full choice. So the dependence on choice is calibrated: harmless in the countable case, a genuine but sub-choice principle in general.

Theorem 4 (completeness is not incompleteness). The completeness theorem and Gödel's first incompleteness theorem 42.01.09 pending concern different objects and are jointly true ^{[Henkin 1949]}. Completeness: the logical axioms and rules derive every semantic consequence — provability matches truth-in-all-models. Incompleteness: any consistent, recursively axiomatized theory $T$ extending a weak arithmetic has a sentence $G_{T}$ with $T ⊬ G_{T}$ and $T ⊬ \neg G_{T}$ , so $T$ does not decide every arithmetic sentence. There is no conflict: $G_{T}$ is unprovable in $T$ precisely because it is false in some model of $T$ (a nonstandard one) and true in the standard model, so $T \neq ⊨ G_{T}$ , and completeness only ever promised provability of full semantic consequences. The phenomenon completeness forbids — a valid sentence with no proof — never occurs; the phenomenon incompleteness exhibits — a true-in- $N$ sentence undecided by a fixed r.e. theory — is about the gap between a theory's models and the standard one.

Synthesis. The truth lemma is the foundational reason consistency and satisfiability are the same property, and putting these together it organizes all four developments: it is exactly what turns the membership relation of a maximal consistent set into a satisfaction relation, so the equivalent forms of Theorem 1 are reformulations of one identification, $⊢ = ⊨$ . The cardinality bound of Theorem 2 is the central insight read off the construction — the universe is made of terms, so it cannot be larger than the language — and the upward and downward Löwenheim-Skolem theorems are dual consequences, one from compactness adding constants, the other from the term model's smallness, the same flexibility of first-order logic seen from both sides. The choice analysis of Theorem 3 generalises the propositional Lindenbaum lemma of 42.01.01 pending to the first-order setting, where the witness axioms are the genuinely new ingredient and the only place the construction reaches past an enumeration. And the contrast of Theorem 4 is the bridge that keeps the two Gödel theorems apart: completeness is about logic's power to derive consequences, incompleteness about arithmetic's models outrunning any r.e. axiomatization, so that the unprovable $G_{T}$ is not a counterexample to completeness but a witness to the multiplicity of models that completeness itself, through compactness 42.01.07 pending, guarantees. This is the keystone of the chapter: a meaning-free calculus proved to capture meaning exactly, with the model theory of 42.02.01 pending and the incompleteness theorems of 42.01.09 pending both standing on the identification it secures.

Full proof set Master

Proposition 1 (consistency preserved by all Henkin axioms). If $Γ$ is a consistent set of $L$ -sentences and $L^{'}$ , $C$ , $H$ are as in the construction, then $Γ \cup H$ is consistent in $L^{'}$ .

Proof. It suffices to show each finite stage stays consistent, since a deduction of a contradiction from $Γ \cup H$ would use finitely many Henkin axioms. Order the Henkin axioms so that each uses a constant fresh to all earlier ones and to $Γ$ . Suppose $Γ \cup H_{0}$ is consistent, $H_{0}$ a finite initial segment, and $h = (\exists x φ \to φ_{c}^{x})$ is next, with $c$ fresh to $Γ \cup H_{0}$ and to $\exists x φ$ . If $Γ \cup H_{0} \cup {h}$ were inconsistent, the deduction theorem gives $Γ \cup H_{0} ⊢ \neg h$ , so $Γ \cup H_{0} ⊢ \exists x φ$ and $Γ \cup H_{0} ⊢ \neg φ_{c}^{x}$ . Since $c$ occurs in no member of $Γ \cup H_{0}$ and not in $\exists x φ$ , generalization-on-constants 42.01.05 pending gives $Γ \cup H_{0} ⊢ \forall x \neg φ$ , i.e. $Γ \cup H_{0} ⊢ \neg\exists x φ$ , contradicting consistency. So every stage, hence $Γ \cup H$ , is consistent. $□$

Proposition 2 (Lindenbaum lemma). Every consistent set $Σ$ of $L^{'}$ -sentences extends to a maximal consistent set $Δ$ of $L^{'}$ -sentences.

Proof. Well-order the $L^{'}$ -sentences as $⟨ σ_{α} : α < λ ⟩$ , $λ = ∣ L^{'} ∣$ (choice for uncountable $L^{'}$ ; an $ω$ -enumeration otherwise). Define $Σ_{0} = Σ$ , $Σ_{α + 1} = Σ_{α} \cup {σ_{α}}$ if consistent, else $Σ_{α} \cup {\neg σ_{α}}$ , and $Σ_{β} = ⋃_{α < β} Σ_{α}$ at limits. Each step preserves consistency: if both $Σ_{α} \cup {σ_{α}}$ and $Σ_{α} \cup {\neg σ_{α}}$ were inconsistent, the deduction theorem gives $Σ_{α} ⊢ \neg σ_{α}$ and $Σ_{α} ⊢ \neg\neg σ_{α}$ , so $Σ_{α}$ is inconsistent. Limits stay consistent because a contradiction uses finitely many premises, all present by some $Σ_{α}$ . Let $Δ = ⋃_{α < λ} Σ_{α}$ . It is consistent (same finiteness argument) and decides every $σ_{α}$ , so it is maximal consistent. Maximality forces $Δ ⊢ σ \Rightarrow σ \in Δ$ : if $σ \in / Δ$ then $\neg σ \in Δ$ , and $Δ ⊢ σ$ would make $Δ$ inconsistent. $□$

Proposition 3 (the congruence and the normal model). On closed $L^{'}$ -terms, $t \approx u \Leftrightarrow (t = u) \in Δ$ is a congruence for all function and relation symbols, and the quotient interprets $=$ as identity, so $A$ is normal.

Proof. Reflexivity is the (A5) theorem $t = t$ . Symmetry and transitivity follow from (A6) instances $t = u \to (t = t \to u = t)$ and $u = v \to (t = u \to t = v)$ with deductive closure of $Δ$ . For a function symbol $f$ , the instances $t_{i} = u_{i} \to (f \overset{ˉ}{t} = f \overset{ˉ}{t} \to f \overset{ˉ}{t} = f \overset{ˉ}{t} [u_{i} / t_{i}])$ applied coordinatewise give $(f t_{1} \dots t_{n} = f u_{1} \dots u_{n}) \in Δ$ from $t_{i} \approx u_{i}$ , so $f^{A}$ is well defined on classes. For a relation symbol $R$ , the (A6) instances $t_{i} = u_{i} \to (R \overset{ˉ}{t} \to R \overset{ˉ}{t} [u_{i} / t_{i}])$ and their converses give $R t_{1} \dots t_{n} \in Δ \Leftrightarrow R u_{1} \dots u_{n} \in Δ$ , so $R^{A}$ is well defined. Finally $=^{A}$ holds of $([t], [u])$ iff $[t] = [u]$ iff $t \approx u$ , which is genuine identity of classes, so $A$ is a normal model. $□$

Proposition 4 (truth lemma). For every $L^{'}$ -sentence $σ$ , $A ⊨ σ \Leftrightarrow σ \in Δ$ .

Proof. First, for every closed term $t$ , $\overset{s}{ˉ} (t) = [t]$ : induct on $t$ , with $\overset{s}{ˉ} (c) = c^{A} = [c]$ and $\overset{s}{ˉ} (f t_{1} \dots t_{n}) = f^{A} ([t_{1}], \dots, [t_{n}]) = [f t_{1} \dots t_{n}]$ . Now induct on $σ$ . Atomic $R t_{1} \dots t_{n}$ : $A ⊨ R t_{1} \dots t_{n} \Leftrightarrow ([t_{1}], \dots, [t_{n}]) \in R^{A} \Leftrightarrow (R t_{1} \dots t_{n}) \in Δ$ . Equality $t = u$ : $A ⊨ t = u \Leftrightarrow [t] = [u] \Leftrightarrow (t = u) \in Δ$ . Negation: $A ⊨ \neg σ \Leftrightarrow A \neq ⊨ σ \Leftrightarrow σ \in / Δ \Leftrightarrow \neg σ \in Δ$ (maximality). Implication: $A ⊨ σ \to τ \Leftrightarrow (A \neq ⊨ σ$ or $A ⊨ τ) \Leftrightarrow (σ \in / Δ$ or $τ \in Δ) \Leftrightarrow (σ \to τ) \in Δ$ . Existential $\exists x φ$ : if $\exists x φ \in Δ$ , the witness property gives closed $t$ with $φ_{t}^{x} \in Δ$ , so by induction $A ⊨ φ_{t}^{x}$ , and the substitution lemma 42.01.04 pending with $\overset{s}{ˉ} (t) = [t]$ gives $A ⊨ \exists x φ$ ; conversely $A ⊨ \exists x φ$ supplies an element $[t]$ with $A ⊨ φ [s (x ∣ [t])] = φ_{t}^{x}$ , so by induction $φ_{t}^{x} \in Δ$ , whence $\exists x φ \in Δ$ by the provable $φ_{t}^{x} \to \exists x φ$ . Every universe element is some $[t]$ , so the quantifier ranges only over term classes, validating the witness reading. $□$

Proposition 5 (completeness and compactness). (i) If $Γ ⊨ φ$ then $Γ ⊢ φ$ . (ii) If every finite subset of $Γ$ is satisfiable, then $Γ$ is satisfiable.

Proof. (i) If $Γ \neq ⊢ φ$ then $Γ \cup {\neg φ}$ is consistent (a deduction of a contradiction from it would give $Γ ⊢ φ$ by the deduction theorem and the tautology $\neg φ \to ⊥ ⊢ φ$ -style reasoning), so by Propositions 1-4 it has a model $A$ , which satisfies $Γ$ but not $φ$ — contradicting $Γ ⊨ φ$ . (ii) Suppose $Γ$ is unsatisfiable. By (the model existence form of) completeness $Γ$ is inconsistent, so $Γ ⊢ β$ and $Γ ⊢ \neg β$ for some $β$ ; the two deductions cite a finite $Γ_{0} \subseteq Γ$ with $Γ_{0} ⊢ β, \neg β$ , so $Γ_{0}$ is inconsistent, hence unsatisfiable by soundness — contradicting finite satisfiability. So $Γ$ is satisfiable. $□$

Connections Master

The deductive calculus and soundness 42.01.05 pending is the prerequisite this unit completes. Soundness proved $Γ ⊢ φ \Rightarrow Γ ⊨ φ$ ; completeness proves the converse, so that $⊢ = ⊨$ . The construction consumes that unit's machinery directly: the deduction theorem drives both the consistency-preservation of the Henkin axioms and the Lindenbaum step, generalization-on-constants is exactly what makes adjoining a witness harmless, and the equality axioms (A5)-(A6) are precisely what make provable equality a congruence, turning the term model into a normal model. The easy half of "consistent iff satisfiable" was that unit's corollary; this unit supplies the hard half.
Structures and Tarski's semantics 42.01.04 pending furnishes the satisfaction relation the canonical model is read against, and its substitution lemma is invoked at the existential step of the truth lemma, converting $A ⊨ φ_{t}^{x}$ into $A ⊨ φ [s (x ∣ [t])]$ with $\overset{s}{ˉ} (t) = [t]$ . The term model is a structure in the precise sense of 42.01.04 pending — a universe with interpreted symbols — built so that its Tarskian satisfaction relation reproduces membership in the maximal consistent set.
Compactness and the Löwenheim-Skolem theorems, co-produced as 42.01.07 pending, are the immediate corollaries: compactness from completeness plus the finiteness of deductions, downward Löwenheim-Skolem from the cardinality bound $∣ A ∣ \leq ∣ L ∣ + ℵ_{0}$ of the term model, and upward Löwenheim-Skolem by adjoining distinct-constant axioms and applying compactness. These two theorems are the engines of the model theory the chapter opens onto, and both rest on the term-model cardinality and deduction-finiteness established here.
Gödel's incompleteness theorems 42.01.09 pending are the standard foil, and the contrast is load-bearing: completeness says first-order provability captures semantic consequence, while incompleteness says no consistent r.e. theory of arithmetic decides every arithmetic sentence. The unprovable Gödel sentence $G_{T}$ is not a valid sentence without a proof — that completeness forbids — but a sentence true in the standard model and false in some nonstandard model of $T$ , so $T \neq ⊨ G_{T}$ ; the nonstandard models whose existence makes this possible are themselves produced by compactness 42.01.07 pending, a corollary of the completeness proved here.
The model theory of first-order structures, co-produced as 42.02.01 pending, takes the term-model construction as its prototype: the method of diagrams, elementary amalgamation, and the existence of saturated and special models are all elaborations of "build a structure from a maximal consistent set of sentences with witnesses." The identification of consistency with satisfiability secured here is the standing hypothesis under which that structure theory operates.

Historical & philosophical context Master

Kurt Gödel proved the completeness of the first-order predicate calculus in his 1929 Vienna dissertation, published in 1930 as Die Vollständigkeit der Axiome des logischen Funktionenkalküls, answering the open problem posed in Hilbert and Ackermann's Grundzüge der theoretischen Logik (1928): that the Hilbert-style calculus derives exactly the universally valid first-order formulas ^{[Henkin 1949]}. Gödel's original argument reduced an arbitrary formula to a normal form and constructed a satisfying assignment by a careful tree argument over the natural numbers, building a model on the integers for a satisfiable countable theory.

The proof now standard is Leon Henkin's, from his 1947 Princeton dissertation under Alonzo Church and his 1949 paper The completeness of the first-order functional calculus ^{[Henkin 1949]}. Henkin replaced Gödel's combinatorial construction with the device of adjoining a new constant and a witnessing axiom for each existential formula, extending to a maximal consistent set with witnesses, and reading the model off the constants of the expanded language; the method extended at once to languages of arbitrary cardinality, yielding the Löwenheim-Skolem theorems through the cardinality of the term model, and to the general (Henkin) models of higher-order logic. The downward and upward Löwenheim-Skolem theorems trace to Leopold Löwenheim (1915) and Thoralf Skolem (1920, 1922), whose work on the cardinality of models and the relativity of set-theoretic notions (the Skolem paradox) framed the model-theoretic reading the Henkin construction makes routine, and the abstract model-existence formulation via consistency properties is due to the model theory of Chen Chung Chang and H. Jerome Keisler ^{[Chang-Keisler Ch. 1]} and the canonical-model treatment of Wilfrid Hodges ^{[Hodges Ch. 6]}.

Bibliography Master

@phdthesis{godel1930completeness,
  author = {G\"{o}del, Kurt},
  title  = {Die Vollst\"{a}ndigkeit der Axiome des logischen Funktionenkalk\"{u}ls},
  school = {University of Vienna},
  year   = {1930},
  note   = {Published in Monatshefte f\"{u}r Mathematik und Physik 37 (1930), 349--360}
}

@article{henkin1949completeness,
  author  = {Henkin, Leon},
  title   = {The completeness of the first-order functional calculus},
  journal = {The Journal of Symbolic Logic},
  volume  = {14},
  number  = {3},
  year    = {1949},
  pages   = {159--166}
}

@book{enderton2001logic,
  author    = {Enderton, Herbert B.},
  title     = {A Mathematical Introduction to Logic},
  edition   = {2},
  publisher = {Harcourt/Academic Press},
  year      = {2001}
}

@book{changkeisler1990modeltheory,
  author    = {Chang, Chen Chung and Keisler, H. Jerome},
  title     = {Model Theory},
  edition   = {3},
  series    = {Studies in Logic and the Foundations of Mathematics},
  volume    = {73},
  publisher = {North-Holland},
  year      = {1990}
}

@book{hodges1993modeltheory,
  author    = {Hodges, Wilfrid},
  title     = {Model Theory},
  series    = {Encyclopedia of Mathematics and its Applications},
  volume    = {42},
  publisher = {Cambridge University Press},
  year      = {1993}
}

@book{shoenfield1967logic,
  author    = {Shoenfield, Joseph R.},
  title     = {Mathematical Logic},
  publisher = {Addison-Wesley},
  year      = {1967}
}

@book{hilbertackermann1928,
  author    = {Hilbert, David and Ackermann, Wilhelm},
  title     = {Grundz\"{u}ge der theoretischen Logik},
  publisher = {Springer},
  year      = {1928}
}

@article{lowenheim1915,
  author  = {L\"{o}wenheim, Leopold},
  title   = {\"{U}ber M\"{o}glichkeiten im Relativkalk\"{u}l},
  journal = {Mathematische Annalen},
  volume  = {76},
  year    = {1915},
  pages   = {447--470}
}

@article{skolem1920,
  author  = {Skolem, Thoralf},
  title   = {Logisch-kombinatorische Untersuchungen \"{u}ber die Erf\"{u}llbarkeit oder Beweisbarkeit mathematischer S\"{a}tze},
  journal = {Skrifter utgit av Videnskapsselskapet i Kristiania},
  year    = {1920}
}

Prerequisites

42.01.05

Tier anchors

beginner: Enderton 2001 *A Mathematical Introduction to Logic* 2e (Harcourt/Academic Press) §2.5 (the central promise of the chapter read informally: a sentence reachable by the rule-pushing proof game is exactly a sentence true in every world, so proof and truth-everywhere are the same reach; the reverse and harder half — that a batch of assumptions that never lets the game derive a flat contradiction can always be made true together in some world — illustrated by manufacturing that world out of the names in the language itself, one invented name for every claim 'something exists with this property', so the world is built from words)
intermediate: Enderton 2001 *A Mathematical Introduction to Logic* 2e §2.5 (the completeness theorem Γ ⊨ φ ⟹ Γ ⊢ φ and its equivalent form 'every consistent set of formulas is satisfiable'; the Henkin construction — adjoining witnessing constants c_{∃x φ} with the Henkin axioms ∃x φ → φ^x_{c}, the Lindenbaum lemma extending a consistent set to a maximal consistent one with witnesses, the canonical term model on the closed terms with the provable-equality congruence quotient producing a normal model, and the truth lemma that the canonical structure satisfies exactly the formulas in the maximal set; the equivalence of completeness with compactness)
master: Enderton 2001 *A Mathematical Introduction to Logic* 2e §2.5-2.6 (the full completeness theorem with the Henkin term model, the truth lemma, the equality quotient to a normal model, the countable and uncountable cases and the cardinality of the model, and the deduction of compactness and Löwenheim-Skolem); Henkin 1949 *The completeness of the first-order functional calculus* (J. Symbolic Logic 14) (the constants-and-maximal-consistent-set proof that replaced Gödel's original argument); Chang and Keisler 1990 *Model Theory* 3e (North-Holland) Ch. 1-2 (the model existence theorem, consistency properties, the method of constants, and the role of choice); Hodges 1993 *Model Theory* (Cambridge) Ch. 6 (the Henkin construction as a special case of building models by approximation); Shoenfield 1967 *Mathematical Logic* (Addison-Wesley) Ch. 4 (the reduction theorem and the completeness theorem with the term model)

References

Enderton, H. B. — A Mathematical Introduction to Logic · 2nd edition, Harcourt/Academic Press (2001), §2.5. States and proves Gödel's completeness theorem for first-order logic in the form: if Γ ⊨ φ then Γ ⊢ φ; equivalently, every consistent set of formulas is satisfiable (has a model). The proof is Henkin's. Step 1 (Henkin witnesses): expand the language L to L' by adjoining a countable (or larger, by cardinality of L) supply of new constant symbols, and for each formula of the form ∃x φ add a Henkin axiom ∃x φ → φ^x_c where c is a constant dedicated to that formula; one shows that if Γ is consistent in L it remains consistent in L' together with all the Henkin axioms (a constant fresh to a deduction can be generalized away, by the generalization-on-constants theorem of 42.01.05). Step 2 (Lindenbaum lemma): extend the consistent L'-theory to a maximal consistent set Δ — one with, for every L'-sentence σ, exactly one of σ, ¬σ in Δ — by a transfinite/enumerative adjunction preserving consistency (Zorn's lemma in general, an enumeration in the countable case). Maximal consistency gives the deductive-closure and membership-respects-connectives properties: σ ∈ Δ iff Δ ⊢ σ; ¬σ ∈ Δ iff σ ∉ Δ; (σ → τ) ∈ Δ iff (σ ∉ Δ or τ ∈ Δ); and because of the Henkin axioms, ∃x φ ∈ Δ iff φ^x_t ∈ Δ for some closed term t (the existential-witness property). Step 3 (the canonical/term model): let the universe be the set of closed L'-terms modulo the relation t ≈ u iff (t = u) ∈ Δ, which the equality axioms make a congruence respecting the function and relation symbols; interpret each function symbol by f([t_1],...,[t_n]) = [f t_1...t_n] and each relation symbol by ([t_1],...,[t_n]) ∈ R^A iff (R t_1...t_n) ∈ Δ; the quotient makes = genuine identity, so A is a normal model. Step 4 (truth lemma): by induction on φ, A ⊨ φ[s] iff φ (with the relevant closed terms substituted) ∈ Δ; the existential case uses the Henkin witness, the universal case its dual, and the atomic case the definitions of the interpretations. Hence A ⊨ Δ ⊇ Γ, so Γ has a model — the reduct to the original language L is the required model of Γ. Corollaries: the compactness theorem (a set all of whose finite subsets are satisfiable is satisfiable, since by completeness an unsatisfiable set is inconsistent, hence proves a contradiction from a finite subset, which is therefore unsatisfiable) and the Löwenheim-Skolem theorem (the term model has cardinality at most that of the language, so a satisfiable countable theory has a countable model). The use of Zorn's lemma (a form of the axiom of choice) is needed for languages of arbitrary cardinality; for a countable language the construction is effective enough to need only a weak choice principle. Completeness, soundness (42.01.05), and the definition of ⊨ (42.01.04) together give ⊢ = ⊨, and recast consistency as satisfiability.
Henkin, L. — The completeness of the first-order functional calculus · Journal of Symbolic Logic 14 (1949), pp. 159-166. Introduces the proof of the completeness theorem that has become standard: rather than Gödel's 1930 argument, Henkin adjoins to the language a new constant for each existential formula and a corresponding axiom asserting that the constant is a witness, then extends the resulting consistent theory to a maximal consistent set possessing witnesses, and reads a model directly off the constants (closed terms) of the extended language. The method generalizes to higher-order logic with general (Henkin) models, to languages of arbitrary cardinality (giving the upward and downward Löwenheim-Skolem theorems through the cardinality of the term model), and underlies the modern model existence theorem. The construction yields a model whose elements are equivalence classes of closed terms under the provable-equality relation; the equality axioms make this relation a congruence, so the quotient interprets = as identity and is a normal model.
Chang, C. C. and Keisler, H. J. — Model Theory · 3rd edition, Studies in Logic 73, North-Holland (1990), Chapters 1-2. Develops the model existence theorem and the Henkin method abstractly through consistency properties (a family of sets of sentences closed under the rules witnessing each connective and quantifier; any member of a consistency property has a model), from which the completeness and compactness theorems and the Löwenheim-Skolem theorems follow uniformly. Treats the method of constants (adjoining witnesses), the elementary diagram, the omitting-types theorem as a refinement of the Henkin construction that avoids realizing a prescribed type, and the dependence of the general (uncountable-language) case on the axiom of choice via the prime-ideal/Zorn machinery; the countable case uses only the enumeration of formulas and a weak choice principle. Establishes that completeness is equivalent over a weak base theory to the compactness theorem and to the Boolean prime ideal theorem.
Hodges, W. — Model Theory · Cambridge University Press (1993), Chapter 6. Presents the Henkin construction as one instance of a general technique for building models by approximation: a structure is specified by a maximal consistent Hintikka-style set of sentences with witnesses, and the carrier is the set of closed terms (the 'canonical model' or 'term model') modulo provable equality. Treats the cardinality of the constructed model (bounded by the cardinality of the language plus ℵ₀), the relativization to a normal model through the equality congruence, and the way the construction specializes to give the elementary amalgamation and the existence of saturated and special models. Frames the completeness theorem as the statement that the deductive consistency of a theory is exactly the existence of a model, and isolates the witness property as the single nontrivial requirement on the maximal set.
Shoenfield, J. R. — Mathematical Logic · Addison-Wesley (1967), Chapter 4. Proves the completeness theorem via the reduction theorem (relating the consistency of a theory to the unprovability of a contradiction) and a term model built from the closed terms of a language expanded by infinitely many new constants, with special (Henkin) axioms forcing the witnessing of existential statements. The maximal consistent extension is obtained by an enumeration of the sentences; the model interprets each closed term by itself (modulo provable equality) and validates a sentence iff it lies in the maximal set. Derives the compactness theorem and the Löwenheim-Skolem theorems as immediate corollaries, and discusses the constructive content and the choice principles required when the language is uncountable.

Estimated time

beginner: 20m
intermediate: 55m
master: 90m