A First Deduction

The first deduction we’ll make will be a deduction of the formula (A → A); that is we will show that ├ (A → A). To find a deduction, I will work backwards (much in the way one constructs elementary ε-δ proofs). Consider the formula schemata

(3) ((A → (A → A)) → (A → A))

(4) (A → (A → A))

(5) (A → A)

Observe that (5) follows by Modus Ponens from (4) and (3) and that all instances of (4) are instances of L1. It follows that we can make a deduction of (5) by adding two lines to a deduction of (3), if there is a deduction of (3). The question is then whether we can deduce (3), and the answer is, Yes we can. Observe that instances of (3) have structure

((A → (A → A)) → (A → A)),

which makes them right-hand sides of instances of L2, where the left-hand sides are

(A → ((A → A) → A)).

Furthermore, all of these left-hand sides are instances of L1. So, we have all the pieces we need to make a deduction:

1. (A → ((A → A) → A)) L1.

2. ((A → ((A → A) → A)) → ((A → (A → A)) → (A → A))) L2

3. ((A → (A → A)) → (A → A)) MP(1,2)

4. (A → (A → A)) L1

5. (A → A) MP(4,3)