19.1 Soundness and Completeness
In this chapter we get a glimpse of some topics in advanced logic.
We have already learned logical systems like BOOL and PROP, and we've used them to prove certain arguments are valid. When we do that, we reason in or with a logical system.
But we can also step back and reason about logical systems. That's what metalogic is. "Meta" means coming "afterward", being "about" something in a more abstract way. Metalogic comes after you've learned some logic, when you want to abstractly reason about logic itself.
For example, think about this. We have two ways to prove an argument is valid using logical systems like BOOL and PROP.
First, we can use the truth-table method, where we construct a joint truth table and see if the conclusion is true on every row on which all the premises are true.
Second, we can give a formal proof of the conclusion from the premises.
That means we can ask metalogical questions like whether these two methods always deliver the same verdict. If we designed our logical systems well, anything you can do with the first, you can do with the second, and vice versa.
Figuring out how to prove that is one of the basic topics of metalogic. More specifically, this is what we want to prove:
- Soundness: If we can give a formal proof of an argument, then it is valid (by the truth-table method).
- Completeness: If an argument is valid (by the truth-table method), then we can give a formal proof of it.
To avoid confusion, the first thing you should realize is that calling a logical system "sound" is not the same as calling an argument sound. It is just an unfortunate coincidence that the same word is used.
In a sense, soundness says that we don't have too many rules: we only have rules that lead to valid conclusions; we don't have any bad rules among them.
Completeness says we have enough rules: we don't need any more, because our rules can prove any valid argument.
At least, our rules can prove any tautologically valid argument; that is, one whose validity just depends on the truth-functional connectives. There are other areas of logic that BOOL and PROP don't cover, which we'll see in later chapters.
The word "theorem" means an important truth about something that we can prove, so soundness and completeness are called metalogical theorems
Let's see if you can reconstruct them.
Since we are calling them theorems, you probably could have guessed that BOOL and PROP are both sound and complete.
That might seem odd, because PROP has more than BOOL does: PROP has more symbols and more proof rules. This mystery is explained later in this chapter, though, when we prove the the extra symbols and rules in PROP are a luxury, not a necessity.
In this book we won't prove completeness, because it takes a lot of work. That is a standard topic in advanced logic classes.
What we will do, however, is prove a version of soundness in the next section.
First, see if you can figure this out.