8. Completeness for Propositional Logic

Recall that a formal proof system is complete if for every set \(\Gamma\) of formulas and every formula \(\phi\) for which \(\Gamma \vDash \phi,\) we can find a formal proof showing that \(\Gamma \vdash \phi\) as well.

Completeness is trickier to prove than soundness. In large part, that’s because it appears to be difficult to prove the theorem with a direct attack. To complete such a “direct” proof, we would need to generate a proof showing that \(\Gamma \vdash \phi\) only knowing that \(\phi\) is a logical consequence of \(\Gamma\). But how would we even begin to write such a proof?

In the proof that we will see below, we avoid the problem entirely by considering an alternative approach to proving the soundness property. For this approach, we begin by examining a notion of consistent sets of formulas.

Consistent and Maximally Consistent Sets of Formulas

We say that a set of formulas is consistent when we cannot derive a proof of a contradiction whose premises are all in the set. It is inconsistent when it is not consistent. And it is maximally consistent when it is consistent and has no strict superset that is also consistent. More formally:

Definition. The set \(\Gamma\) of formulas is:

Maximally consistent sets of formulas are particularly nice to work with because they satisfy some strong structural properties.

Proposition 1. For every maximally consistent set \(\Gamma\), the following statements about a formula \(\phi \in L^p(\sigma)\) are equivalent:

  1. \(\phi \in \Gamma\).
  2. \(\neg \phi \notin \Gamma\).
  3. \(\Gamma \vdash \phi\).
  4. \(\Gamma \cup \{\phi\} \not\vdash \bot\).

Proof. (\(1 \Rightarrow 2\)) When \(\phi \in \Gamma\), then we can’t have \(\neg \phi\) in \(\Gamma\) otherwise we can use the ¬E rule with \(\{\phi, \neg \phi\}\) to obtain \(\bot\), contradicting the consistency of \(\Gamma\).

(\(2 \Rightarrow 3\)) By the definition of maximal consistency, \(\neg \phi \notin \Gamma\) only when \(\Gamma \cup \{\neg \phi\} \vdash \bot\), which means that we can derive \(\Gamma \vdash \phi\) using the RAA rule.

(\(3 \Rightarrow 4\)) When \(\Gamma \vdash \phi\), every formal proof whose premises are in \(\Gamma \cup \{\phi\}\) can be turned into a proof with the same conclusion and premises in \(\Gamma\) by replacing any line that uses the PR rule to invoke \(\phi\) with the formal derivation of \(\phi\) from \(\Gamma\). Therefore, since \(\Gamma\) is consistent then \(\Gamma \not\vdash \bot\) and we have \(\Gamma \cup \{\phi\} \not\vdash \bot\) as well.

(\(4 \Rightarrow 1\)) Since \(\Gamma\) is maximally consistent, if \(\Gamma \cup \{\phi\}\) is consistent then we must have \(\phi \in \Gamma\).

We use this structure to prove the first result.

Maximally Consistent Sets are Satisfiable

Lemma 2. Every maximally consistent set \(\Gamma\) of formulas is satisfiable.

Proof. Consider the truth assignment \(v \colon P \to \{T, F\}\) on the set $P$ of all propositional variables in \(\sigma\) defined by

\[v(\pi) = \begin{cases} T & \mbox{if } \pi \in \Gamma \\ F & \mbox{if } \pi \notin \Gamma \end{cases}\]

for every propositional variable \(\pi \in P\). We prove that the corresponding truth value function \(v^* \colon L^p(\sigma) \to \{T, F\}\) satisfies

\[v^*(\phi) = \begin{cases} T & \mbox{if } \phi \in \Gamma \\ F & \mbox{if } \phi \notin \Gamma \end{cases}\]

for every formula \(\phi \in L^p(\sigma)\). This will complete the proof of the lemma since it implies that \(v\) satisfies every formula in \(\Gamma\). We proceed by induction on the length \(n\) of the string \(\phi\).

In the base case, when \(n=1\) then \(\phi\) consists of a single propositional variable symbol and the claim is directly satisfied by the definition of \(v\).

For the induction step, when \(n > 1\) then \(\phi\) has one of the following forms:

In all of these cases, the condition that \(v^*(\phi) = T\) if and only if \(\phi \in \Gamma\) is satisfied.

Consistent Sets are Satisfiable

Our goal in this section is to extend Lemma 2 to show that all consistent sets are satisfiable. To do this, we need two more basic facts of consistent and satisfiable sets of formulas.

Proposition 3. For any set \(\Gamma\) of formulas and any superset \(\Gamma' \supseteq \Gamma\),

Proof. For the first claim, it is easier to prove the contrapositive statement. If \(\Gamma\) is not consistent, then \(\Gamma \vdash \bot\). And as we saw in the last lecture, when \(\Gamma' \supseteq \Gamma\), this means that \(\Gamma' \vdash \bot\) as well and so \(\Gamma'\) is also inconsistent.

For the second claim, consider any truth assignment that satisfies all the formulas ini \(\Gamma'\). Then the same truth assignment necessarily satisfies all the formulas in \(\Gamma \subseteq \Gamma'\) as well.

We are now ready to complete our strengthening of Lemma 2.

Lemma 4. Every consistent set \(\Gamma\) of formulas is satisfiable.

Proof. By Lemma 2 and Proposition 3, all we need to show is that the consistent set \(\Gamma\) of formulas has a superset \(\Gamma'\) that is maximally consistent. We construct the set \(\Gamma'\) in the following way:

Fix any ordering \(\phi_1,\phi_2,\phi_3,\ldots\) of the formulas in \(L^p(\sigma)\). Initialize \(\Gamma_0 = \Gamma\). Then for each \(k=1,2,3,\ldots\), define

\[\Gamma_k = \begin{cases} \Gamma_{k-1} \cup \{\phi_k\} & \mbox{if this set is consistent} \\ \Gamma_{k-1} & \mbox{otherwise.} \end{cases}\]

Define \(\Gamma' = \bigcup_{k \ge 0} \Gamma_k\). By this construction, for any \(k \ge 0\), we have

\[\Gamma' \supseteq \Gamma_k \supseteq \Gamma_{k-1} \supseteq \cdots \supseteq \Gamma_0 = \Gamma\]

so \(\Gamma'\) is a superset of \(\Gamma\). It remains to show that \(\Gamma'\) is maximally consistent.

As a first step, note that \(\Gamma_0 = \Gamma\) is consistent. And for every \(k \ge 1\), our construction guarantees that if \(\Gamma_{k-1}\) is consistent, then so is \(\Gamma_k\). So \(\Gamma_k\) is consistent for all \(k \in \mathbb{N}\). Now assume for the sake of contradiction that \(\Gamma'\) is inconsistent, so that \(\Gamma' \vdash \bot\). Fix any formal proof of this implication. Since formal proofs have finite length, there is an index \(n \in \mathbb{N}\) for which all the premises used in the proof are in \(\phi_1,\ldots,\phi_n\). By our construction, this means that the same proof also shows that \(\Gamma_n \vdash \bot\). But this contradicts the fact that we just established that every \(\Gamma_n\) is consistent, so we indeed must have that \(\Gamma'\) is also consistent, as we wanted to show.

Finally, to show that \(\Gamma'\) is maximally consistent, we must show that for every \(\phi_k \notin \Gamma'\), we have \(\Gamma' \cup \{\phi_k\} \vdash \bot\). And, indeed, \(\phi_k \notin \Gamma'\) if and only if \(\phi_k \notin \Gamma_k\), which happens only when \(\Gamma_k \cup \{\phi_k\}\) is not consistent. In this case, as Proposition 3 shows, we also have that \(\Gamma' \cup \{\phi_k\} \vdash \bot\).

The Completeness Theorem

If we take the contrapositive of Lemma 4 above, we see that we have established a special case of the Completeness Theorem: we showed that if \(\Gamma \vDash \bot\), then \(\Gamma \vdash \bot.\) To complete the proof of the full Completeness Theorem, we show that this special case implies the general case as well.

Theorem. (Completeness for Propositional Logic) For every set \(\Gamma\) of formulas and every formula \(\phi\), if \(\Gamma \vDash \phi\) then \(\Gamma \vdash \phi\).

Proof. Fix any \(\Gamma\) and \(\phi\) for which \(\Gamma \vDash \phi.\) Then every truth assignment which satisfies every formula in \(\Gamma\) also satisfies \(\phi\). Or, equivalently, there is no truth assignment that satisfies every formula in \(\Gamma \cup \{\neg \phi\}.\) Thus, \(\Gamma \cup \{\neg \phi\} \vDash \bot.\)

By the contrapositive form of Lemma 4, this means that \(\Gamma \cup \{\neg \phi\} \vdash \bot.\) In turn, this means that we can use the RAA rule (along with a subproof with assumption \(\neg \phi\) and conclusion \(\bot\)) to obtain the implication \(\Gamma \vdash \phi\), as we wanted to show.