Contents / Mathematical Logic / Formal Systems and Proofs

Chapter 3

Formal Systems and Proofs

Formal systems, inference rules, natural deduction, soundness, completeness, compactness, and decidability.

Introduction

A formal system replaces the informal notion of proof with a finite object that can be checked mechanically. Fix a language, fix a set of axioms, fix a handful of rules of inference, and " $ϕ$ is provable" becomes a statement about finite strings of symbols — decidable to verify, even when it is undecidable to discover.

Running alongside it is a second, entirely different relation. Semantic entailment asks whether $ϕ$ is true in every structure satisfying the hypotheses, a condition quantifying over structures of every cardinality. The central fact of first-order logic is that these two relations, built from unrelated materials, coincide. Soundness gives one inclusion by an induction any careful reader can run; Gödel's completeness theorem gives the other, and its proof — the Henkin construction — builds a model out of syntax itself. From that one theorem, compactness and the Löwenheim–Skolem theorems fall out as corollaries, and the chapter ends where the method reaches its limit: validity is provable, but not decidable.

3.1Axioms, Rules, and Derivations

A formal system is specified by three pieces of data, and the whole point of the specification is that nothing else is permitted to enter a proof.

Definition 3.1 (Formal system). A formal system $S$ consists of

a language: a set of symbols together with a rule, decidable by inspection, saying which finite strings count as well-formed formulas;
a set of axioms, a distinguished set of well-formed formulas, usually given as axiom schemas — patterns every instance of which is an axiom;
a set of rules of inference, each a relation between a finite list of premises and a conclusion.

$S$ is effective if the three conditions "is a formula", "is an axiom" and "follows from these premises by that rule" are all decidable.

Effectiveness is not decoration. Everything in this chapter that deserves the word formal rests on it: a derivation can be checked by a clerk who does not know what the symbols mean, and — in the last section — the set of theorems can be enumerated by a machine.

Definition 3.2 (Derivation). Let $Γ$ be a set of formulas. A derivation of $ϕ$ from $Γ$ in $S$ is a finite sequence $ψ_{1}, \dots, ψ_{n}$ of formulas with $ψ_{n} = ϕ$ , in which each $ψ_{k}$ is

an axiom of $S$ , or
a member of $Γ$ , or
the conclusion of a rule of $S$ whose premises all occur among $ψ_{1}, \dots, ψ_{k - 1}$ .

We write $Γ ⊢_{S} ϕ$ , read " $Γ$ derives $ϕ$ ", when such a sequence exists, and drop the subscript when $S$ is fixed. A formula with $\emptyset ⊢ ϕ$ is a theorem of $S$ , written $⊢ ϕ$ .

Notation. The turnstile $⊢$ is a syntactic symbol belonging to the metatheory: $Γ ⊢ ϕ$ is a statement about the system, not a formula of it, and it is never written inside a formula. Its semantic counterpart $⊨$ , introduced in the next section, is a different relation with a different definition, and the two are kept apart throughout — conflating them makes the completeness theorem unstatable.

Intuition. A derivation is a board game with no hidden information. Axioms are positions you may place for free; rules say exactly which position may be added next. A referee who knows only the rulebook can confirm a win by scanning the record of play, and cannot be persuaded by a move that merely feels right.

Hilbert systems take the extreme position: many axiom schemas, one rule. The following three schemas, with modus ponens, are complete for the ${\to, \neg}$ -fragment of propositional logic, and they are the system we work in for the rest of the section. Here $ϕ, ψ, χ$ range over all formulas, so each line is a schema with infinitely many instances.

Definition 3.3 (The Hilbert system $H$ ). The axioms of $H$ are all instances of

A1: ϕ \to (ψ \to ϕ),

A2: (ϕ \to (ψ \to χ)) \to ((ϕ \to ψ) \to (ϕ \to χ)),

A3: (\neg ψ \to \neg ϕ) \to (ϕ \to ψ),

and the sole rule is modus ponens (MP): from $ϕ$ and $ϕ \to ψ$ infer $ψ$ .

Example 3.4 (Deriving the identity law). Show that $⊢_{H} p \to p$ .

Solution. The obstacle is that $H$ has no way to "assume $p$ ": every line must be an axiom instance or an MP conclusion. The trick is to use A2 with $ψ$ taken to be $p \to p$ , so that two applications of MP strip the implication down to the target.

$(p \to ((p \to p) \to p)) \to ((p \to (p \to p)) \to (p \to p))$ — A2 with $ϕ = p$ , $ψ = p \to p$ , $χ = p$ .
$p \to ((p \to p) \to p)$ — A1 with $ϕ = p$ , $ψ = p \to p$ .
$(p \to (p \to p)) \to (p \to p)$ — MP on 2 and 1.
$p \to (p \to p)$ — A1 with $ϕ = p$ , $ψ = p$ .
$p \to p$ — MP on 4 and 3.

Five lines, no appeal anywhere to the meaning of $p$ . □□

Five lines for $p \to p$ is a fair warning about Hilbert systems: they are built to be easy to reason about, not to reason in. Their metatheory is short — one rule to check in the soundness induction — and that is exactly the trade we want when proving theorems about provability.

Natural deduction, due to Gentzen, makes the opposite trade. It has no axioms at all; each connective carries an introduction rule saying how to prove a formula with that connective as its main symbol, and an elimination rule saying what may be extracted from one. For implication:

\to I: \frac{Γ , ϕ ⊢ ψ}{Γ ⊢ ϕ \to ψ} \to E: \frac{Γ ⊢ ϕ \to ψ Γ ⊢ ϕ}{Γ ⊢ ψ}

The rule $\to$ I formalises the move every mathematician makes without comment: suppose $ϕ$ ; … ; therefore $ψ$ ; hence if $ϕ$ then $ψ$ . The assumption $ϕ$ is discharged — used inside the subproof, absent from the conclusion. In natural deduction $p \to p$ is one line: assume $p$ , discharge it.

Hilbert systems have no such rule. What they have instead is a theorem of the metatheory saying the rule is admissible: anything $\to$ I would let you conclude, $H$ can already derive. That is the deduction theorem, and it is what makes $H$ usable at all.

Theorem 3.5 (Deduction theorem). In the system $H$ , for every set of formulas $Γ$ and all formulas $ϕ, ψ$ :

Γ \cup {ϕ} ⊢ ψ ⟺ Γ ⊢ ϕ \to ψ .

Proof. ( $\Leftarrow$ ) Suppose $Γ ⊢ ϕ \to ψ$ . Copy that derivation, append the line $ϕ$ (a member of $Γ \cup {ϕ}$ ), and append $ψ$ by MP. This direction needs nothing beyond the definition of a derivation.

( $\Rightarrow$ ) Suppose $ψ_{1}, \dots, ψ_{n}$ is a derivation of $ψ = ψ_{n}$ from $Γ \cup {ϕ}$ . We show by strong induction on $k$ that $Γ ⊢ ϕ \to ψ_{k}$ for every $k \leq n$ ; the case $k = n$ is the claim.

Case 1: $ψ_{k}$ is an axiom of $H$ , or $ψ_{k} \in Γ$ . Then $Γ ⊢ ψ_{k}$ in one line. The A1 instance $ψ_{k} \to (ϕ \to ψ_{k})$ is an axiom, so MP gives $Γ ⊢ ϕ \to ψ_{k}$ in three lines.

Case 2: $ψ_{k}$ is $ϕ$ itself. Then $ϕ \to ψ_{k}$ is $ϕ \to ϕ$ , and the derivation in Example Deriving the identity law goes through with $ϕ$ in place of $p$ , using only axioms, so $Γ ⊢ ϕ \to ϕ$ with no hypotheses at all. This is the case that forces A2 into the axiom list: from A1 alone no derivation of $ϕ \to ϕ$ exists, and the theorem would fail.

Case 3: $ψ_{k}$ follows by MP from earlier lines $ψ_{i}$ and $ψ_{j} = (ψ_{i} \to ψ_{k})$ , with $i, j < k$ . By the induction hypothesis,

Γ ⊢ ϕ \to ψ_{i} and Γ ⊢ ϕ \to (ψ_{i} \to ψ_{k}) .

Take the A2 instance

(ϕ \to (ψ_{i} \to ψ_{k})) \to ((ϕ \to ψ_{i}) \to (ϕ \to ψ_{k})) .

MP with the second induction hypothesis yields $Γ ⊢ (ϕ \to ψ_{i}) \to (ϕ \to ψ_{k})$ , and MP with the first yields $Γ ⊢ ϕ \to ψ_{k}$ .

Every line of the original derivation falls under exactly one case, so the induction is complete.∎

Read the proof again watching what it consumed. Case 1 used A1, Case 2 used A1 and A2, Case 3 used A2, and nothing anywhere used A3. The deduction theorem is a theorem about the implicational fragment: it holds in any Hilbert system containing A1 and A2 and closed under MP. That is worth remembering, because the same argument is reused verbatim for first-order systems.

Pitfall. In first-order logic the deduction theorem needs a side condition. If generalisation (from $ϕ$ infer $\forall x ϕ$ ) is a rule of the system, then ${ϕ (x)} ⊢ \forall x ϕ (x)$ , yet $⊢ ϕ (x) \to \forall x ϕ (x)$ is false — read $ϕ (x)$ as " $x = c$ " in a structure with two elements. The repair is to forbid generalising on a variable occurring free in an undischarged hypothesis.

Example 3.6 (Transitivity of implication, without a subproof). Derive ${ϕ \to ψ, ψ \to χ} ⊢_{H} ϕ \to χ$ .

Solution. By the deduction theorem it is enough to derive $χ$ from ${ϕ \to ψ, ψ \to χ, ϕ}$ , which is immediate: $ϕ$ with $ϕ \to ψ$ gives $ψ$ by MP, and $ψ$ with $ψ \to χ$ gives $χ$ by MP. Three lines, then one appeal to the theorem.

Unwinding the theorem's proof mechanically would turn those three lines into a derivation of about a dozen, every one an A1 or A2 instance. That is the standard experience, and the reason one proves the deduction theorem once rather than repeating the construction each time. □□

Remark. Three properties of $⊢$ follow straight from Definition Derivation and are used without comment from here on. Monotonicity: if $Γ ⊢ ϕ$ and $Γ \subseteq Δ$ then $Δ ⊢ ϕ$ , since the same sequence is still a derivation. Finiteness: if $Γ ⊢ ϕ$ then $Γ_{0} ⊢ ϕ$ for some finite $Γ_{0} \subseteq Γ$ , since a derivation is a finite sequence and can cite only finitely many members of $Γ$ . Transitivity (cut): if $Γ ⊢ ϕ$ and $Δ \cup {ϕ} ⊢ ψ$ then $Γ \cup Δ ⊢ ψ$ , by concatenation. Finiteness is what will later deliver compactness, and it is a property of $⊢$ alone — $⊨$ has no comparable reason to enjoy it.

Exercises for §3.1 →

3.2Truth in a Structure: Entailment Against Derivability

Nothing in the previous section mentioned truth. A derivation is a pattern of symbols, and $Γ ⊢ ϕ$ was settled by looking at finite strings. Semantics starts from the opposite end: it supplies the symbols with meanings and asks what is true.

Definition 3.7 (Structure). Let $L$ be a first-order language with relation symbols, function symbols and constant symbols. An $L$ -structure $M$ consists of a non-empty set $M$ , the domain, together with

a relation $R^{M} \subseteq M^{n}$ for each $n$ -ary relation symbol $R$ of $L$ ,
a function $f^{M} : M^{n} \to M$ for each $n$ -ary function symbol $f$ ,
an element $c^{M} \in M$ for each constant symbol $c$ .

A structure interprets the symbols; an assignment $s$ , mapping variables into $M$ , interprets the free variables. Together they determine, for every formula, whether it holds — and Tarski's definition makes "determine" precise by recursion on the construction of the formula.

Definition 3.8 (Satisfaction). For an $L$ -structure $M$ and an assignment $s$ , write $M ⊨ ϕ [s]$ (" $M$ satisfies $ϕ$ under $s$ ") according to the clauses

$M ⊨ (t_{1} = t_{2}) [s]$ iff $t_{1}$ and $t_{2}$ denote the same element of $M$ under $s$ ;
$M ⊨ R (t_{1}, \dots, t_{n}) [s]$ iff the denoted tuple lies in $R^{M}$ ;
$M ⊨ \neg ϕ [s]$ iff $M ⊨ ϕ [s]$ fails;
$M ⊨ (ϕ \to ψ) [s]$ iff $M ⊨ ϕ [s]$ fails or $M ⊨ ψ [s]$ holds;
$M ⊨ \forall x ϕ [s]$ iff $M ⊨ ϕ [s (x \mapsto a)]$ for every $a \in M$ .

For a sentence — a formula with no free variables — the assignment is irrelevant, and we write $M ⊨ ϕ$ .

Definition 3.9 (Entailment, validity, satisfiability). Let $Γ$ be a set of sentences and $ϕ$ a sentence.

$M$ is a model of $Γ$ , written $M ⊨ Γ$ , if $M ⊨ γ$ for every $γ \in Γ$ .
$Γ$ entails $ϕ$ , written $Γ ⊨ ϕ$ , if every model of $Γ$ is a model of $ϕ$ .
$ϕ$ is valid, written $⊨ ϕ$ , if every structure is a model of $ϕ$ .
$Γ$ is satisfiable if it has at least one model.

Notation. The symbol $⊨$ is now doing two jobs, and both are standard. With a structure on the left ( $M ⊨ ϕ$ ) it is satisfaction; with a set of sentences on the left ( $Γ ⊨ ϕ$ ) it is entailment. The left argument disambiguates. What $⊨$ never means is derivability: $Γ ⊨ ϕ$ mentions no axioms, no rules and no proofs, and $Γ ⊢ ϕ$ mentions no structures.

The two relations differ in kind, not merely in definition, and it pays to say exactly how.

	$Γ ⊢ ϕ$	$Γ ⊨ ϕ$
decided by	a finite derivation	all structures interpreting $L$
witness	a finite object one can write down	none in general
depends on	the chosen axioms and rules	nothing but the language
verifying a positive case	mechanical	a proof in the metatheory
verifying a negative case	no finite object certifies it directly	one countermodel suffices

Intuition. $⊢$ is a claim about a search space: somewhere among the finite strings there sits a certificate. $⊨$ is a claim about a universe: every structure whatsoever, of every size, makes $ϕ$ true whenever it makes $Γ$ true. There is no a priori reason for these to have anything to do with each other, and for most consequence relations they do not. That first-order logic makes them agree is a theorem, not a definition.

Refuting an entailment is the easy direction, and the technique is always the same: exhibit one structure.

Example 3.10 (A non-entailment). Let $L$ have one binary relation $R$ . Show that

\forall x \exists y R (x, y) \neq ⊨ \exists y \forall x R (x, y) .

Solution. Take $M = Z$ and $R^{M} = {(a, b) : b > a}$ . Every integer has some larger integer, so $M ⊨ \forall x \exists y R (x, y)$ . But no integer $b$ exceeds every integer $a$ , so $M ⊨ \exists y \forall x R (x, y)$ fails.

One structure satisfying the hypothesis and falsifying the conclusion is exactly what "not every model of the hypothesis is a model of the conclusion" asks for. □□

Pitfall. A countermodel refutes an entailment, never a derivation. The two tasks are related only through the soundness and completeness theorems, and it is worth noticing which theorem you are leaning on: using a countermodel to conclude $Γ ⊬ ϕ$ is an application of soundness, in contrapositive form.

Example 3.11 (Entailment with an infinite hypothesis set). Let $L$ contain constants $c_{0}, c_{1}, c_{2}, \dots$ and let

Γ = {c_{i} \neq = c_{j} : i < j} .

Show that $Γ ⊨ \exists x \exists y (x \neq = y)$ , and that no finite subset of $Γ$ decides the size of a model beyond a fixed bound.

Solution. Any model of $Γ$ interprets $c_{0}$ and $c_{1}$ as distinct elements, so it satisfies $\exists x \exists y (x \neq = y)$ ; that is the entailment. For the second claim, a finite $Γ_{0} \subseteq Γ$ mentions only constants among $c_{0}, \dots, c_{N}$ for some $N$ , and a structure with $N + 1$ elements interpreting those constants injectively — and every remaining $c_{k}$ arbitrarily — is a model of $Γ_{0}$ .

So each finite fragment is satisfiable in a finite domain, while $Γ$ itself is not: any model of the whole of $Γ$ has infinitely many elements. Hold on to this example. It is the mechanism behind every application of compactness later in the chapter, and behind the fact that "the domain is finite" is not expressible by any single first-order sentence. □□

Remark. Two conditions on a set $Γ$ will run in parallel for the rest of the chapter, and the notation separates them the same way. $Γ$ is satisfiable if some structure models it — a semantic condition. $Γ$ is consistent if $Γ ⊬ ⊥$ — a syntactic one, defined in the section on consistency below.

That these two conditions coincide is the completeness theorem in its sharpest form, and the sections ahead earn each direction in turn: soundness gives satisfiable $\Rightarrow$ consistent, and the Henkin construction gives consistent $\Rightarrow$ satisfiable.

Exercises for §3.2 →

3.3Soundness: Derivability Implies Entailment

Soundness is the promise that the machinery of the first section never manufactures a falsehood. It is the easy half of the correspondence, and the proof is a template worth learning in full, because every extension of a formal system is verified by re-running it on the new axioms and rules.

Theorem 3.12 (Soundness). For every set of sentences $Γ$ and every sentence $ϕ$ ,

Γ ⊢ ϕ ⟹ Γ ⊨ ϕ .

The proof needs exactly two inputs, and isolating them is the whole method.

Lemma 3.13 (Axioms are valid). Every instance of A1, A2 and A3 is valid: it is true under every structure and assignment.

Proof. Fix a structure and assignment; each of $ϕ, ψ, χ$ then has a definite truth value, and by the satisfaction clause for $\to$ it suffices to check the four (or eight) combinations.

A1, $ϕ \to (ψ \to ϕ)$ . If $ϕ$ is false the implication is true by the clause. If $ϕ$ is true, then $ψ \to ϕ$ is true, since its consequent is; so the implication is true again.

A2, $(ϕ \to (ψ \to χ)) \to ((ϕ \to ψ) \to (ϕ \to χ))$ . Suppose the whole formula were false. Then $ϕ \to (ψ \to χ)$ is true, $ϕ \to ψ$ is true and $ϕ \to χ$ is false. The last makes $ϕ$ true and $χ$ false. From $ϕ$ true and $ϕ \to ψ$ true, $ψ$ is true. From $ϕ$ true and $ϕ \to (ψ \to χ)$ true, $ψ \to χ$ is true; with $ψ$ true this forces $χ$ true, contradicting $χ$ false.

A3, $(\neg ψ \to \neg ϕ) \to (ϕ \to ψ)$ . Suppose it were false: then $\neg ψ \to \neg ϕ$ is true while $ϕ$ is true and $ψ$ is false. From $ψ$ false, $\neg ψ$ is true, so $\neg ϕ$ is true, so $ϕ$ is false — contradicting $ϕ$ true.∎

Lemma 3.14 (Modus ponens preserves truth). If $M ⊨ ϕ [s]$ and $M ⊨ (ϕ \to ψ) [s]$ , then $M ⊨ ψ [s]$ .

Proof. By the satisfaction clause, $M ⊨ (ϕ \to ψ) [s]$ means that $M ⊨ ϕ [s]$ fails or $M ⊨ ψ [s]$ holds. The first disjunct is excluded by hypothesis, so the second holds.∎

With the two lemmas in hand, the theorem is an induction on the position of a line in the derivation — the standard form of "induction on derivations" for a linear proof system.

Proof. Let $ψ_{1}, \dots, ψ_{n}$ be a derivation of $ϕ = ψ_{n}$ from $Γ$ , and let $M$ be any model of $Γ$ . We prove by strong induction on $k$ that $M ⊨ ψ_{k}$ for every $k \leq n$ .

Fix $k$ and assume $M ⊨ ψ_{i}$ for all $i < k$ . By Definition Derivation, $ψ_{k}$ arises in one of three ways.

$ψ_{k}$ is an axiom. Then $M ⊨ ψ_{k}$ by Lemma Axioms are valid, which holds in every structure and so in particular in $M$ .
$ψ_{k} \in Γ$ . Then $M ⊨ ψ_{k}$ because $M$ is a model of $Γ$ .
$ψ_{k}$ follows by MP from $ψ_{i}$ and $ψ_{j} = (ψ_{i} \to ψ_{k})$ with $i, j < k$ . The induction hypothesis gives $M ⊨ ψ_{i}$ and $M ⊨ ψ_{i} \to ψ_{k}$ , and Lemma Modus ponens preserves truth gives $M ⊨ ψ_{k}$ .

Hence $M ⊨ ψ_{n} = ϕ$ . As $M$ was an arbitrary model of $Γ$ , every model of $Γ$ models $ϕ$ , i.e. $Γ ⊨ ϕ$ .∎

Remark. The induction is on the derivation, not on the formula. Structural induction on formulas is a different tool, used in the satisfaction lemmas above; induction on derivations is what lets a proof about $⊢$ dispose of a proof of unbounded length by looking at one line at a time. In a tree-shaped system such as natural deduction the same argument runs as induction on the height of the derivation tree, one case per rule.

Intuition. Soundness is a safety guarantee, and the shape of the argument says why it holds: truth is an invariant of the derivation process. The axioms start inside the invariant, every rule keeps you inside it, and so every line you can ever reach is inside it. An unsound system is one with either a false axiom or a rule that can step out.

The theorem is usually applied in its contrapositive form, where it becomes a tool for proving unprovability — otherwise a hard thing to establish, since no finite object certifies the absence of a derivation.

Corollary 3.15 (Consistency from satisfiability). If $Γ$ has a model, then there is no sentence $ϕ$ with both $Γ ⊢ ϕ$ and $Γ ⊢ \neg ϕ$ . In the vocabulary of the next section: every satisfiable set is consistent.

Proof. Suppose $M ⊨ Γ$ while $Γ ⊢ ϕ$ and $Γ ⊢ \neg ϕ$ . Soundness applied twice gives $Γ ⊨ ϕ$ and $Γ ⊨ \neg ϕ$ , so $M ⊨ ϕ$ and $M ⊨ \neg ϕ$ . The satisfaction clause for $\neg$ makes the second say that $M ⊨ ϕ$ fails — a contradiction.∎

Example 3.16 (Unprovability by countermodel). Show that $\forall x \exists y R (x, y) ⊬ \exists y \forall x R (x, y)$ in any sound system.

Solution. Example A non-entailment produced the structure $(Z, >)$ , a model of the hypothesis in which the conclusion fails; so the entailment does not hold. If the derivation existed, soundness would force the entailment. Hence no derivation exists.

Notice what has been proved and in which system: the argument rules out a derivation in every sound system at once, without examining a single axiom list. That leverage is the practical value of soundness. □□

Pitfall. Soundness is not consistency, and consistency does not give it back. Consistency says the theory proves no contradiction; soundness says it proves nothing false in the intended structure. In the language of arithmetic the theory $T = {\forall x \forall y (x = y)}$ is consistent — the one-element structure is a model — yet thoroughly unsound for $N$ , since it proves $0 = 1$ . The implication runs one way only: a theory sound for some structure is consistent, by Corollary Consistency from satisfiability.

Exercises for §3.3 →

3.4Consistency, Maximal Consistent Sets, and Lindenbaum's Lemma

Completeness will be proved by building a model out of syntax. The raw material for that construction is a set of sentences so rich that it decides every question — a maximal consistent set — and this section assembles it. Everything here is pure proof theory: no structure is mentioned until the next section.

Definition 3.17 (Consistency). A set of sentences $Γ$ is inconsistent if there is a sentence $ϕ$ with $Γ ⊢ ϕ$ and $Γ ⊢ \neg ϕ$ , and consistent otherwise. We abbreviate " $Γ$ is inconsistent" by $Γ ⊢ ⊥$ .

Lemma 3.18 (Ex falso). If $Γ$ is inconsistent then $Γ ⊢ ψ$ for every sentence $ψ$ . Consequently an inconsistent set derives everything, and consistency is equivalent to the existence of even one underivable sentence.

Proof. Suppose $Γ ⊢ ϕ$ and $Γ ⊢ \neg ϕ$ , and let $ψ$ be arbitrary. Continue the derivations as follows. The A1 instance $\neg ϕ \to (\neg ψ \to \neg ϕ)$ is an axiom, so MP with $\neg ϕ$ gives $Γ ⊢ \neg ψ \to \neg ϕ$ . The A3 instance $(\neg ψ \to \neg ϕ) \to (ϕ \to ψ)$ is an axiom, so MP gives $Γ ⊢ ϕ \to ψ$ . MP with $ϕ$ gives $Γ ⊢ ψ$ .∎

This is the first place A3 has earned its keep: negation is what turns one contradiction into total collapse, which is why "consistent" is such a strong condition on a set of sentences.

Lemma 3.19 (Reductio). For every set $Γ$ and sentence $ϕ$ :

$Γ \cup {\neg ϕ}$ is inconsistent if and only if $Γ ⊢ ϕ$ ;
$Γ \cup {ϕ}$ is inconsistent if and only if $Γ ⊢ \neg ϕ$ .

Proof. Both "if" directions are immediate: if $Γ ⊢ ϕ$ then $Γ \cup {\neg ϕ}$ derives both $ϕ$ (by monotonicity) and $\neg ϕ$ (in one line), and symmetrically for (2).

For the "only if" directions, suppose $Γ \cup {χ}$ is inconsistent, where $χ$ is $\neg ϕ$ in case (1) and $ϕ$ in case (2). Then $Γ \cup {χ} ⊢ ψ$ and $Γ \cup {χ} ⊢ \neg ψ$ for some $ψ$ , and the deduction theorem turns these into

Γ ⊢ χ \to ψ and Γ ⊢ χ \to \neg ψ .

Two schemas of $H$ finish the job, one for each case:

(\neg ϕ \to ψ) \to ((\neg ϕ \to \neg ψ) \to ϕ), (ϕ \to ψ) \to ((ϕ \to \neg ψ) \to \neg ϕ) .

Both are derivable from A1–A3 by modus ponens — routine but lengthy exercises of exactly the kind the deduction theorem exists to shorten — and two applications of MP then give $Γ ⊢ ϕ$ in case (1) and $Γ ⊢ \neg ϕ$ in case (2).∎

Lemma 3.20 (Consistency is a finite condition). $Γ$ is consistent if and only if every finite subset of $Γ$ is consistent.

Proof. If some finite $Γ_{0} \subseteq Γ$ is inconsistent, monotonicity makes $Γ$ inconsistent. Conversely, if $Γ ⊢ ϕ$ and $Γ ⊢ \neg ϕ$ , then by finiteness of $⊢$ (Remark following the deduction theorem) there are finite $Γ_{1}, Γ_{2} \subseteq Γ$ with $Γ_{1} ⊢ ϕ$ and $Γ_{2} ⊢ \neg ϕ$ ; the finite set $Γ_{1} \cup Γ_{2} \subseteq Γ$ is then inconsistent.∎

That lemma is where compactness is really born. It is a statement about $⊢$ , proved from the fact that derivations are finite, and the completeness theorem is what will transport it to the semantic side.

Sets that decide everything

Definition 3.21 (Maximal consistent set). A set of sentences $Δ$ is maximal consistent if $Δ$ is consistent and no proper superset of $Δ$ is consistent: for every sentence $ϕ \in / Δ$ , the set $Δ \cup {ϕ}$ is inconsistent.

Lemma 3.22 (Properties of a maximal consistent set). Let $Δ$ be maximal consistent. Then for all sentences $ϕ, ψ$ :

$Δ$ is deductively closed: if $Δ ⊢ ϕ$ then $ϕ \in Δ$ .
Negation-completeness: exactly one of $ϕ \in Δ$ , $\neg ϕ \in Δ$ holds.
$(ϕ \to ψ) \in Δ$ if and only if $ϕ \in / Δ$ or $ψ \in Δ$ .

Proof. (1) Suppose $Δ ⊢ ϕ$ but $ϕ \in / Δ$ . By maximality $Δ \cup {ϕ}$ is inconsistent, so Lemma Reductio (2) gives $Δ ⊢ \neg ϕ$ ; with $Δ ⊢ ϕ$ this makes $Δ$ inconsistent, a contradiction.

(2) Not both, since that would make $Δ$ inconsistent outright. At least one: if $ϕ \in / Δ$ then $Δ \cup {ϕ}$ is inconsistent by maximality, so $Δ ⊢ \neg ϕ$ by Lemma Reductio (2), and $\neg ϕ \in Δ$ by part (1) above.

(3) ( $\Rightarrow$ ) If $(ϕ \to ψ) \in Δ$ and $ϕ \in Δ$ , then $Δ ⊢ ψ$ by MP, so $ψ \in Δ$ by (1). ( $\Leftarrow$ ) If $ψ \in Δ$ , the A1 instance $ψ \to (ϕ \to ψ)$ gives $Δ ⊢ ϕ \to ψ$ , hence $(ϕ \to ψ) \in Δ$ . If instead $ϕ \in / Δ$ then $\neg ϕ \in Δ$ by (2), and the derivation inside Lemma Ex falso gives $Δ ⊢ ϕ \to ψ$ ; apply (1).∎

Intuition. A maximal consistent set is an opinionated theory: for every sentence in the language it has already taken a side, and it never contradicts itself. Clause (3) is the striking one — the membership table for $\to$ inside $Δ$ is exactly the truth table for $\to$ . That coincidence is not luck; it is the reason a maximal consistent set can be read as a model, which is precisely what the next section does.

Pitfall. Maximal consistent is not the same as complete-and-recursively-axiomatised. Lindenbaum's lemma below hands you a maximal consistent extension of any consistent theory, so every consistent theory has a negation-complete extension — and Gödel's first incompleteness theorem is not thereby contradicted. What Gödel rules out is a negation-complete effective extension of arithmetic; the set produced below is in general not decidable, and the construction gives no way to recognise its members.

Theorem 3.23 (Lindenbaum's lemma). Every consistent set of sentences $Γ$ is contained in a maximal consistent set $Δ$ .

Proof. Suppose first that the language is countable, so the sentences may be enumerated as $ϕ_{0}, ϕ_{1}, ϕ_{2}, \dots$ . Define an increasing chain of sets by

Δ_{0} = Γ, Δ_{n + 1} = {Δ_{n} \cup {ϕ_{n}} Δ_{n} if this set is consistent, otherwise,

and put $Δ = ⋃_{n \geq 0} Δ_{n}$ .

Each $Δ_{n}$ is consistent, by induction: $Δ_{0} = Γ$ is consistent by hypothesis, and the recursion adds $ϕ_{n}$ only when consistency survives.

$Δ$ is consistent. Suppose not. By Lemma Consistency is a finite condition some finite $Δ^{'} \subseteq Δ$ is inconsistent. Each member of $Δ^{'}$ entered at some stage, and $Δ^{'}$ is finite, so all of them lie in $Δ_{N}$ for $N$ the largest such stage — the chain is increasing. Then $Δ_{N}$ is inconsistent by monotonicity, contradicting the previous paragraph.

$Δ$ is maximal. Let $ϕ \in / Δ$ and let $n$ be its index in the enumeration, $ϕ = ϕ_{n}$ . Since $ϕ_{n} \in / Δ \supseteq Δ_{n + 1}$ , the recursion must have taken the second branch, i.e. $Δ_{n} \cup {ϕ_{n}}$ was inconsistent. As $Δ_{n} \subseteq Δ$ , monotonicity makes $Δ \cup {ϕ}$ inconsistent too.

For an arbitrary language, replace the enumeration by Zorn's lemma. Order by inclusion the set $P$ of consistent supersets of $Γ$ ; it is non-empty since $Γ \in P$ . If $C \subseteq P$ is a chain, then $⋃ C$ is consistent — any inconsistency would involve a finite subset, which by the chain property lies inside a single member of $C$ — so $⋃ C \in P$ is an upper bound for $C$ . Zorn's lemma supplies a maximal element $Δ$ of $P$ , and maximality in $P$ is exactly maximal consistency.∎

Remark. The two arguments are the same argument. Both rest entirely on Lemma Consistency is a finite condition: consistency is a property of finite character, and a property of finite character is preserved under unions of chains. The countable case simply replaces the choice principle with an explicit enumeration, which is why it needs no appeal to the axiom of choice — worth noting, because the general Lindenbaum lemma, and hence completeness for uncountable languages, genuinely does use choice (the Boolean prime ideal theorem suffices).

Example 3.24 (Maximal consistent sets need not be unique). Let $Γ = \emptyset$ in a propositional language with one atom $p$ . Describe the maximal consistent sets extending $Γ$ .

Solution. By negation-completeness, a maximal consistent $Δ$ contains exactly one of $p$ , $\neg p$ . Each choice extends to a maximal consistent set: take $Δ^{+}$ to be all sentences true under the valuation $p \mapsto true$ , and $Δ^{-}$ all sentences true under $p \mapsto false$ . Both are consistent (each is the set of sentences satisfied by an actual valuation, so Corollary Consistency from satisfiability applies) and each is negation-complete, hence maximal by property (2) read backwards.

So there are exactly two, one per valuation of $p$ . Lindenbaum's lemma promises a maximal extension, never a canonical one — and the ambiguity is not a defect: distinct maximal consistent sets are what distinct models look like from the syntactic side. □□

Exercises for §3.4 →

3.5Gödel's Completeness Theorem

Soundness said the proof system is safe. Completeness says it is not timid: everything that follows semantically is already derivable, so the finite certificates of the first section exhaust the infinitary relation of the second.

Theorem 3.25 (Gödel's completeness theorem). Let $Γ$ be a set of sentences and $ϕ$ a sentence of a first-order language. Then

Γ ⊨ ϕ ⟹ Γ ⊢ ϕ .

Combined with Theorem Soundness, the two relations coincide: $Γ ⊢ ϕ$ if and only if $Γ ⊨ ϕ$ .

Why is this surprising? $Γ ⊨ ϕ$ quantifies over every structure interpreting the language — domains of every cardinality, a collection far too large to inspect. The theorem says that this unbounded semantic fact is always witnessed by a finite string of symbols. Nothing in the definitions suggests it; the proof has to produce the derivation, or produce something equivalent to it.

The standard route, due to Henkin, produces neither directly. It proves a statement about consistency instead, and lets Lemma Reductio convert it.

Theorem 3.26 (Model existence). Every consistent set of sentences has a model.

Proof. (Completeness, granted model existence.) Suppose $Γ ⊨ ϕ$ and, for contradiction, $Γ ⊬ ϕ$ . By Lemma Reductio (1), $Γ \cup {\neg ϕ}$ is consistent, so by model existence it has a model $M$ . Then $M ⊨ Γ$ , so $Γ ⊨ ϕ$ gives $M ⊨ ϕ$ ; but $M ⊨ \neg ϕ$ says $M ⊨ ϕ$ fails. Contradiction, so $Γ ⊢ ϕ$ .

The work is therefore entirely in model existence, proved below.∎

The idea of the construction is startling on first meeting: if the sentences cannot be interpreted by anything else, interpret them by themselves. The domain of the model will be built from the closed terms of the language, and a sentence will be declared true exactly when it belongs to a maximal consistent set. Two obstacles stand in the way, and the construction is designed around them.

Obstacle 1: existential sentences need witnesses. A maximal consistent $Δ$ may contain $\exists x ϕ (x)$ while containing no closed term $t$ with $ϕ (t) \in Δ$ . The term model would then have to make $\exists x ϕ (x)$ true with nothing in its domain to satisfy $ϕ$ . The repair is to add constants that supply the missing witnesses.

Obstacle 2: equality. The terms $t$ and $u$ are different strings, but $Δ$ may contain $t = u$ , which the model must respect. The repair is a quotient.

Definition 3.27 (Henkin theory). A set of sentences $Δ$ in a language $L$ has witnesses (is a Henkin theory) if for every formula $ϕ (x)$ with one free variable there is a closed term $c$ of $L$ such that

(\exists x ϕ (x) \to ϕ (c)) \in Δ.

Lemma 3.28 (Witnesses can be added). Let $Γ$ be a consistent set of $L$ -sentences. Then there is a language $L^{*} \supseteq L$ , obtained by adding new constant symbols, and a consistent set $Γ^{*} \supseteq Γ$ of $L^{*}$ -sentences which has witnesses. If $L$ is countable, so is $L^{*}$ .

Proof. For each $L$ -formula $ϕ (x)$ with one free variable introduce a fresh constant $c_{ϕ}$ , and let $L_{1} = L \cup {c_{ϕ}}$ . Put

Γ_{1} = Γ \cup {\exists x ϕ (x) \to ϕ (c_{ϕ}) : ϕ (x) an L -formula with one free variable} .

$Γ_{1}$ is consistent. By Lemma Consistency is a finite condition it is enough to check finite subsets, so suppose finitely many Henkin axioms were inconsistent with $Γ$ ; take one of them, for the formula $ϕ$ , added last. Reductio and the deduction theorem give $Γ^{'} ⊢ \neg (\exists x ϕ (x) \to ϕ (c_{ϕ}))$ for the remaining set $Γ^{'}$ , whence $Γ^{'} ⊢ \exists x ϕ (x)$ and $Γ^{'} ⊢ \neg ϕ (c_{ϕ})$ . But $c_{ϕ}$ is fresh: it occurs nowhere in $Γ^{'}$ , so it behaves as a free variable, and generalising on it gives $Γ^{'} ⊢ \forall x \neg ϕ (x)$ — contradicting $Γ^{'} ⊢ \exists x ϕ (x)$ . This freshness argument is the heart of the lemma; it is exactly the side condition on generalisation from the Pitfall in the first section, used here in the direction it was designed for.

Iterate. The new constants create new formulas, which need witnesses of their own, so repeat: $L_{n + 1}$ and $Γ_{n + 1}$ are built from $L_{n}$ and $Γ_{n}$ the same way. Set $L^{*} = ⋃_{n} L_{n}$ and $Γ^{*} = ⋃_{n} Γ_{n}$ . The union is consistent, again because an inconsistency would be finite and would therefore already live in some $Γ_{n}$ . Every $L^{*}$ -formula has all its constants in some $L_{n}$ , so its witness axiom was added at stage $n + 1$ : $Γ^{*}$ has witnesses. Each stage adds countably many constants to a countable language, so $L^{*}$ is countable when $L$ is.∎

Lemma 3.29 (Truth lemma). Let $Δ$ be a maximal consistent Henkin theory in a language $L^{*}$ . Define a structure $M_{Δ}$ as follows. On the set of closed $L^{*}$ -terms put $t \sim u$ iff $(t = u) \in Δ$ ; take the domain to be the set of classes $[t]$ ; interpret each constant $c$ as $[c]$ , each function symbol by $f^{M} ([t_{1}], \dots, [t_{n}]) = [f (t_{1}, \dots, t_{n})]$ , and each relation symbol by $([t_{1}], \dots, [t_{n}]) \in R^{M}$ iff $R (t_{1}, \dots, t_{n}) \in Δ$ . Then for every $L^{*}$ -sentence $σ$ ,

M_{Δ} ⊨ σ ⟺ σ \in Δ.

Proof. First, $\sim$ is an equivalence relation and the interpretations are well defined, because $Δ$ is deductively closed and the equality axioms (reflexivity, symmetry, transitivity, congruence for $f$ and $R$ ) are derivable; deductive closure, Lemma Properties of a maximal consistent set (1), puts their instances in $Δ$ . The domain is non-empty since $L^{*}$ has constants.

Now induct on the number of connectives and quantifiers in $σ$ .

Atomic. $M_{Δ} ⊨ R (t_{1}, \dots, t_{n})$ holds iff $R (t_{1}, \dots, t_{n}) \in Δ$ , by definition of $R^{M}$ ; likewise for $t = u$ by definition of $\sim$ .

Negation. $M_{Δ} ⊨ \neg σ$ iff $M_{Δ} ⊨ σ$ fails iff (induction hypothesis) $σ \in / Δ$ iff (negation-completeness, property (2)) $\neg σ \in Δ$ .

Implication. $M_{Δ} ⊨ σ \to τ$ iff $M_{Δ} ⊨ σ$ fails or $M_{Δ} ⊨ τ$ , which by the induction hypothesis is " $σ \in / Δ$ or $τ \in Δ$ ", which is $(σ \to τ) \in Δ$ by property (3).

Existential. Write $\exists x ϕ (x)$ for $\neg\forall x \neg ϕ (x)$ . Suppose $\exists x ϕ (x) \in Δ$ . Because $Δ$ has witnesses, $\exists x ϕ (x) \to ϕ (c) \in Δ$ for some closed term $c$ , so $ϕ (c) \in Δ$ by MP and deductive closure, so $M_{Δ} ⊨ ϕ (c)$ by the induction hypothesis — and $[c]$ is an element of the domain satisfying $ϕ$ . Conversely, if $M_{Δ} ⊨ \exists x ϕ (x)$ then some class $[t]$ satisfies $ϕ$ , so $ϕ (t) \in Δ$ by the induction hypothesis, and $ϕ (t) \to \exists x ϕ (x)$ is derivable, so $\exists x ϕ (x) \in Δ$ .

Every element of the domain is $[t]$ for a closed term $t$ — this is why the witnesses were needed, and it is the only point where a term model differs from an arbitrary structure. The universal case follows from the existential one and negation.∎

The three lemmas now assemble with nothing left over.

Proof. (Model existence.) Let $Γ$ be consistent. By Lemma Witnesses can be added, extend it to a consistent $Γ^{*}$ with witnesses in a language $L^{*}$ . By Lindenbaum's lemma, extend $Γ^{*}$ to a maximal consistent set $Δ \supseteq Γ^{*}$ of $L^{*}$ -sentences; adding sentences preserves the witness property, so $Δ$ is a maximal consistent Henkin theory. By the truth lemma, $M_{Δ} ⊨ σ$ for every $σ \in Δ$ , in particular for every $σ \in Γ$ . Finally, discard the interpretations of the constants of $L^{*} ∖ L$ : the resulting $L$ -structure still models $Γ$ , since the truth of an $L$ -sentence does not depend on symbols it never mentions.∎

Figure 3.30. The Henkin construction. The consistent set

Γ

is enlarged twice — first by witness axioms in an expanded language, then by Lindenbaum's lemma to a maximal consistent

Δ

— and the truth lemma converts the final set into the term model

M_{Δ}

, whose elements are equivalence classes of closed terms. Each enlargement preserves consistency; only the last step leaves syntax.

Intuition. The construction answers "where could a model possibly come from?" with: from the syntax, and from nothing else. The elements of the model are the names the language can write down; the facts of the model are the sentences the theory has decided to accept. Consistency is what makes this coherent, maximality is what makes every question have an answer, and the witnesses are what stop the language from asserting the existence of something it cannot name.

Remark. Three ingredients carried the proof, and none can be dropped. Lindenbaum's lemma supplies negation-completeness, without which the truth lemma has no case for $\neg$ . The Henkin extension supplies witnesses, without which the existential case fails. The quotient by $\sim$ makes equality a genuine identity rather than a relation. For a countable language the whole argument avoids the axiom of choice beyond an explicit enumeration; in general it uses the Boolean prime ideal theorem, strictly weaker than full choice.

Pitfall. Completeness is about derivability of consequences, not about theories deciding every sentence. A theory $T$ is called negation-complete when $T ⊢ σ$ or $T ⊢ \neg σ$ for every $σ$ ; Gödel's incompleteness theorem says no effective consistent extension of arithmetic is negation-complete. The two theorems are both Gödel's and both true, because they are about different things: the completeness theorem concerns the logic, incompleteness concerns a particular theory.

Exercises for §3.5 →

3.6Compactness and the Löwenheim–Skolem Theorems

The completeness theorem is not only a statement about proofs. Because it identifies a semantic relation with a syntactic one, every property of derivations transfers to semantics — and derivations have one property semantics had no right to expect. They are finite.

Theorem 3.31 (Compactness). Let $Γ$ be a set of sentences. If every finite subset of $Γ$ is satisfiable, then $Γ$ is satisfiable. Equivalently: if $Γ ⊨ ϕ$ , then $Γ_{0} ⊨ ϕ$ for some finite $Γ_{0} \subseteq Γ$ .

Proof. Suppose every finite subset of $Γ$ is satisfiable. By Corollary Consistency from satisfiability, every finite subset of $Γ$ is consistent, so $Γ$ is consistent by Lemma Consistency is a finite condition. By Theorem Model existence, $Γ$ has a model, i.e. $Γ$ is satisfiable.

For the second form, suppose $Γ ⊨ ϕ$ . By completeness $Γ ⊢ ϕ$ ; by finiteness of $⊢$ some finite $Γ_{0} \subseteq Γ$ has $Γ_{0} ⊢ ϕ$ ; by soundness $Γ_{0} ⊨ ϕ$ .∎

Intuition. Trace the finiteness through the argument and you see where compactness comes from. A derivation is a finite sequence, so it can cite only finitely much of $Γ$ ; completeness says every semantic consequence has such a derivation; therefore every semantic consequence already follows from finitely much of $Γ$ . The theorem is the finiteness of proofs, viewed through the mirror that completeness provides.

Pitfall. Compactness earns its keep on infinite $Γ$ ; on a finite $Γ$ it says nothing, since $Γ$ is one of its own finite subsets. The characteristic application has exactly the shape of Example Entailment with an infinite hypothesis set: infinitely many sentences, each finite fragment satisfiable in a small structure, and a conclusion about the infinite whole that no single fragment could reach.

Example 3.32 (Arbitrarily large finite models force an infinite one). Let $T$ be a theory with finite models of unbounded size. Show that $T$ has an infinite model.

Solution. For $n \geq 2$ let

λ_{n} : \exists x_{1} \dots \exists x_{n} i < j ⋀ x_{i} \neq = x_{j},

the sentence "there are at least $n$ distinct elements", and set $T^{'} = T \cup {λ_{2}, λ_{3}, \dots}$ .

Take any finite $Δ \subseteq T^{'}$ . It mentions finitely many of the $λ_{n}$ ; let $N$ be the largest index among them. By hypothesis $T$ has a finite model $M$ with at least $N$ elements, and such an $M$ satisfies $λ_{2}, \dots, λ_{N}$ , hence all of $Δ$ . So every finite subset of $T^{'}$ is satisfiable, and compactness gives a model $N ⊨ T^{'}$ . Since $N ⊨ λ_{n}$ for every $n$ , the domain of $N$ has at least $n$ elements for every $n$ : it is infinite. And $N ⊨ T$ .

No single finite model was infinite, of course; each finite fragment was satisfied by a different one, and compactness is exactly the tool that stitches those separate witnesses into one structure. □□

Corollary 3.33 (Finiteness is not first-order expressible). There is no set of first-order sentences whose models are exactly the finite structures — and in particular no single sentence.

Proof. Such a set $Σ$ would have finite models of unbounded size, since every finite structure is a model. By the example above it would then have an infinite model, contradicting the requirement that its models be exactly the finite ones.∎

Example 3.34 (Non-standard models of arithmetic). Let $Th (N)$ be the set of all first-order sentences true in the standard model of arithmetic. Produce a model of $Th (N)$ containing an element larger than every numeral.

Solution. Add a fresh constant $c$ and let

Γ = Th (N) \cup {c > \underline{n} : n \in N},

where $\underline{n}$ is the numeral $1 + \dots + 1$ with $n$ ones. A finite subset mentions $c > \underline{n}$ only for $n \leq N$ , and $N$ itself models it once $c$ is interpreted as $N + 1$ ; the sentences of $Th (N)$ say nothing about $c$ . So every finite subset is satisfiable, and compactness gives $M ⊨ Γ$ .

In $M$ the element $c^{M}$ exceeds every numeral, so it is not the interpretation of any numeral: $M$ is a non-standard model. Yet $M$ satisfies every first-order truth of arithmetic, since $Th (N) \subseteq Γ$ . First-order logic therefore cannot pin down $N$ up to isomorphism — not even by taking every truth about it as an axiom. □□

The Henkin construction pays a second dividend, and it is a statement about size. Look again at the model built in the previous section: its domain consists of equivalence classes of closed terms of $L^{*}$ , and $L^{*}$ is countable whenever $L$ is. The model the proof produces is therefore small, whatever the theory may have been trying to describe.

Theorem 3.35 (Downward Löwenheim–Skolem). Let $L$ be a countable language. Every satisfiable set of $L$ -sentences has a countable model. More generally, for a language of cardinality $κ$ , every satisfiable set has a model of cardinality at most $κ + ℵ_{0}$ .

Proof. Let $Γ$ be satisfiable; by Corollary Consistency from satisfiability it is consistent. Run the proof of Theorem Model existence. Lemma Witnesses can be added keeps a countable language countable, since each of its countably many stages adds one constant per formula of a countable language. The domain of $M_{Δ}$ is a set of equivalence classes of closed terms of $L^{*}$ , and there are only countably many such terms, so the domain is countable (and non-empty). The cardinality bound in the general case is the same count with $κ$ in place of $ℵ_{0}$ .∎

Theorem 3.36 (Upward Löwenheim–Skolem). If a set of sentences $Γ$ has an infinite model, then it has a model of every infinite cardinality $κ$ at least as large as the language.

Proof. Add $κ$ fresh constants ${c_{α} : α < κ}$ and let

Γ^{'} = Γ \cup {c_{α} \neq = c_{β} : α < β < κ} .

Any finite subset mentions finitely many constants, and the given infinite model of $Γ$ interprets them as distinct elements, so every finite subset is satisfiable. Compactness gives a model of $Γ^{'}$ , which has at least $κ$ elements. Downward Löwenheim–Skolem applied to the language $L \cup {c_{α}}$ , of cardinality $κ$ , then cuts it down to one of cardinality exactly $κ$ .∎

Remark. Together the two theorems say that first-order logic is blind to cardinality above the size of the language: a theory with an infinite model has models of every sufficiently large cardinality, so no first-order theory with an infinite model is categorical. This is why "the reals are the unique complete ordered field" is not a first-order statement — completeness quantifies over subsets, and second-order quantification is exactly what first-order logic gives up in exchange for the completeness theorem.

Pitfall. Skolem's paradox is the usual stumbling block. First-order ZFC, if consistent, has a countable model by downward Löwenheim–Skolem, even though ZFC proves "there exists an uncountable set". There is no contradiction: uncountability of a set $A$ means there is no bijection between $A$ and $ω$ , and a countable model may simply contain no such bijection among its elements. Uncountability is relative to the model; what looks uncountable from inside can be countable from outside.

Exercises for §3.6 →

3.7Decidability, Semi-Decidability, and the Limits of the Method

Completeness says a derivation exists whenever the entailment holds. It does not say anyone can find it, and this last section is about the gap between the two. The distinction that measures the gap is between deciding a set and merely enumerating it.

Definition 3.37 (Decidable and semi-decidable). Let $A$ be a set of finite strings (formulas, say).

$A$ is decidable if some algorithm, on every input, halts and correctly reports whether the input is in $A$ .
$A$ is semi-decidable (recursively enumerable) if some algorithm halts with "yes" on exactly the inputs in $A$ , and on inputs outside $A$ either halts with "no" or runs forever.

The emphasis on "halts on every input" is the whole content of the definition. A procedure that recognises theorems by searching for a proof, and never terminates when there is none, is a perfectly good semi-decision procedure and not a decision procedure at all.

Theorem 3.38 (Post's theorem). $A$ is decidable if and only if both $A$ and its complement are semi-decidable.

Proof. ( $\Rightarrow$ ) A decision procedure for $A$ is in particular a semi-decision procedure for $A$ , and negating its output gives one for the complement.

( $\Leftarrow$ ) Let $P$ semi-decide $A$ and $Q$ semi-decide the complement. On input $x$ , run $P$ and $Q$ in parallel — alternate one step of each. Every $x$ lies in $A$ or in its complement, so exactly one of them eventually halts with "yes"; report accordingly. The procedure halts on every input, so it decides $A$ .∎

Theorem 3.39 (Theoremhood is semi-decidable). Let $S$ be an effective formal system in a countable language. Then ${ϕ : ⊢_{S} ϕ}$ is semi-decidable.

Proof. Because $S$ is effective, "is this finite sequence a derivation of $ϕ$ ? " is decidable: check each line against the axiom test and the rule tests. The finite sequences of formulas over a countable language can be enumerated, so the following halts exactly on theorems: enumerate the sequences, checking each, and halt with "yes" at the first derivation of $ϕ$ . On a non-theorem the search never ends.∎

Corollary 3.40 (Validity is semi-decidable). The set of valid first-order sentences is semi-decidable.

Proof. By completeness, $ϕ$ is valid iff $⊢ ϕ$ in an effective complete proof system for first-order logic, and Theorem Theoremhood is semi-decidable applies to that system.∎

This is exactly as far as the method reaches. The next theorem says that the other half of Post's criterion fails, so the search cannot be turned into a decision procedure — by any means whatever, not merely by proof search.

Theorem 3.41 (Church–Turing: undecidability of first-order validity). The set of valid sentences of first-order logic, in a language with at least one binary relation symbol, is undecidable: no algorithm halts on every input and correctly reports validity.

Proof. (Sketch; the full argument is Chapter 35 of Enderton or the standard development in any computability text.) The proof is a reduction from a known undecidable problem, the halting problem for Turing machines. Its three ingredients are:

Arithmetisation. A Turing machine computation can be encoded in first-order logic: for each machine $M$ and input $w$ one writes down a single sentence $σ_{M, w}$ , constructed effectively from $M$ and $w$ , whose conjuncts describe the tape alphabet, the transition table and the initial configuration.
The reduction. $σ_{M, w}$ is built so that $M$ halts on $w$ if and only if the sentence $σ_{M, w} \to η$ is valid, where $η$ asserts that a halting configuration is reached. Every model of $σ_{M, w}$ is forced to contain a copy of the computation, so validity of the implication tracks halting exactly.
Undecidability of halting, which is proved independently by diagonalisation.

Given a decision procedure for validity, feeding it $σ_{M, w} \to η$ would decide halting. No such procedure exists, so validity is undecidable. What the argument rests on is therefore: the Church–Turing thesis (that "algorithm" is captured by Turing machines), the effectiveness of the encoding in (1), and the undecidability of halting in (3).∎

Corollary 3.42 (Refutability is not semi-decidable). The set of non-valid first-order sentences is not semi-decidable.

Proof. If it were, then validity — semi-decidable by Corollary Validity is semi-decidable — and its complement would both be semi-decidable, so validity would be decidable by Post's theorem, contradicting Church–Turing.∎

Intuition. The asymmetry is the thing to carry away. A valid sentence always announces itself eventually: keep enumerating derivations and one turns up. An invalid sentence need not announce itself at all, because the countermodel that refutes it may be infinite, and no finite search is guaranteed to find it. Provability is a search with a finite certificate; refutability, in general, is not.

Decidability returns as soon as the quantifiers are tamed, and the contrast with the propositional case is instructive.

Theorem 3.43 (Propositional validity is decidable). There is an algorithm deciding whether a propositional formula is a tautology.

Proof. A formula $ϕ$ contains finitely many atoms, say $n$ of them, and its truth value under a valuation depends only on their values. Enumerate all $2^{n}$ valuations, evaluate $ϕ$ under each by recursion on its structure, and answer "valid" iff every valuation makes it true. The enumeration is finite, so the procedure halts on every input.∎

Example 3.44 (Running the decision procedure). Decide whether $ϕ = (p \to q) \to (\neg q \to \neg p)$ is a tautology, and count the work.

Solution. Two atoms, so $2^{2} = 4$ valuations.

$p$	$q$	$p \to q$	$\neg q \to \neg p$	$ϕ$
T	T	T	T	T
T	F	F	F	T
F	T	T	T	T
F	F	T	T	T

Row 2 is the instructive one: both inner implications are false, so the outer implication is true because its antecedent fails. All four rows give T, so the procedure halts and reports "valid" — the law of contraposition, as expected.

The work is $2^{n}$ rows and no more, which is what decidability requires: finite, guaranteed to terminate. It says nothing about efficiency, and indeed propositional satisfiability is NP-complete, so the practical tools (DPLL, CDCL) spend their effort avoiding the enumeration rather than improving on its bound. Slow but finite is still decidable; the first-order case is not slow, it is impossible. □□

Remark. Many fragments and theories sit on the decidable side, and each buys its decidability by giving something up.

Monadic first-order logic (only unary relation symbols, no function symbols) is decidable — with no way to relate two elements, a formula with $n$ predicates cannot distinguish more than $2^{n}$ kinds of element, which bounds the models to check.
Presburger arithmetic, the theory of $(N, +, <, 0, 1)$ , is decidable by quantifier elimination. Adding multiplication makes it undecidable, which is where Gödel's incompleteness theorems begin.
Real closed fields, the theory of $(R, +, \cdot, <, 0, 1)$ , is decidable by Tarski's quantifier-elimination algorithm — and is a theory with multiplication, which shows that multiplication alone is not the culprit; the ability to define the integers inside the structure is.

Pitfall. Undecidability does not mean "no proofs". Every valid sentence still has a finite derivation, and the search of Theorem Theoremhood is semi-decidable will find it. What fails is the ability to know in advance that the search will end. An automated theorem prover left running on a non-theorem is not malfunctioning; it is doing exactly what the theory predicts.

Exercises for §3.7 →

Common Mistakes

Writing $⊢$ where $⊨$ belongs. They are different relations with different definitions: $⊢$ is settled by a finite derivation in a fixed system, $⊨$ by every structure in the language. That they agree for first-order logic is the content of two theorems, not a matter of notation.
Using the deduction theorem without its side condition. In a first-order system with generalisation, $Γ \cup {ϕ} ⊢ ψ$ gives $Γ ⊢ ϕ \to ψ$ only when no generalisation in the derivation was applied to a variable free in $ϕ$ . Ignoring this "proves" $ϕ (x) \to \forall x ϕ (x)$ .
Confusing consistency with soundness. Consistency is internal — no contradiction is derivable. Soundness is a relation to a semantics — nothing false is derivable. A consistent theory can prove falsehoods about its intended structure.
Confusing the completeness of a logic with the negation-completeness of a theory. Gödel proved both a completeness and an incompleteness theorem, and they are compatible: the first says the logic derives every semantic consequence, the second that no effective consistent theory of arithmetic decides every sentence.
Applying compactness to a finite theory. A finite $Γ$ is a finite subset of itself, so the theorem is vacuous there. Its power is on infinite sets, where each finite fragment may have a different, smaller model.
Expecting a canonical model from the Henkin construction. It produces some model, built from the terms of an expanded language and depending on an arbitrary maximal consistent extension. Distinct extensions give non-isomorphic models, which is exactly why Löwenheim–Skolem can vary the cardinality at will.
Reading undecidability as a bound on proofs. Undecidable means no uniform halting decision procedure. Valid sentences retain their finite derivations; it is the non-valid ones that admit no finite certificate.

About the practice questions. They check that you can carry out this chapter's computations correctly, and each one is graded on a single answer. They are not proof exercises: working through them confirms the mechanics, not that you could prove the results yourself. For that, re-read the statements above and try to reconstruct their proofs with the page closed.

Practice this chapter