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)
Proof(
1 SubProof(
2 Assume( ¬(p ∨ ¬p) ),
3 SubProof(
4 Assume( p ),
5 ( p ∨ ¬ p ) by OrI1(4),
6 ( F ) by NegE(5, 2)
),
7 ( ¬p ) by NotI(3),
8 ( p ∨ ¬p ) by OrI2(7),
9 ( F ) By NegE(8, 2)
),
10 ( p ∨ ¬p ) By 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))
Proof(
1 SubProof(
2 Assume( p → q ),
//goal: reach (¬p → q) → q
),
//use ImplyI 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))
Proof(
1 SubProof(
2 Assume( p → q ),
3 SubProof(
4 Assume( ¬p → q ),
//goal: reach q
)
//use ImplyI to conclude (¬p → q) → q
//goal: reach (¬p → q) → q
),
//use ImplyI 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))
Proof(
1 SubProof(
2 Assume( p → q ),
3 SubProof(
4 Assume( ¬p → q ),
//Begin LEM proof, p ∨ ¬p
5 SubProof(
6 Assume( ¬(p ∨ ¬p) ),
7 SubProof(
8 Assume( p ),
9 ( p ∨ ¬ p ) by OrI1(8),
10 ( F ) by NegE(9, 6)
),
11 ( ¬p ) by NotI(7),
12 ( p ∨ ¬p ) by OrI2(11),
13 ( F ) By NegE(12, 4)
),
14 ( p ∨ ¬p ) By PbC(5)
//End LEM proof for p ∨ ¬p
//goal: reach q
)
//use ImplyI to conclude (¬p → q) → q
//goal: reach (¬p → q) → q
),
//use ImplyI 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))
Proof(
1 SubProof(
2 Assume( p → q ),
3 SubProof(
4 Assume( ¬p → q ),
//Begin LEM proof, p ∨ ¬p
5 SubProof(
6 Assume( ¬(p ∨ ¬p) ),
7 SubProof(
8 Assume( p ),
9 ( p ∨ ¬ p ) by OrI1(8),
10 ( F ) by NegE(9, 6)
),
11 ( ¬p ) by NotI(7),
12 ( p ∨ ¬p ) by OrI2(11),
13 ( F ) By NegE(12, 4)
),
14 ( p ∨ ¬p ) By PbC(5),
//End LEM proof for p ∨ ¬p
//use OR elimination on p ∨ ¬p, try to reach q
15 SubProof(
16 Assume( p ),
17 ( q ) By ImplyE(2, 16)
),
18 SubProof(
19 Assume( ¬p ),
20 ( q ) By ImplyE(4, 19)
),
21 ( q ) By OrE(14, 15, 18)
//goal: reach q
)
//use ImplyI to conclude (¬p → q) → q
22 ( (¬p → q) → q ) By ImplyI(3)
//goal: reach (¬p → q) → q
),
//use ImplyI to conclude (p → q) → ((¬p → q) → q)
23 ( (p → q) → ((¬p → q) → q) ) By ImplyI(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