Theorems
Definition
A theorem in propositional logic is something that is always true with no need for premises. The truth table for a theorem is always a tautology – it is true for any truth assignment.
To express a theorem as a sequent, we write:
⊢ (theorem)This shows that we are trying to prove our theorem with NO premises. Such a proof will always immediately begin with a subproof, as there are no premises to process.
Law of the excluded middle, revisited
For example, the law of the excluded middle (LEM), p ∨ ¬p, is a theorem. We proved in section 4.5 that p ∨ ¬p is always true with no premises:
⊢ p ∨ ¬ p
{
1. {
2. ¬ (p ∨ ¬ p) assume
3. {
4. p assume
5. p ∨ ¬ p ∨i1 4
6. ⊥ ¬e 5 2
}
7. ¬ p ¬i 3
8. p ∨ ¬ p ∨i2 7
9. ⊥ ¬e 8 2
}
10. p ∨ ¬ p pbc 1
}We also see that the truth table for LEM is a tautology:
*
-------------
p | p ∨ ¬ p
-------------
T | T F
F | T T
-------------
TautologyAnother example
Suppose we wish to prove the following theorem of propositional logic:
(p → q) → ((¬p → q) → q)We would need to prove the sequent:
⊢ (p → q) → ((¬p → q) → q)We see that the top-level operator of what we are trying to prove is an implies operator. So, we begin our proof using the strategy for implies introduction:
⊢ (p → q) → ((¬p → q) → q)
{
1. {
2. p → q assume
//goal: reach (¬p → q) → q
}
//use →i to conclude (p → q) → ((¬p → q) → q)
}Inside subproof 1, we are trying to prove (¬p → q) → q. The top-level operator of that statement is an implies, so we nest another subproof with the goal of using implies introduction:
⊢ (p → q) → ((¬p → q) → q)
{
1. {
2. p → q assume
3. {
4. ¬p → q assume
//goal: reach q
}
//use →i to conclude (¬p → q) → q
//goal: reach (¬p → q) → q
}
//use →i to conclude (p → q) → ((¬p → q) → q)
}Now we must prove q in subproof 3. We have available propositions p → q and ¬p → q – we can see that if we had LEM (p ∨ ¬p) available, then we could use OR elimination to get our q in both cases. We insert the LEM proof into subproof 3:
⊢ (p → q) → ((¬p → q) → q)
{
1. {
2. p → q assume
3. {
4. ¬p → q assume
//Begin LEM proof, p ∨ ¬p
5. {
6. ¬ (p ∨ ¬ p) assume
7. {
8. p assume
9. p ∨ ¬ p ∨i1 8
10. ⊥ ¬e 9 6
}
11. ¬ p ¬i 7
12. p ∨ ¬ p ∨i2 11
13. ⊥ ¬e 12 6
}
14. p ∨ ¬ p pbc 5
//End LEM proof for p ∨ ¬p
//use OR elimination on p ∨ ¬p
//goal: reach q
}
//use →i to conclude (¬p → q) → q
//goal: reach (¬p → q) → q
}
//use →i to conclude (p → q) → ((¬p → q) → q)
}Finally, we do OR elimination with p ∨ ¬p and tie together the rest of the proof:
⊢ (p → q) → ((¬p → q) → q)
{
1. {
2. p → q assume
3. {
4. ¬p → q assume
//Begin LEM proof, p ∨ ¬p
5. {
6. ¬ (p ∨ ¬ p) assume
7. {
8. p assume
9. p ∨ ¬ p ∨i1 8
10. ⊥ ¬e 9 6
}
11. ¬ p ¬i 7
12. p ∨ ¬ p ∨i2 11
13. ⊥ ¬e 12 6
}
14. p ∨ ¬ p pbc 5
//End LEM proof for p ∨ ¬p
//use OR elimination on p ∨ ¬p, try to reach q
15. {
16. p assume
17. q →e 2 16
}
18. {
19. ¬ p assume
20. q →e 4 19
}
21. q ∨e 14 15 18
//goal: reach q
}
//use →i to conclude (¬p → q) → q
22. (¬p → q) → q →i 3
//goal: reach (¬p → q) → q
}
//use →i to conclude (p → q) → ((¬p → q) → q)
23. (p → q) → ((¬p → q) → q) →i 1
}If we complete a truth table for (p → q) → ((¬p → q) → q), we also see that it is a tautology:
*
-------------------------------
p q | (p → q) → ((¬p → q) → q)
-------------------------------
T T | T T F T T
T F | F T F T F
F T | T T T T T
F F | T T T F T
------------------------------
Tautology