The Completeness Theorem

Derives Theorem A4.1. Induction on the length of the derivation, using Axiom 7.34 at the meta-level. Let \(M\) be any structure with \(M\vDash T\), and let \(\psi_{1},\ldots,\psi_{k}\) be a derivation of \(\varphi\) from \(T\). We show every \(\psi_{i}\) is true in \(M\).

If \(\psi_{i}\) is a member of \(T\), it is true in \(M\) by assumption. If it is a logical axiom, it is true in every structure whatever: the propositional axioms are tautologies in the sense of Definition 7.14, and their truth tables were computed once and for all in Section 7.1.2; the quantifier axiom \(\forall x\,\psi(x)\rightarrow\psi(t)\) holds because if \(\psi\) is satisfied by every element it is satisfied by the one denoted by \(t\); and the equality axioms hold because equality is interpreted as genuine identity on the domain.

If \(\psi_{i}\) follows by modus ponens from \(\psi_{j}\) and \(\psi_{j}\rightarrow\psi_{i}\) with \(j<i\), then both are true in \(M\) by the induction hypothesis, and row two of Equation (7.10) — the only row in which a conditional is false — is thereby excluded, so \(\psi_{i}\) is true. If \(\psi_{i}\) is \(\forall x\,\psi\) obtained by generalization from \(\psi\), where \(x\) does not occur free in \(T\), then \(\psi\) is true in \(M\) under every assignment to \(x\), which is what \(\forall x\,\psi\) asserts.

Every line is therefore true in \(M\), in particular the last, so \(M\vDash\varphi\). As \(M\) was an arbitrary model of \(T\), \(T\vDash\varphi\).

Derives Lemma A4.3. The language is countable, so its sentences can be listed \(\varphi_{0},\varphi_{1},\varphi_{2},\ldots\) — there are countably many finite strings over a countable alphabet, by Proposition 7.67. Given a consistent \(S\), define an increasing chain by \(S_{0}:=S\) and

Each \(S_{n}\) is consistent, by induction on \(n\). The base case is the hypothesis on \(S\). For the step, suppose \(S_{n}\) is consistent but both \(S_{n}\cup\set{\varphi_{n}}\) and \(S_{n}\cup\set{\neg\varphi_{n}}\) are not. Inconsistency of the first gives \(S_{n}\vdash\neg\varphi_{n}\) and of the second \(S_{n}\vdash\varphi_{n}\) — in each case by discharging the assumption, which is the deduction theorem — so \(S_{n}\) proves both a sentence and its negation, contradicting its consistency. Hence at least one of the two branches of Equation (A4.2) is consistent, and \(S_{n+1}\) is.

Let \(S^{*}:=\bigcup_{n\geq0}S_{n}\). It is consistent: a derivation of a contradiction is a finite object and mentions only finitely many members of \(S^{*}\), all of which lie in some single \(S_{n}\) — the chain is increasing — and that \(S_{n}\) was shown consistent. It is maximal: every sentence of the language is some \(\varphi_{n}\), and Equation (A4.2) placed either it or its negation in \(S_{n+1}\), so no consistent sentence can be added.

Derives Lemma A4.4. (1) Not both, by consistency. At least one: if neither is in \(S^{*}\), then by maximality \(S^{*}\cup\set{\varphi}\) is inconsistent, giving \(S^{*}\vdash\neg\varphi\), and likewise \(S^{*}\vdash\varphi\); that contradicts consistency.

(2) If \(S^{*}\vdash\varphi\) then \(S^{*}\cup\set{\varphi}\) is consistent — adding what is already derivable cannot produce a new contradiction — so maximality forces \(\varphi\in S^{*}\).

(3)–(5) Each follows from (1) and (2) together with the propositional tautologies of Proposition 7.22. For (5): if \(\varphi\notin S^{*}\) then \(\neg\varphi\in S^{*}\) by (1), and \(\neg\varphi\vdash \varphi\rightarrow\psi\), so \(\varphi\rightarrow\psi\in S^{*}\) by (2); if \(\psi\in S^{*}\) the same conclusion follows from \(\psi\vdash\varphi\rightarrow\psi\). Conversely if \(\varphi\rightarrow\psi\in S^{*}\) and \(\varphi\in S^{*}\), modus ponens and (2) give \(\psi\in S^{*}\). The other two are proved the same way.

Derives Lemma A4.5. A derivation is finite, so if the extended set were inconsistent, finitely many Henkin axioms would already suffice; it is enough to show that adding one at a time preserves consistency. So suppose \(S'\) is consistent, \(S'\) does not mention the constant \(c:=c_{\varphi}\), and \(S'\cup\set{H_{\varphi}}\) is inconsistent. Then

In particular \(S'\vdash\neg\varphi(c)\).

Now the crucial step. The constant \(c\) occurs nowhere in \(S'\), so it plays no role in the derivation beyond being a name; replacing every occurrence of \(c\) throughout the derivation by a variable \(y\) that appears nowhere in it yields again a correct derivation, and therefore \(S'\vdash\neg\varphi(y)\) with \(y\) free and unconstrained. Generalization is then legitimate — its side condition is exactly that the variable is not free in the premises — and gives

But \(S'\vdash\exists x\,\varphi(x)\) was established above, so \(S'\) is inconsistent, contrary to hypothesis. Hence \(S'\cup\set{H_{\varphi}}\) is consistent.

Derives Lemma A4.7. Reflexivity: \(t=t\) is a logical axiom, so it lies in \(T^{*}\) by Lemma A4.4(2). Symmetry and transitivity: the equality congruence schemas give \(\vdash(t=s)\rightarrow(s=t)\) and \(\vdash\left((t=s)\wedge(s=u)\right)\rightarrow(t=u)\), and deductive closure transfers these to membership in \(T^{*}\). So \(\sim\) satisfies the three clauses of Definition 7.58 and, by Theorem 7.60, partitions \(\mathrm{CT}\) into classes.

\(\mathrm{CT}\) is non-empty because \(L_{\infty}\) contains the Henkin constants, of which there is at least one; a structure must have a non-empty domain, and this is where that is secured.

Well-definedness: suppose \(t_{i}\sim s_{i}\) for each \(i\), i.e.\ \((t_{i}=s_{i})\in T^{*}\). The congruence schema for the function symbol \(f\) gives

so by Lemma A4.4(2),(3) the conclusion lies in \(T^{*}\) and \([f(\vect{t})]=[f(\vect{s})]\). The congruence schema for the relation symbol \(R\) gives the same conclusion for Equation (A4.8).

Derives Lemma A4.8. Induction on the number of connectives and quantifiers in \(\varphi\). The statement being proved is about all sentences of that complexity at once, which is what makes the quantifier case go through.

Atomic. A closed atomic sentence is \(R(t_{1},\ldots,t_{n})\) or \(t=s\). For the first, Equation (A4.8) says \(M\vDash R(t_{1},\ldots,t_{n})\) precisely when \(R(t_{1},\ldots,t_{n})\in T^{*}\). For the second, \(M\vDash t=s\) means \([t]=[s]\), which by Equation (A4.5) means \((t=s)\in T^{*}\). Note that the interpretation of a closed term \(t\) in \(M\) is \([t]\) itself, by induction on the term using Equations (A4.6) and (A4.7).

Negation. \(M\vDash\neg\varphi\) iff \(M\nvDash\varphi\), iff \(\varphi\notin T^{*}\) by the induction hypothesis, iff \(\neg\varphi\in T^{*}\) by Lemma A4.4(1).

Conditional. \(M\vDash\varphi\rightarrow\psi\) iff \(M\nvDash\varphi\) or \(M\vDash\psi\), which by the induction hypothesis is \(\varphi\notin T^{*}\) or \(\psi\in T^{*}\), which by Lemma A4.4(5) is \(\varphi\rightarrow\psi\in T^{*}\). The cases of \(\wedge\) and \(\vee\) are identical, using clauses (3) and (4).

Existential. Every element of the domain is \([t]\) for some closed term \(t\), so

Each \(\varphi(t)\) has fewer quantifiers than \(\exists x\,\varphi(x)\), so the induction hypothesis applies to it and the right-hand side is equivalent to \(\varphi(t)\in T^{*}\) for some closed \(t\).

If \(\exists x\,\varphi(x)\in T^{*}\), the Henkin axiom Equation (A4.3) for \(\varphi\) is in \(T^{*}\) by Equation (A4.4), and modus ponens with Lemma A4.4(2) puts \(\varphi(c_{\varphi})\in T^{*}\); that is the required witness. Conversely if \(\varphi(t)\in T^{*}\) for some closed \(t\), then since \(\vdash\varphi(t)\rightarrow\exists x\,\varphi(x)\) is a logical axiom, deductive closure gives \(\exists x\,\varphi(x)\in T^{*}\).

Universal. \(\forall x\,\varphi\) is treated as \(\neg\exists x\,\neg\varphi\), already covered.

Derives Theorem A4.9. Given consistent \(S\), build \(T^{*}\) as in Equation (A4.4) and let \(M\) be the term structure of Definition A4.6. By Lemma A4.8, \(M\) satisfies exactly the sentences of \(T^{*}\), and \(S\subset T^{*}\), so \(M\vDash S\). The model is a structure for \(L_{\infty}\); forgetting the interpretations of the added constants leaves a model of \(S\) in the original language.

Derives Theorem A4.10. Contrapositive. Suppose \(T\nvdash\varphi\). Then \(T\cup\set{\neg\varphi}\) is consistent — an inconsistency would give \(T\vdash\varphi\) by reductio — so by Theorem A4.9 it has a model \(M\). That \(M\) satisfies \(T\) and falsifies \(\varphi\), so \(T\nvDash\varphi\).

Derives Corollary A4.11. If \(T\) had no model it would, by Theorem A4.9, be inconsistent, so some derivation would produce a contradiction from it. A derivation is a finite object and cites only finitely many members of \(T\); those form a finite inconsistent subset, which by Theorem A4.1 has no model. This contradicts the hypothesis.