7. Soundness for Propositional Logic

In the last few lectures, we have seen two completely different ways to analyze logical arguments. Whenever \(\Gamma\) is a set of formulas that represent the premises of the argument and \(\phi\) is a formula that represents the conclusion of the argument,

• \(\Gamma \vDash \phi\) means that \(\phi\) is a logical consequence of \(\Gamma\): whenever a truth assignment satisfies every formula in \(\Gamma\), it necessarily also satisfies the conclusion \(\phi\).

• \(\Gamma \vdash \phi\) means that \(\phi\) is implied by \(\Gamma\): there exists a formal proof with premises in \(\Gamma\) and last line \(\phi\).

For some formal deduction systems, the two assertions are not equivalent to each other. But we hope that this is not the case with the formal deduction system that we have been studying! Our goal in studying formal proofs is to obtain an alternative to the truth table method for establishing the validity of logical argument. In order to show that our system does achieve this goal, we need to establish two fundamental properties:

• Soundness: If \(\Gamma \vdash \phi\), then \(\Gamma \vDash \phi\).

• Completeness: If \(\Gamma \vDash \phi\), then \(\Gamma \vdash \phi\).

The soundness of a proof system guarantees that whenever we obtain a proof of \(\phi\) from \(\Gamma\), then we know that \(\phi\) truly is a logical consequence of \(\Gamma\) or, in other words, that the logical argument we are examining is valid.

The completeness property, meanwhile, guarantees that every valid argument has a formal proof demonstrating that fact.

We will prove that our formal deduction system satisfies both of these properties.

The Soundness Theorem

The soundness property might be the most important of the two. After all, what good is a formal proof if it sometimes leads to a conclusion that is not guaranteed to be a logical consequence of the premises? So we begin with the proof that our formal deduction system does satisfy this property.

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

The proof of the Soundness Theorem for Propositional Logic is conceptually simple. We proceed by induction on the number \(n\) of lines in the proof. The main part of the proof will then be to simply show that the formula \(\phi_n\) in the last line of the proof is implied by the set \(\Gamma\) of premises whenever that last line of the proof is justified by one of the Basic Rules of our proof system.

There are two minor complications to this high-level idea for the proof:

• We need to establish some basic properties of logical consequence to make the high-level idea described above more precise.
• We need to be careful in how we choose our induction hypothesis so that the argument properly handles subproofs; and

We address these complications in order.

Basic Properties of Logical Consequence

Let us start with two elementary facts about logical consequence.

Proposition 1. For any set \(\Gamma\) of formulas and any formula \(\phi\) where \(\Gamma \vDash \phi\), every set \(\Gamma' \supseteq \Gamma\) also satisfies \(\Gamma' \vDash \phi\).

Proof. Fix any \(\Gamma\) and \(\phi\) where \(\Gamma \vDash \phi\). By definition, all the truth assignments that satisfy every formula in \(\Gamma\) also satisfy \(\phi\). And for any \(\Gamma' \supseteq \Gamma\), every truth assignment that satisfies all the formulas in \(\Gamma'\) also satisfies all the formulas in \(\Gamma\). Therefore, every truth assignment that satisfies all the formulas in \(\Gamma'\) satisfies \(\phi\).

Proposition 2. Let \(\Gamma\) be any set of formulas and \(\phi_1,\ldots,\phi_k\) by any \(k\) formulas where \(\Gamma \vDash \phi_1, \ldots, \Gamma \vDash \phi_k\). If \(\psi\) is a formula for which \(\{\phi_1,\ldots,\phi_k\} \vDash \psi\), then \(\Gamma \vDash \psi\).

Proof. By the logical consequences \(\Gamma \vDash \phi_1, \ldots, \Gamma \vDash \phi_k\), every truth assignment that satisfies every formula in \(\Gamma\) also satisfies all of \(\phi_1,\ldots,\phi_k\). And by the logical consequence \(\{\phi_1,\ldots,\phi_k\} \vDash \psi\), all of these truth assignments also satisfy \(\psi\).

We can now establish specific properties of logical consequence related to the basic rules of our proof system.

Proposition 3. Fix any formulas \(\phi\), \(\psi\), and \(\theta\). Fix any set \(\Gamma\) of formulas. Let \(\bot\) represent any contradiction. Then:

• (⋀I)   \(\{\phi, \psi\} \vDash (\phi \wedge \psi)\)
• (⋀E)   \(\{(\phi \wedge \psi)\} \vDash \phi\) and \(\{(\phi \wedge \psi)\} \vDash \psi\)
• (⋁I)   \(\{\phi\} \vDash (\phi \vee \psi)\) and \(\{\psi\} \vDash (\phi \vee \psi)\)
• (⋁E)   If \(\Gamma \cup \{\phi\} \vDash \theta\) and \(\Gamma \cup \{\psi\} \vDash \theta\) then \(\Gamma \cup \{(\phi \vee \psi)\} \vDash \theta\).
• (→I)   If \(\Gamma \cup \{\phi\} \vDash \psi\) then \(\Gamma \vDash (\phi \to \psi)\)
• (→E)   \(\{ (\phi \to \psi), \phi\} \vDash \psi\)
• (↔︎I)   \(\{ (\phi \to \psi), (\psi \to \phi)\} \vDash (\phi \leftrightarrow \psi)\)
• (↔︎E)   \(\{ (\phi \leftrightarrow \psi) \} \vDash (\phi \to \psi)\) and \(\{ (\phi \leftrightarrow \psi) \} \vDash (\psi \to \phi)\)
• (¬I)   If \(\Gamma \cup \{\phi\} \vDash \bot\) then \(\Gamma \vDash \neg \phi\)
• (¬E)   \(\{\phi, \neg \phi\} \vDash \bot\)
• (⊥E)   \(\{\bot\} \vDash \phi\)
• (RAA)   If \(\Gamma \cup \{\neg \phi\} \vDash \bot\) then \(\Gamma \vDash \phi\)

Proof. We verify the (⋀I) claim that \(\{\phi, \psi\} \vDash (\phi \wedge \psi)\) directly using a truth table:

\[\begin{array}{cc|c} \phi & \psi & (\phi \wedge \psi) \\ \hline T & T & T \\ T & F & F \\ F & T & F \\ F & F & F \end{array}\]

Similarly, we establish the (⋀E), (⋁I), (→E), (↔︎I), (↔︎E), (¬E), and (⊥E) claims directly using truth tables.

For the (→I) claim, consider any set \(\Gamma\) and formulas \(\phi\) and \(\psi\) for which \(\Gamma \cup \{\phi\} \vDash \psi.\) Consider any truth assignment that satisfies every formula in \(\Gamma\). If this truth assignment also satisfies \(\phi\), then it also satisfies \(\psi\). In other words, \(\Gamma \vDash (\phi \to \psi).\)

Similarly, we establish the final claims (⋁E), (¬I), and (RAA) in the same way by considering the truth assignments that satisfy all the formulas in \(\Gamma.\)

Undischarged Assumptions

To prove the Soundness Theorem by induction on the number of lines in a proof of \(\Gamma \vdash \phi\), we need to define an induction hypothesis that also handles the case where the last line of the proof is part of a subproof. For such proofs, we cannot say that the premise of the proof implies its last line because lines in a subproof also (potentially) rely on the additional assumption introduced in the first line of the subproof. To handle this complication, we introduce one more notion.

Definition. In a proof with formulas \(\phi_1,\ldots,\phi_n\), the undischarged assumptions at line \(k\) of the proof, which we will denote by \(A_k\), is the set of assumptions of each of the subproofs that are currently open at line \(k\).

Note that when \(\phi_1,\ldots,\phi_n\) are the formulas at each line of a formal proof showing that \(\Gamma \vdash \phi_n\), then by definition \(A_n = \emptyset\) because the last line of the proof is not in a subproof.

The Proof

With the basic facts in place and the notion of undischarged assumption, we can now complete the proof of the Soundness Theorem.

Theorem. (Soundness Theorem, restated) For every set of formulas \(\Gamma\) and every formula \(\phi\), if \(\Gamma \vdash \phi\) then \(\Gamma \vDash \phi.\)

Proof. Fix any \(\Gamma\) and \(\phi\) for which \(\Gamma \vdash \phi\) and let \(\phi_1,\ldots,\phi_n\) denote the formulas on each line of a formal proof of this implication. We prove by induction on the line number that each \(k\) in the range \(1 \le k \le n\) satisfies

\[\Gamma \cup A_k \vDash \phi_k.\]

Doing so completes the proof of the theorem since we must have \(\phi_n = \phi\) and \(A_n = \emptyset\) in the final line of the proof.

In the base case, when \(k=1\), there are two possibilities for the justification of the line:

• PR: If the line is justified with the premise rule, then \(\phi_1 \in \Gamma\) and so \(\Gamma \vDash \phi_1\).

• AS: If the line is obtained from the Assumption rule that starts a subproof, then \(A_1 = \{\phi_1\}\) and so \(\Gamma \cup A_1 \vDash \phi_1\).

For the induction step, fix \(k > 1.\) By the induction hypothesis, we can assume that for every \(i < k\), we have \(\Gamma \cup A_i \vDash \phi_i.\) Consider the different justifications of the \(k\)th line of the proof:

• PR or AS: If \(\phi_k\) is obtained via the premise or assumption rules, the same argument as in the base case holds here and guarantees that \(\Gamma \cup A_k \vDash \{\phi_k\}.\)

• R: In this case, \(\phi_k = \phi_i\) for some \(i < k\).

  By the induction hypothesis, \(\Gamma \cup A_i \vDash \phi_i = \phi_k\).

  And line \(i\) can be referenced at line \(k\) only if every subproof at line \(i\) has not yet been closed. So \(A_k \supseteq A_i\). By Proposition 1, this means that \(\Gamma \cup A_k \vDash \phi_k\).

• ⋀I: In this case, \(\phi_k = (\phi_i \wedge \phi_j)\) for some \(i, j < k.\)

  By the induction hypothesis, \(\Gamma \cup A_i \vDash \phi_i\) and \(\Gamma \cup A_j \vDash \phi_j.\)

  The subproofs at lines \(i\) and \(j\) cannot be yet be closed on line \(k\) for the reference to be valid, so \(A_k \supseteq A_i\) and \(A_k \supseteq A_j\). By Proposition 1, this means that \(\Gamma \cup A_k \vDash \phi_i\) and \(\Gamma \cup A_k \vDash \phi_j.\)

  By case ⋀I of Proposition 3, \(\{ \phi_i, \phi_j \} \vDash \phi_k.\)

  And so by Proposition 2, \(\Gamma \cup A_k \vDash \phi_k.\)

• ⋀E, ⋁I, →E, ↔︎I, ↔︎E, ¬E, or ⊥E: In these cases, the argument is exactly the same as for ⋀I except that we use the appropriate case of Proposition 3.

• →I: In this case, \(\phi_k = (\phi_i \to \phi_j)\) for some \(i, j < k.\)

  By the assumption hypothesis, \(\Gamma \cup A_j \vDash \phi_j.\) And the subproof \(i\)-\(j\) must not be part of any other subproof that ended before line \(k\), so we must have \(A_k \supseteq A_j \setminus \{\phi_i\}.\) By Proposition 1, \((\Gamma \cup A_k) \cup \{\phi_i\} \vDash \phi_j.\)

  By the →I case of Proposition 3, \(\Gamma \cup A_k \vDash \phi_j.\)

• ⋁E, ¬I, and RAA: These cases are essentially identical to →I, once again with the main difference being the use of the appropriate case of Proposition 3.