5  Completeness

We want the axiom system to derive a formula \(\varphi\) from a set of formulas \(\Gamma\) only when \(\varphi\) is a logical consequence of \(\Gamma\). That is what would make the axiom system sound. On the other hand, we want to be able to derive a formula \(\varphi\) from a set of formulas \(\Gamma\) whenever \(\varphi\) is a logical consequence of \(\Gamma\). That is what would make the axiom system complete. We now set out to justify that the axiom system we have described is both sound and complete.

Soundness

For every set of formulas \(\Gamma\) and every formula \(\varphi\), if \(\Gamma \vdash \varphi\), then \(\Gamma \models \varphi\).

One way to proceed is to use a complete induction (without a base case) on the length of proofs to argue that for every positive integer \(n\), if \(\langle \chi_1, ..., \chi_n\rangle\) is a derivation of \(\varphi\) from \(\Gamma\), then \(\Gamma \models \varphi\). The proof is left as an exercise to the reader.

5.1 Consistency

A set of formulas \(\Gamma\) is consistent if, and only if, \(\bot\) is not derivable from \(\Gamma\). That is, \(\Gamma\) is consistent if, and only if, \(\Gamma \nvdash \bot\).

We say that \(\Gamma\) is inconsistent if, and only if, \(\Gamma\) is not consistent. That is, \(\Gamma\) is inconsistent if, and only if, \(\Gamma \vdash \bot\).

Recall the definition of \(\bot\) in terms of \(\top\): \[ \bot := \neg \top. \]

Since \(\top\) is an abbreviation for the formula \(p \to p\), \(\bot\) is an abbreviation for \(\neg (p \to p)\).

Here is an important observation:

Proposition 5.1 Given a set of formulas \(\Gamma\) and a formula \(\varphi\), \[ \begin{array}{lll} \Gamma \vdash \varphi & \text{iff} & \Gamma, \neg \varphi \ \ \text{is inconsistent}.\\ \end{array} \]

Proof. We discuss one direction at a time.

(\(\Rightarrow\)) We first argue that if \(\Gamma \vdash \varphi\), then \(\Gamma, \neg \varphi \vdash \bot\).

To that purpose we note that a derivation of \(\varphi\) from \(\Gamma\) is automatically a derivation of \(\varphi\) from the larger set \(\Gamma, \neg \varphi\). We use this fact to produce a derivation of \(\bot\) from \(\Gamma, \neg \varphi\). \[ \begin{array}{llll} 1 & & \neg \varphi \to (\neg \bot \to \neg \varphi) & \textsf{A1}[\neg \varphi/p, \bot/q] \\ 2 & & \neg \varphi & \\ 3 & & \neg \bot \to \neg \varphi & \textsf{MP} \ 1, 2\\ 4 & & (\neg \bot \to \neg \varphi) \to (\varphi \to \bot) & \textsf{Prop} \ 3.2\\ 5 & & \varphi \to \bot & \textsf{MP} \ 3, 4\\ 6 & & \varphi & \Gamma \vdash \varphi\\ 7 & & \bot & \textsf{MP} \ 4, 5\\ \end{array} \]

(\(\Leftarrow\)) We now argue that if \(\Gamma, \neg \varphi \vdash \bot\), then \(\Gamma \vdash \varphi\).

We use the Deduction Theorem to move from \(\Gamma, \neg \varphi \vdash \bot\) to \(\Gamma \vdash \neg \varphi \to \bot\).

The plan now is to argue that \(\Gamma \vdash \neg \varphi \to \neg \bot\). For that observation, in combination with an instance of \(\textsf{A3}\) will deliver \(\Gamma \vdash \varphi\), which is what we want.

Since \(\Gamma, \neg \varphi \vdash \top\), and, by Prop 3.4, \(\Gamma, \neg \varphi \vdash \top \to \neg \neg \top\), \(\Gamma \neg \varphi \vdash \neg \neg \top\). But \(\neg \neg \top\) is just an abbreviation for \(\neg \bot\), which means \(\Gamma, \neg \varphi \vdash \neg \bot\). So, by the Deduction Theorem again, \(\Gamma \vdash \neg \varphi \to \neg \bot\).

We now outline a derivation of \(\varphi\) from \(\Gamma\): \[ \begin{array}{llll} 1 & & \neg \varphi \to \neg \bot & \Gamma \vdash \neg \varphi \to \neg \bot \\ 2 & & (\neg \varphi \to \neg \bot) \to ((\neg \varphi \to \bot) \to \varphi) & \textsf{A3}[\varphi/p, \bot/q]\\ 3 & & (\neg \varphi \to \bot) \to \varphi & \textsf{MP} \ 1, 2\\ 4 & & \neg \varphi \to \bot & \Gamma \vdash \neg \varphi \to \bot \\ 5 & & \varphi & \textsf{MP} \ 3, 4\\ \end{array} \]

\(\blacksquare\)

5.2 Maximal Consistency

A set of formulas \(\Gamma\) is maximal consistent if, and only if,

  1. \(\Gamma\) is consistent, and

  2. for every formula \(\varphi\), if \(\Gamma, \varphi\) is consistent, then \(\varphi \in \Gamma\).

Proposition 5.2 Given a maximal consistent set of formulas \(\Gamma\) and two formulas \(\varphi\) and \(\psi\),

  1. \(\Gamma \vdash \varphi\) if, and only if, \(\varphi \in \Gamma\).

  2. \(\neg \varphi \in \Gamma\) if, and only if, \(\varphi \notin \Gamma\).

  3. \(\varphi \to \psi \in \Gamma\) if, and only if \(\varphi \notin \Gamma\) or \(\psi \in \Gamma\).

Proof. Given a maximal consistent set of formulas \(\Gamma\) and two formulas \(\varphi\) and \(\psi\), we look at each claim in turn.

  1. \(\Gamma \vdash \varphi\) if, and only if, \(\varphi \in \Gamma\).

(\(\Rightarrow\)) We argue that if \(\Gamma \vdash \varphi\), then \(\varphi \in \Gamma\).

Suppose \(\Gamma \vdash \varphi\). We proceed by a reductio. Suppose \(\varphi \notin \Gamma\). By definition of maximal consistency, if \(\Gamma\) is maximal consistent and \(\varphi \notin \Gamma\), then \(\Gamma, \varphi\) is inconsistent. But now, since \(\Gamma \vdash \varphi\), by proposition 3.7, \(\Gamma, \neg \varphi\) must be inconsistent as well. It follows that \(\Gamma\) must itself be inconsistent, which contradicts its maximal consistency.1 We conclude that \(\varphi \in \Gamma\).

(\(\Leftarrow\)) We argue that if \(\varphi \in \Gamma\), then \(\Gamma \vdash \varphi\).

If \(\varphi \in \Gamma\), then there is a one-line derivation of \(\varphi\) from \(\Gamma\).

  1. \(\neg \varphi \in \Gamma\) if, and only if, \(\varphi \notin \Gamma\).

(\(\Rightarrow\)) We argue that if \(\neg \varphi \in \Gamma\), then \(\varphi \notin \Gamma\).

Suppose \(\neg \varphi \in \Gamma\). Then, by 1 above, \(\Gamma \vdash \neg \varphi\). Since \(\Gamma\) is consistent, \(\Gamma \nvdash \varphi\). This is because by proposition 3.6, \(\Gamma \vdash \neg \varphi \to (\varphi \to \bot)\). But by 1 above, from \(\Gamma \nvdash \varphi\), we infer that \(\varphi \notin \Gamma\).

(\(\Leftarrow\)) We show that if \(\varphi \notin \Gamma\), then \(\neg \varphi \in \Gamma\).

Suppose \(\varphi \notin \Gamma\). Since \(\Gamma\) is maximal consistent, \(\Gamma, \varphi\) is inconsistent. Given propositions 3.3 and 3.4, \(\Gamma, \varphi\) is inconsistent if, and only if, \(\Gamma, \neg \neg \varphi\) is inconsistent. So, since \(\Gamma, \neg \neg \varphi\) is inconsistent, we conclude, by proposition 3.7, that \(\Gamma \vdash \neg \varphi\). So, by 1 above, \(\neg \varphi \in \Gamma\).

  1. \(\varphi \to \psi \in \Gamma\) if, and only if \(\varphi \notin \Gamma\) or \(\psi \in \Gamma\).

(\(\Rightarrow\)) We argue that if \(\varphi \to \psi \in \Gamma\), then if \(\varphi \in \Gamma\), then \(\psi \in \Gamma\).

Suppose \(\varphi \to \psi \in \Gamma\). Then, given 1 above, \(\Gamma \vdash \varphi \to \psi\). Now: if \(\varphi \in \Gamma\), then \(\Gamma \vdash \varphi\) and \(\Gamma \vdash \psi\), whence \(\psi \in \Gamma\).

(\(\Leftarrow\)) We show that if \(\varphi \notin \Gamma\) or \(\psi \in \Gamma\), then \(\varphi \to \psi \in \Gamma\).

Suppose \(\varphi \notin \Gamma\) or \(\psi \in \Gamma\).

If \(\varphi \notin \Gamma\), then given 2 above, \(\neg \varphi \in \Gamma\). Since, by proposition 3.6, \(\vdash \neg \varphi \to (\varphi \to \psi)\) and \(\Gamma \vdash \neg \varphi\), we infer \(\Gamma \vdash \varphi \to \psi\). So, given 1, \(\varphi \to \psi \in \Gamma\).

If \(\psi \in \Gamma\), then since \(\vdash \psi \to (\varphi \to \psi)\), \(\Gamma \vdash \varphi \to \psi\). So, given 1 above, \(\varphi \to \psi \in \Gamma\).

\(\blacksquare\)

We now have the toolkit we need in order to prove the completeness of the system.

Completeness

For every set of formulas \(\Gamma\) and every formula \(\varphi\), if \(\Gamma \models \varphi\), then \(\Gamma \vdash \varphi\).

We follow an indirect route toward that conclusion.

Completeness Reformulated

For all \(\Gamma\) and \(\varphi\), if \(\Gamma \nvdash \varphi\), then \(\Gamma \not \models \varphi\).

For all \(\Gamma\) and \(\varphi\), if \(\Gamma, \neg \varphi\) is consistent, then \(\Gamma, \neg \varphi\) is satisfiable.

For all \(\Gamma\), if \(\Gamma\) is consistent, then \(\Gamma\) is satisfiable.

We set out to prove the last claim, which will suffice for our purposes. For given a set of formulas \(\Gamma\) and a formula \(\varphi\), if \(\Gamma \nvdash \varphi\), then by proposition 3.6, \(\Gamma, \neg \varphi\) is consistent. Given the link between consistency and satisfiability given by the last claim, we are able to infer that \(\Gamma, \neg \varphi\) is satisfiable, whence \(\Gamma \not \models \varphi\).

We reach our target, we will proceed to justify two double-arrows from the diagram below.

Plan

\[ \begin{array}{clllc} \Gamma \ \text{consistent} & & & & \Gamma \ \text{satisfiable}\\ \Downarrow & & & & \Uparrow \\ \exists \Sigma \ (\Gamma \subseteq \Sigma \wedge \Sigma \ \text{maxcon}) & & \Rightarrow & & \exists \Sigma \ (\Gamma \subseteq \Sigma \wedge \Sigma \ \text{satisfiable})\\ \end{array} \]

One step, which corresponds to the top-down double-arrow, is to extend a consistent set of formulas \(\Gamma\) to a maximal consistent set \(\Sigma\) (Lindenbaum Lemma.) The other step, which corresponds to the left-to-right double arrow, is argue that every maximal consistent set is satisfiable (Henkin Lemma).

Lemma 5.1 (Lindenbaum Lemma) If \(\Gamma\) is a consistent set of formulas, then \(\Gamma\) is a subset of a maximal consistent set of formulas \(\Sigma\).

Proof. We begin with an enumeration of the formulas of propositional logic: \[ \varphi_0, \varphi_1, \cdots, \varphi_n, \cdots \] Given \(\Gamma\) be a consistent set of formulas, we build a maximal consistent superset \(\Sigma\) by the following recursion: \[ \begin{array}{lll} \Sigma_0 & = & \Gamma \\ \Sigma_{n+1} & = & \begin{cases} \Sigma_n, \varphi_n & \text{if consistent}\\ \Sigma_n & \text{otherwise} \end{cases} \end{array} \] We let \[ \Sigma = \bigcup_{n\in \mathbb{N}} \Sigma_n. \]We now argue that \(\Sigma\) is a maximal consistent superset of \(\Gamma\).

We proceed in several steps.

Proposition 5.3 \(\Gamma \subseteq \Sigma\)

This is because \(\Gamma = \Sigma_0\) and \(\Sigma_0 \subseteq \Sigma\).

Proposition 5.4 For each natural number \(n\), \(\Gamma_n\) is consistent.

Proof. A simple induction on \(n\) suffices:

  • \(\Sigma_0\) is consistent on the assumption \(\Gamma\) is consistent.

  • If \(\Sigma_n\) is consistent, then \(\Sigma_{n+1}\) is \(\Sigma_n, \varphi_n\) if consistent, or else \(\Sigma_n\). Either way, \(\Sigma_{n+1}\) is consistent.

\(\blacksquare\)

Proposition 5.5 For each natural number \(n\), for every \(m < n\), \(\Sigma_m \subseteq \Sigma_n\).

Proof. We argue by induction on \(n\):

  • \(\Sigma_0\) is vacuously a superset of any set that may precede it in the sequence. This is because nothing precedes \(\Sigma_0\) in the sequence.

  • \(\Sigma_{n+1}\) is \(\Sigma_n, \varphi_n\) if consistent, or else \(\Sigma_n\). Either way, since by inductive hypothesis, for every \(m < n\) \(\Sigma_{m} \subseteq \Sigma_{n}\) and \(\Sigma_n \subseteq \Sigma_{n+1}\), we conclude that for every \(m < n\) \(\Sigma_{m} \subseteq \Sigma_{n+1}\).

\(\blacksquare\)

Proposition 5.6 For every finite subset \(\Delta \subseteq \Sigma\), there is some natural number \(n\) such that \(\Delta \subseteq \Sigma_n\).

Proof. If \(\Delta\) is a finite subset of \(\Sigma\), then let \(\varphi_n\) be the member of \(\Delta\) of highest index. That is for all \(m\), if \(\varphi_m \in \Delta\), then \(m \leq n\). Notice that for each natural number \(m\), if \(\varphi_m \in \Sigma\), then \(\varphi_m \in \Sigma_{m+1}\). That is, a formula \(\varphi_m\) is accepted into \(\Sigma\) via \(\Sigma_{m+1}\) if at all. So, it follows that \(\Delta \subseteq \Sigma_{n+1}\) if \(n\) is the highest index of a formula in \(\Delta\).

\(\blacksquare\)

It follows from the above that every finite subset of \(\Sigma\) is consistent. We now argue that \(\Sigma\) is consistent as well.

Proposition 5.7 \(\Sigma\) is consistent.

Proof. For purposes of a reductio, suppose \(\Sigma \vdash \bot\). That means that there is a finite derivation \((\chi_1, \dots, \chi_n)\) of \(\bot\) from \(\Sigma\). It follows that there is a derivation of \(\bot\) from a finite subset of \(\Sigma\), which would require that finite subset of \(\Sigma\) to be inconsistent. That contradicts the observation that every finite subset of \(\Sigma\) is consistent.

\(\blacksquare\)

Proposition 5.8 Given a formula \(\varphi\), if \(\Sigma, \varphi\) is consistent, then \(\varphi \in \Sigma\).

Proof. A formula \(\varphi\) will be assigned an index by the enumeration, which means \(\varphi = \varphi_n\). Now, if \(\Sigma, \varphi_n\) is consistent, then \(\Sigma_n, \varphi_n\) will be consistent as well. But that means that by construction of \(\Sigma\), \(\varphi_n \in \Sigma_{n+1} \subseteq \Sigma\).

\(\blacksquare\)

We conclude that \(\Sigma\) is a maximal consistent superset of \(\Gamma\).

\(\blacksquare\)

It remains to show that a maximal consistent set of formulas is satisfiable.

Lemma 5.2 (Henkin Lemma) Every maximal consistent set \(\Sigma\) is satisfiable.

Proof. Given a maximal consistent set \(\Sigma\), let \(V\) based on an assignment \(v\) defined: \[ \begin{array}{lll} v(p_n) = 1 & \text{iff} & p_n \in \Sigma. \end{array} \]

We use an induction on the complexity of \(\varphi\) to establish:
\[ \begin{array}{lll} V(\varphi) = 1 & \text{iff} & \varphi \in \Sigma. \end{array} \]
- Base Case:

\[ \begin{array}{llll} V(p_n) = 1 & \text{iff} & v(p_n) = 1 & \\ & \text{iff} & p_n \in \Sigma. & \textsf{Def} \ v \end{array} \]
- Inductive Step for \(\neg\):

\[ \begin{array}{llll} V(\neg \varphi) = 1 & \text{iff} & V(\varphi) = 0 & \\ & \text{iff} & \varphi \notin \Sigma & \textsf{IH} \\ & \text{iff} & \neg \varphi \in \Sigma & \textsf{Prop} \ 3.8, 2 \\ \end{array} \]
- Inductive Step for \(\to\):

\[ \begin{array}{llll} V(\varphi \to \psi) = 1 & \text{iff} & V(\varphi) = 0 \ \text{or} \ V(\psi) =1 & \\ & \text{iff} & \varphi \notin \Sigma \ \text{or} \ \psi \in \Sigma& \textsf{IH} \\ & \text{iff} & \varphi \to \psi \in \Sigma & \textsf{Prop} \ 3.8, 3 \\ \end{array} \]
We conclude that \(V\) verifies exactly those formulas in \(\Sigma\). So, it follows that \(\Sigma\) is satisfiable.

\(\blacksquare\)

This concludes the proof of completeness. From now on, we are entitled to assume that the axiom system proves every tautology and that if proves \(\varphi\) from \(\Gamma\) whenever \(\varphi\) is a logical consequence of \(\Gamma\). These are facts we will use when we introduce suitable axiom systems for different modal logics.

  1. This is problem 3 in assignment 2.↩︎