# How can I progress this derivation?

I'm learning propositional calculus in a discrete mathematics course.

I'm trying to kick the habit of using axioms like equations and now I'm a little stuck and could use a nudge.

Using a compact Hilbert system of axioms: $$\begin{array}[ll] \text{a1}:&A\lor A\Rightarrow A\\ \text{a2}:&A\Rightarrow A\lor B\\ \text{a3}:&A\lor B\Rightarrow B\lor A\\ \text{a4}:&(A\Rightarrow B)\Rightarrow((C\Rightarrow A)\Rightarrow (C\Rightarrow B))\\ \end{array} \\\\ \text{Prove: }A\Rightarrow A$$

I derived the following:

$$\begin{array}[lll] \\ 1&(A\Rightarrow B)\Rightarrow((A\lor A\Rightarrow A)\Rightarrow (A \lor A\Rightarrow B))&\text{using C=A\lor A in a4}\\ 2&(A\Rightarrow B)\Rightarrow (A\lor A\Rightarrow B)&\text{mp using 1 and a1}\\ 3&(A\Rightarrow A\lor B)\Rightarrow(A\lor A \Rightarrow A\lor B)&\text{sub. A\lor B for B}\\ 4&A\lor A\Rightarrow A\lor B&\text{mp using 3 and a2}\\ \end{array}$$ I'm pretty sure I'm not too far off of getting this to come together but I'm a little stumped as to an appropriate substitution.

Or have I taken a wrong turn in one of my substitutions already?

-
How does your second step follow from axiom 2? –  mjqxxxx Oct 4 '12 at 19:00
I think I'm substituting again instead of deducing ... –  Stephen Oct 4 '12 at 19:06
The only way to derive $A \Rightarrow A$ is using axiom 4 (or axiom 1, if you could first derive $(A \Rightarrow A) \vee (A \Rightarrow A)$, which seems harder rather than easier). Replacing $B$ and $C$ with $A$, and $A$ with $B$, in axiom 4 gives you $(B \Rightarrow A) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow A))$. So if you can get $B \Rightarrow A$ and $A \Rightarrow B$ for any formula $B$, you have the result. Can you see what $B$ should be? –  mjqxxxx Oct 4 '12 at 20:43
If I substituted $A\lor A$ for B I could use mp to eliminate the first implication leaving $(A\Rightarrow A\lor A)\Rightarrow (A\Rightarrow A)$ and then if I use a specialization of a2 I can use mp again to leave me with $A\Rightarrow A$? (I will explore this on my chalk board but I think that's the direction you're pointing me) –  Stephen Oct 4 '12 at 21:33
@mjqxxxx Thank you for your help, it's greatly aided my understanding. I think I will try to find a book or site with a list of problems so I can practice this more. –  Stephen Oct 4 '12 at 21:34

The only way to derive $A \Rightarrow A$ is using axiom 4 (or axiom 1, if you could first derive $(A \Rightarrow A) \vee (A \Rightarrow A)$, which seems harder rather than easier). Replacing $B$ and $C$ with $A$, and $A$ with $B$, in axiom 4 gives $(B\Rightarrow A) \Rightarrow ((A\Rightarrow B)\Rightarrow(A\Rightarrow A))$. So if you can get $B \Rightarrow A$ and $A \Rightarrow B$ for any formula $B$, you have the result. Using $A\vee A$ in place of $B$ works. Here's a proof: $$\begin{array}{ l l l } \text{a.} & (A \vee A\Rightarrow A) \Rightarrow ((A\Rightarrow A\vee A)\Rightarrow (A\Rightarrow A)) & \text{(specialization of axiom 4)} \\ \text{b.} & (A\Rightarrow A\vee A)\Rightarrow(A\Rightarrow A) & \text{(a. and axiom 1, using modus ponens)} \\ \text{c.} & A\Rightarrow A\vee A & \text{(specialization of axiom 2)} \\ \text{d.} & A\Rightarrow A & \text{(b. and c., using modus ponens)} \\ \end{array}$$