The other day I learned a short proof that the Propositional Calculus is consistent.
This was a bit of a surprise to me since I’m steeped in all sorts of much more advanced Gödel results, which I’m not really qualified to contemplate, and the whole thing makes it seem like proving a system consistent should be a Herculean effort. But for PC it turns out to be rather simple.
I won't try to explain here what PC is. But I will try to explain what “consistent” means.
The key is to split everything you know about boolean logic into two disjoint categories: semantics and derivations.
-
The semantics of PC are about truth-values. In a semantic view of the formula ((P ⊃ Q) ⊃ (¬Q ⊃ ¬P)), the letters P and Q are boolean variables, ¬ is boolean NOT, and ⊃ is a binary operator such that a ⊃ b means "NOT (a AND NOT b)". This particular formula is valid, which means that no matter what values you assign to P and Q, the formula evaluates to true.
-
Derivations are proofs. There's a formal definition of what constitutes a proof in the Propositional Calculus: you're given some axioms to start with, and some derivation rules that produce new theorems from those axioms.
Key point: those derivation rules, and derivations generally, don't operate on boolean values at all: it's more like processing the formulas themselves, as strings, using regular expressions. You can check a proof without knowing that "¬" means NOT or that "∧" means AND. (For this reason, instead of "semantics and derivations", the two categories are typically called "semantics and syntax".) Conversely, you can show that a formula is semantically valid without proving it with a derivation—just check all possible combinations of boolean values.
But both views are well-defined. There's nothing mysterious about boolean operators. And there's nothing all that mysterious about string manipulation either.
Soundness
PC is considered "sound" if every theorem you can prove (in the derivation system) is in fact valid (semantically). It's a kind of agreement between these two independent systems.
It's pretty easy to show that PC is sound:
You can just manually check that each axiom is valid by trying all possible combinations of boolean values. Spoiler: they're all valid.
Then you must show that the derivation rules of PC preserve validity. If the inputs to the Modus Ponens rule are both valid, for example, then the result will be valid. I'll skip the details but it's also pretty straightforward.
But taken together, (1) and (2) mean that every step of a proof is necessarily a valid formula. And so the conclusion of every proof is valid, and thus PC is sound, Q.E.D.
Consistency
Now, a deductive system is "consistent" if it is impossible to prove two contradictory theorems (that is, two theorems that are the same except one adds a ¬ operator at the front). (There are other possible definitions of an inconsistency, but they're all equivalent as far as PC is concerned.)
So here we are finally.
Theorem: PC is consistent.
Proof: Suppose we did have proofs in PC of two contradictory theorems. Both must be valid, since PC is sound. But if the first is valid, it always evaluates to true. And in that case the second would be always false, and thus not valid—a contradiction. Therefore there are no such contradictions in PC, and therefore it is consistent.
