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 if⁠f 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) if⁠f, whenever there is a formal proof of $𝒞$ from assumptions among $\mathrm{\Gamma }$, then $\mathrm{\Gamma }$ genuinely entails $𝒞$ (given that semantics). Otherwise put, to prove that TFL’s proof system is sound, we need to prove the following

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 if⁠f the assumptions on which that line depends entail the sentence on that line.¹¹ 1 The word ‘shiny’ is not standard among logicians. To illustrate the idea, consider the following:

Proof. Suppose $\mathrm{\Gamma }⊢𝒞$. Then there is a TFL-proof, with $𝒞$ appearing on its last line, whose only undischarged assumptions are among $\mathrm{\Gamma }$. The Shininess Lemma tells us that every line on every TFL-proof is shiny. So this last line is shiny, i.e., $\mathrm{\Gamma }\models 𝒞$. QED

It remains to prove the Shininess Lemma.

To do this, we observe that every line of any TFL-proof is either a premise or an assumption, or it is obtained by applying some rule. Premises are automatically shiny: if $𝒜$ is a premise, then it is among the sentences in $\mathrm{\Gamma }$, and $\mathrm{\Gamma }\models 𝒜$ trivially. Assumptions are also shiny, since the any assumption $𝒜$ depends on itself, and $𝒜\models 𝒜$. 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 rule-sound if⁠f for all TFL-proofs, if we obtain a line on a TFL-proof by applying that rule, and every earlier line in the TFL-proof is shiny, then our new line is also shiny. What we need to show is that every rule in TFL’s proof system is rule-sound.

We will do this below. But having demonstrated the rule-soundness of every rule, the Shininess Lemma will follow immediately:

Proof. Start with line $1$ of any TFL proof. It must be either a premise or an assumption, and those are all shiny, as we’ve seen above. Take the next line, $2$. If it is a premise or assumption, it is shiny. If not, it is obtained from line $1$ using an inference which is rule-sound. Since line $1$ is shiny, line $2$ is also shiny. Take the next line, $3$. If it is a premise or assumption, it is shiny. If not, it is obtained from a previous line using an inference which is rule-sound, and we’ve established that all previous lines are shiny. Thus, line $3$ is also shiny. And so on. In general, the sentence written on line $n$ must either be a premise or assumption (which is shiny) or be obtained using a formal inference rule which is rule-sound. Since every earlier line is shiny, line $n$ itself is shiny. We can simply go through this reasoning, for any TFL proof, starting with line $1$ and continuing to the last line, and get that every line of every TFL-proof is shiny. QED

It remains to show that every rule is rule-sound. This is not difficult, but it is time-consuming, 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 TFL-proof (context will indicate which TFL-proof we have in mind). This includes all premises of our proof, and all assumptions of subproofs which are still open at line $i$. Let’s first record our observation about premises and assumptions from above.

If $𝒜$ is a premise on line $n$, then it is among ${\mathrm{\Delta }}_n$ as that includes all premises of the proof. If it is introduced as an assumption of a subproof on line $n$, then everything in the subproof (including line $n$, i.e., $𝒜$ itself) depends on $𝒜$, and so $𝒜$ is among ${\mathrm{\Delta }}_n$. In either case, ${\mathrm{\Delta }}_n\models 𝒜$.

Now let’s proceed to show that all the inference rules are rule-sound.

Proof. Consider any application of $\wedge$I in any TFL-proof, i.e., something like:

So, let $v$ be any valuation that makes all of ${\mathrm{\Delta }}_n$ true.

We first show that $v$ makes $𝒜$ 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 $𝒜$ true. Since $v$ makes all of ${\mathrm{\Delta }}_i$ true, it makes $𝒜$ true too.

We can similarly see that $v$ makes $ℬ$ true.

So $v$ makes $𝒜$ true and $v$ makes $ℬ$ true. Consequently, $v$ makes $𝒜\wedge ℬ$ true. So any valuation that makes all sentences among ${\mathrm{\Delta }}_n$ true also makes $𝒜\wedge ℬ$ true. That is: line $n$ is shiny. QED

All of the remaining lemmas establishing rule-soundness will have, essentially, the same structure as this one did.

Proof. Assume that every line before line $n$ on some TFL-proof is shiny, and that $\wedge$E is used on line $n$. So the situation is:

We leave this as an exercise.

Proof. Assume that every line before line $n$ on some TFL-proof is shiny, and that $\wedge$E is used on line $n$. So the situation is:

Proof. Assume that every line before line $n$ on some TFL-proof is shiny, and that $\neg$E is used on line $n$. So the situation is:

We leave this as an exercise.

Proof. Assume that every line before line $n$ on some TFL-proof is shiny, and that $\neg$I is used on line $n$. So the situation is:

We leave these as exercises.

This establishes that all the basic rules of our proof system are rule-sound. Finally, we show:

Proof. Suppose that we used a derived rule to obtain some sentence, $𝒜$, on line $n$ of some TFL-proof, and that every earlier line is shiny. Every use of a derived rule can be replaced (at the cost of long-windedness) with multiple uses of basic rules. That is to say, we could have used basic rules to write $𝒜$ on some line $n+k$, without introducing any further assumptions. So, applying our individual results that all basic rules are rule-sound several times ($k+1$ times, in fact), we can see that line $n+k$ is shiny. Hence the derived rule is rule-sound. QED

And that’s that! We have shown that every rule—basic or otherwise—is rule-sound, 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 that no formal proof will lead you astray. That is: our proof system is sound.