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