Chapter 48 Soundness
In this chapter we relate TFL’s semantics to its natural deduction proof system (as defined in part IV). We will prove that the formal proof system is safe: you can only prove sentences from premises from which they actually follow. Intuitively, a formal proof system is sound iff it does not allow you to prove any invalid arguments. This is obviously a highly desirable property. It tells us that our proof system will never lead us astray. Indeed, if our proof system were not sound, then we would not be able to trust our proofs. The aim of this chapter is to prove that our proof system is sound.
Let’s make the idea more precise. We’ll abbreviate a list of sentences using the greek letter $\mathrm{\Gamma}$ (‘gamma’). A formal proof system is sound (relative to a given semantics) iff, whenever there is a formal proof of $\mathcal{C}$ from assumptions among $\mathrm{\Gamma}$, then $\mathrm{\Gamma}$ genuinely entails $\mathcal{C}$ (given that semantics). Otherwise put, to prove that TFL’s proof system is sound, we need to prove the following
Soundness Theorem. For any sentences $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\Gamma}$}$ and $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{C}$}$: if $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\Gamma}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\u22a2$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{C}$}$, then $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\Gamma}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\models $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{C}$}$
To prove this, we will check each of the rules of TFL’s proof system individually. We want to show that no application of those rules ever leads us astray. Since a proof just involves repeated application of those rules, this will show that no proof ever leads us astray. Or at least, that is the general idea.
To begin with, we must make the idea of ‘leading us astray’ more precise. Say that a line of a proof is shiny iff the assumptions on which that line depends entail the sentence on that line.^{1}^{1} 1 The word ‘shiny’ is not standard among logicians. To illustrate the idea, consider the following:
Line number

Subproof level

Formula

Justification


$1$ 
0

$F\to (G\wedge H)$

PR

$2$ 
open subproof,
1

$F$

AS

$3$ 
1

$G\wedge H$

$\to $E $1$, $2$

$4$ 
1

$G$

$\wedge $E $3$

$5$ 
close subproof,
0

$F\to G$

$\to $I $2$–$4$

Line $1$ is shiny iff $F\to (G\wedge H)\models F\to (G\wedge H)$. You should be easily convinced that line $1$ is, indeed, shiny! Similarly, line $4$ is shiny iff $F\to (G\wedge H),F\models G$. Again, it is easy to check that line $4$ is shiny. As is every line in this TFLproof. We want to show that this is no coincidence. That is, we want to prove:
Shininess Lemma. Every line of every TFLproof is shiny.
Then we will know that we have never gone astray, on any line of a proof. Indeed, given the Shininess Lemma, it will be easy to prove the Soundness Theorem:
Proof. Suppose $\mathrm{\Gamma}\u22a2\mathcal{C}$. Then there is a TFLproof, with $\mathcal{C}$ appearing on its last line, whose only undischarged assumptions are among $\mathrm{\Gamma}$. The Shininess Lemma tells us that every line on every TFLproof is shiny. So this last line is shiny, i.e. $\mathrm{\Gamma}\models \mathcal{C}$. QED
It remains to prove the Shininess Lemma.
To do this, we observe that every line of any TFLproof is obtained by applying some rule. So what we want to show is that no application of a rule of TFL’s proof system will lead us astray. More precisely, say that a rule of inference is rulesound iff for all TFLproofs, if we obtain a line on a TFLproof by applying that rule, and every earlier line in the TFLproof is shiny, then our new line is also shiny. What we need to show is that every rule in TFL’s proof system is rulesound.
We will do this in the next section. But having demonstrated the rulesoundness of every rule, the Shininess Lemma will follow immediately:
Proof. Fix any line, line $n$, on any TFLproof. The sentence written on line $n$ must be obtained using a formal inference rule which is rulesound. This is to say that, if every earlier line is shiny, then line $n$ itself is shiny. Hence, by strong induction on the length of TFLproofs, every line of every TFLproof is shiny. QED
Note that this proof appeals to a principle of strong induction on the length of TFLproofs. This is the first time we have seen that principle, and you should pause to confirm that it is, indeed, justified.
It remains to show that every rule is rulesound. This is not difficult, but it is timeconsuming, since we need to check each rule individually, and TFL’s proof system has plenty of rules! To speed up the process marginally, we will introduce a convenient abbreviation: ‘${\mathrm{\Delta}}_{i}$’ (‘delta’) will abbreviate the assumptions (if any) on which line $i$ depends in our TFLproof (context will indicate which TFLproof we have in mind).
Introducing an assumption is rulesound.
If $\mathcal{A}$ is introduced as an assumption on line $n$, then $\mathcal{A}$ is among ${\mathrm{\Delta}}_{n}$, and so ${\mathrm{\Delta}}_{n}\models \mathcal{A}$.
$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\wedge $}$I is rulesound.
Proof. Consider any application of $\wedge $I in any TFLproof, i.e., something like:
Line number

Subproof level

Formula

Justification


$i$ 
0

$\mathcal{A}$


$j$ 
0

$\mathcal{B}$


$n$ 
0

$\mathcal{A}\wedge \mathcal{B}$

$\wedge $I $i$, $j$

To show that $\wedge $I is rulesound, we assume that every line before line $n$ is shiny; and we aim to show that line $n$ is shiny, i.e. that ${\mathrm{\Delta}}_{n}\models \mathcal{A}\wedge \mathcal{B}$.
So, let $v$ be any valuation that makes all of ${\mathrm{\Delta}}_{n}$ true.
We first show that $v$ makes $\mathcal{A}$ true. To prove this, note that all of ${\mathrm{\Delta}}_{i}$ are among ${\mathrm{\Delta}}_{n}$. By hypothesis, line $i$ is shiny. So any valuation that makes all of ${\mathrm{\Delta}}_{i}$ true makes $\mathcal{A}$ true. Since $v$ makes all of ${\mathrm{\Delta}}_{i}$ true, it makes $\mathcal{A}$ true too.
We can similarly see that $v$ makes $\mathcal{B}$ true.
So $v$ makes $\mathcal{A}$ true and $v$ makes $\mathcal{B}$ true. Consequently, $v$ makes $\mathcal{A}\wedge \mathcal{B}$ true. So any valuation that makes all of the sentences among ${\mathrm{\Delta}}_{n}$ true also makes $\mathcal{A}\wedge \mathcal{B}$ true. That is: line $n$ is shiny. QED
All of the remaining lemmas establishing rulesoundness will have, essentially, the same structure as this one did.
$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\wedge $}$E is rulesound.
Proof. Assume that every line before line $n$ on some TFLproof is shiny, and that $\wedge $E is used on line $n$. So the situation is:
Line number

Subproof level

Formula

Justification


$i$ 
0

$\mathcal{A}\wedge \mathcal{B}$


$n$ 
0

$\mathcal{A}$

$\wedge $E $i$

(or perhaps with $\mathcal{B}$ on line $n$ instead; but similar reasoning will apply in that case). Let $v$ be any valuation that makes all of ${\mathrm{\Delta}}_{n}$ true. Note that all of ${\mathrm{\Delta}}_{i}$ are among ${\mathrm{\Delta}}_{n}$. By hypothesis, line $i$ is shiny. So any valuation that makes all of ${\mathrm{\Delta}}_{i}$ true makes $\mathcal{A}\wedge \mathcal{B}$ true. So $v$ makes $\mathcal{A}\wedge \mathcal{B}$ true, and hence makes $\mathcal{A}$ true. So ${\mathrm{\Delta}}_{n}\models \mathcal{A}$. QED
$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\vee $}$I is rulesound.
We leave this as an exercise.
$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\vee $}$E is rulesound.
Proof. Assume that every line before line $n$ on some TFLproof is shiny, and that $\wedge $E is used on line $n$. So the situation is:
Line number

Subproof level

Formula

Justification


$m$ 
0

$\mathcal{A}\vee \mathcal{B}$


$i$ 
open subproof,
1

$\mathcal{A}$

AS

$j$ 
1

$\mathcal{C}$


$k$ 
close subproof,
open subproof,
1

$\mathcal{B}$

AS

$l$ 
1

$\mathcal{C}$


$n$ 
close subproof,
0

$\mathcal{C}$

$\vee $E $m$, $i$–$j$, $k$–$l$

Let $v$ be any valuation that makes all of ${\mathrm{\Delta}}_{n}$ true. Note that all of ${\mathrm{\Delta}}_{m}$ are among ${\mathrm{\Delta}}_{n}$. By hypothesis, line $m$ is shiny. So any valuation that makes ${\mathrm{\Delta}}_{n}$ true makes $\mathcal{A}\vee \mathcal{B}$ true. So in particular, $v$ makes $\mathcal{A}\vee \mathcal{B}$ true, and hence either $v$ makes $\mathcal{A}$ true, or $v$ makes $\mathcal{B}$ true. We now reason through these two cases:

1.
$v$ makes $\mathcal{A}$ true. All of ${\mathrm{\Delta}}_{i}$ are among ${\mathrm{\Delta}}_{n}$, with the possible exception of $\mathcal{A}$. Since $v$ makes all of ${\mathrm{\Delta}}_{n}$ true, and also makes $\mathcal{A}$ true, $v$ makes all of ${\mathrm{\Delta}}_{i}$ true. Now, by assumption, line $j$ is shiny; so ${\mathrm{\Delta}}_{j}\models \mathcal{C}$. But the sentences ${\mathrm{\Delta}}_{i}$ are just the sentences ${\mathrm{\Delta}}_{j}$, so ${\mathrm{\Delta}}_{i}\models \mathcal{C}$. So, any valuation that makes all of ${\mathrm{\Delta}}_{i}$ true makes $\mathcal{C}$ true. But $v$ is just such a valuation. So $v$ makes $\mathcal{C}$ true.

2.
$v$ makes $\mathcal{B}$ true. Reasoning in exactly the same way, considering lines $k$ and $l$, $v$ makes $\mathcal{C}$ true.
Either way, $v$ makes $\mathcal{C}$ true. So ${\mathrm{\Delta}}_{n}\models \mathcal{C}$. QED
$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\neg}$}$E is rulesound.
Proof. Assume that every line before line $n$ on some TFLproof is shiny, and that $\mathrm{\neg}$E is used on line $n$. So the situation is:
Line number

Subproof level

Formula

Justification


$i$ 
0

$\mathcal{A}$


$j$ 
0

$\mathrm{\neg}\mathcal{A}$


$n$ 
0

$\perp $

$\mathrm{\neg}$E $i$, $j$

Note that all of ${\mathrm{\Delta}}_{i}$ and all of ${\mathrm{\Delta}}_{j}$ are among ${\mathrm{\Delta}}_{n}$. By hypothesis, lines $i$ and $j$ are shiny. So any valuation which makes all of ${\mathrm{\Delta}}_{n}$ true would have to make both $\mathcal{A}$ and $\mathrm{\neg}\mathcal{A}$ true. But no valuation can do that. So no valuation makes all of ${\mathrm{\Delta}}_{n}$ true. So ${\mathrm{\Delta}}_{n}\models \perp $, vacuously. QED
X is rulesound.
We leave this as an exercise.
$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\neg}$}$I is rulesound.
Proof. Assume that every line before line $n$ on some TFLproof is shiny, and that $\mathrm{\neg}$I is used on line $n$. So the situation is:
Line number

Subproof level

Formula

Justification


$i$ 
open subproof,
1

$\mathcal{A}$

AS

$j$ 
1

$\perp $


$n$ 
close subproof,
0

$\mathrm{\neg}\mathcal{A}$

$\mathrm{\neg}$I $i$–$j$

Let $v$ be any valuation that makes all of ${\mathrm{\Delta}}_{n}$ true. Note that all of ${\mathrm{\Delta}}_{n}$ are among ${\mathrm{\Delta}}_{i}$, with the possible exception of $\mathcal{A}$ itself. By hypothesis, line $j$ is shiny. But no valuation can make ‘$\perp $’ true, so no valuation can make all of ${\mathrm{\Delta}}_{j}$ true. Since the sentences ${\mathrm{\Delta}}_{i}$ are just the sentences ${\mathrm{\Delta}}_{j}$, no valuation can make all of ${\mathrm{\Delta}}_{i}$ true. Since $v$ makes all of ${\mathrm{\Delta}}_{n}$ true, it must therefore make $\mathcal{A}$ false, and so make $\mathrm{\neg}\mathcal{A}$ true. So ${\mathrm{\Delta}}_{n}\models \mathrm{\neg}\mathcal{A}$. QED
IP, $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\to $}$I, $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\to $}$E, $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\leftrightarrow $}$I, and $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\leftrightarrow $}$E are all rulesound.
We leave these as exercises.
This establishes that all the basic rules of our proof system are rulesound. Finally, we show:
All of the derived rules of our proof system are rulesound.
Proof. Suppose that we used a derived rule to obtain some sentence, $\mathcal{A}$, on line $n$ of some TFLproof, and that every earlier line is shiny. Every use of a derived rule can be replaced (at the cost of longwindedness) with multiple uses of basic rules. That is to say, we could have used basic rules to write $\mathcal{A}$ on some line $n+k$, without introducing any further assumptions. So, applying our individual results that all basic rules are rulesound several times ($k+1$ times, in fact), we can see that line $n+k$ is shiny. Hence the derived rule is rulesound. QED
And that’s that! We have shown that every rule—basic or otherwise—is rulesound, which is all that we required to establish the Shininess Lemma, and hence the Soundness Theorem.
But it might help to round off this chapter if we repeat my informal explanation of what we have done. A formal proof is just a sequence—of arbitrary length—of applications of rules. We have shown that any application of any rule will not lead you astray. It follows (by induction)that no formal proof will lead you astray. That is: our proof system is sound.
Practice exercises
A. Complete the Lemmas left as exercises in this chapter. That is, show that the following are rulesound:

1.
$\vee $I. (Hint: this is similar to the case of $\wedge $E.)

2.
X. (Hint: this is similar to the case of $\mathrm{\neg}$E.)

3.
$\to $I. (Hint: this is similar to $\vee $E.)

4.
$\to $E.

5.
IP. (Hint: this is similar to the case of $\mathrm{\neg}$I.)