# 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
-------------
Tautology``````

## Another 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``````