Theorems of Propositional Logic
All the derivations we've constructed in this chapter have begun with one or more premises. We used the premises as the starting points for drawing inferences using the rules of inference, the equivalence rules, and most recently, conditional and indirect proof. When using conditional and indirect proof, we saw that we could introduce temporary assumptions, beyond the initial premises which we were given to start our derivations and proofs. Although our sample derivations using conditional and indirect proof began with premises, one can construct derivations which don't begin with premises at all! That's because the use of conditional and indirect proof allow us to introduce assumptions, and we can start a proof with one or more assumptions, even when there are no premises. When we prove a wff without using any premises, we call the last line of such a proof a theorem.
As usual, we look at an example. We'll show that the wff (P v ~P) is a theorem, that is, that we can construct a proof of it from no premises. To do that we'll use indirect proof. We'll assume ~(P v ~P) and derive a contradiction, and infer (P v ~P) by indirect proof. Here we go:
| 1. | ~(P v ~P) | assump, ip | SP1 |
| 2. | (~P & ~~P) | DEM, 1 | SP |
| 3. | (~P & P) | DN, 2 | SP1 |
| 4. | (P & ~P) | COM, 3 | SP1 |
| 5. | (P v ~P) | ip, 1-4 |
This is a short proof! We assumed the negation of what we were looking for, and we constructed an indirect proof from the assumption without delay.
Let's prove a theorem using conditional proof. The theorem we'll prove is (A ⊃ (B ⊃ A)).
| 1. | A | assump, cp | SP1 |
| 2. | B | assump, cp | SP1, SP2 |
| 3. | A v ~B | disj, 1 | SP1, SP2 |
| 4. | A | ds, 2, 3 | SP1, SP2 |
| 5. | (B ⊃ A) | cp, 2-4 | SP1 |
| 6. | (A ⊃ (B ⊃ A)) | cp, 1 - 5 |
In this proof we began by assuming the antecedent of the main conditional, and then we immediately introduced another subproof, assuming the antecedent of the embedded conditional. Lines 3 and 4 use disjoining and disjunctive syllogism to infer a line we already had, namely line 1. This indirect way of inferring something we already had on an earlier line is necessary because there is no rule which says that you can simply repeat a line. Note that this proof uses nested subproofs, a technique we introduced earlier.
How do you know when a wff is a theorem and when it isn't? That's the subject of the final section of this chapter. But before moving on, please prove some theorems!
 |
 |