Section Progress:

19.2 Proving Soundness

In this section we will do some metalogic and prove the soundness of BOOL, which says: If a conclusion, C, is provable (in a formal proof) from some premises, then those premises really do entail C.

Soundness: If an argument is formally provable in BOOL, then the argument is valid.

In other words: any argument we can give a formal proof of in BOOL really is valid.

Actually, we are going to prove a slightly simpler version of soundness for BOOL.

Soundness is a conditional claim, and the antecedent concerns arguments that we can give a formal proof of. That is talking about any argument we can give a formal proof of, whether that proof takes 1 step or 10 steps or 100 steps.

Soundness covers all these possibilities: if we can prove it in BOOL, it really is valid.

What we are going to do is just consider the simplest case: arguments with 1 step. In other words, arguments with no intermediary conclusions: the conclusion itself is the only line under the premises.

1-Step Soundness: If conclusion can be proven in BOOL with a one-step formal proof, then that conclusion really is a logical consequence of the premises.

We’ll call this theorem 1-Step Soundness: Any formal proof in BOOL with just one step really is valid.

Instead of just proving it for you, though, we’re going to show you that you can figure out how to prove it yourself.

For starters, note that this theorem is necessarily true: we can prove it without any premises. All we need to do is remember our logical definitions and our proof skills.

The logical structure of 1-Step Soundness is a conditional. It says: IF …, THEN …

Okay, now we have a plan. Let’s assume that a conclusion, C, is provable in one-step from some premises. What we want to show is that those premises really do validly entail C. If we do that, then we’ve proven soundness via conditional proof.

Next, recall our definition of formal proofs: every line of the formal proof below the premises must be justified by one of the 7 proof rules of BOOL: Reit, plus Intro and Elim rules for each connective.

So we now know a distinction: the one step of our one-step proof is justified by Reit, or &Intro, or &Elim, or vIntro, or vElim, or ~Intro, or ~Elim.

Now we have a plan: using proof by cases, we take each case in turn and prove that if the conclusion was justified by that rule, then it really is a valid consequence of the premises.

Two of the cases are actually quite easy to dispatch, because they are impossible.

We are making progress, because now we know that the conclusion was justified by just one of these 5 rules: Reit, &Intro, &Elim, vIntro or ~Elim.

So our proof by cases only has 5 cases to deal with.

Now let’s do some of the cases.

Case 1: Reit. Say the conclusion is justified by Reit. What we want to show is that the conclusion really does follow from the premises.

That is easy: since the conclusion is justified by Reit, that means it is identical to one of the premises. So we know it is valid, because that means it is a circular argument, which is one of the weird cases of validity. So that case is done.

Case 2: &Intro. If the conclusion is justified by &Intro, that means the conclusion is a complex sentence that has a structure like this: X&Y, where X and Y are two of the premises. We know that because that’s how we define the &Intro rule.

What we need to show is that the conclusion follows from the premises. To do that, just recall our definition of validity: IF the premises are true, THEN the conclusion is true. Since this is a conditional, we assume the antecedent: assume that the premises are true. Since X and Y are among the premises, that means X is true and Y is true. And what we have to show is that the conclusion, X&Y, is true. But that follows immediately from the truth table for conjunction: if both conjuncts are true, then so is the conjunction. That takes care of case 2.

Now that you’ve seen how two of the cases work, you should be able to figure the rest of them out. Basically, we end up using how the rules are defined, plus how the truth-functional connectives are defined, and that allows us to show that the argument is valid in each case.

Your turn to try.

Let’s keep going.

Now there’s only one more case to go.

1-Step Soundness: If a conclusion is provable (in a formal proof) from some premises, then those premises really do entail C.

We showed that in every case, the premises really do prove the conclusion.

That means we’ve completed the  proof of 1-Step Soundness.

We started, remember, by assuming that some conclusion (call it C) was provable in BOOL from some premises, and we needed to show that the premises logically entail C.

That meant that C was justified by one of 5 rules, so we did a proof by cases and showed that C is entailed by the premises no matter which of the rules it is.

It took a bit of work, but that’s a pretty big metalogic accomplishment. The proof of the unrestricted version of soundness is only slightly more complicated, but we won’t do it here. It’s a standard topic in advanced logic classes.

19.2 Proving Soundness