# Does this proof using Novikov axiomatic propositional logic hold?

This question seems absolutely elementary but I'm having a hard time completing the proof, in fact I may have taken a bit of a left turn on it or I may be improperly applying axioms all together. Clearly I'm not asking for a complete solution, but if anyone can offer anything that will increase my insight I would appreciate it..

Prove that $$A \lor A \Rightarrow A$$ using the Novikov axiom system.

The axioms I have are stated as:

1. $A \Rightarrow (B \Rightarrow A)$
2. $(A\Rightarrow(B\Rightarrow C))\Rightarrow((A\Rightarrow B)\Rightarrow(A\Rightarrow C))$
3. $A \land B \Rightarrow A$
4. $A\land B \Rightarrow B$
5. $(A \Rightarrow B)\Rightarrow ((A\Rightarrow C)\Rightarrow (A\Rightarrow B \land C))$
6. $A\Rightarrow A\lor B$
7. $B\Rightarrow A\lor B$
8. $(A\Rightarrow C)\Rightarrow ((B\Rightarrow C)\Rightarrow (A\lor B\Rightarrow C))$
9. $(A\Rightarrow B)\Rightarrow(\lnot B \Rightarrow \lnot A)$
10. $A \Rightarrow \lnot\lnot A$
11. $\lnot\lnot A\Rightarrow A$

We may use a substitution (specialization) and modus ponens.

So based on the idea that I will need to use something more expanded to start with and try to contract it:

Start with 8: $(A\Rightarrow C)\Rightarrow ((B\Rightarrow C)\Rightarrow (A\lor B\Rightarrow C))$

Apply 6: $(A\Rightarrow C)\Rightarrow ((B\Rightarrow C)\Rightarrow (A \Rightarrow C))$

Apply 6: $(A \lor B\Rightarrow C)\Rightarrow ((B\Rightarrow C)\Rightarrow (A \lor B \Rightarrow C))$

Apply 7: $(A \lor A \lor B\Rightarrow C)\Rightarrow ((A \lor B\Rightarrow C)\Rightarrow (A \lor A \lor B \Rightarrow C))$

Apply 6: $(A \lor A \Rightarrow C)\Rightarrow ((A \Rightarrow C)\Rightarrow (A \lor A \Rightarrow C))$

Apply 3: (rearranging A and C using rename rules) $(A \lor A \Rightarrow A \land C)\Rightarrow ((A \Rightarrow A \land C)\Rightarrow (A \lor A \Rightarrow A \land C))$

Apply 3: $(A \lor A \Rightarrow A)\Rightarrow ((A \Rightarrow A)\Rightarrow (A \lor A \Rightarrow A))$

Apply 1: $(A \lor A)\Rightarrow ((A)\Rightarrow (A \lor A))$

Apply 6: $(A \lor A)\Rightarrow (A\Rightarrow A)$

Apply 1: (or modus ponens?) $A \lor A\Rightarrow A$

I think this is wrong because I don't think I can use 6 both to expand A and also to contract $A \lor B$ ... I think the rule would need a $\Leftrightarrow$ for that.

Thanks!

-

There aren't a lot of ways to derive something about $\vee$; axiom 8 is about it. From it (setting $B=C=A$), you can see that if we knew $A \Rightarrow A$, we could derive $(A\Rightarrow A)\Rightarrow (A\vee A \Rightarrow A)$, and from there derive $A\vee A \Rightarrow A$. So how to derive $A \Rightarrow A$? From axiom 2 (setting $C=A$) and axiom 1, we derive $(A\Rightarrow B)\Rightarrow(A\Rightarrow A)$. Now we just need to derive $A\Rightarrow B$ for any old $B$. There are several axioms of this form; any of axiom 1, axiom 6, or axiom 10 will work. We may as well use axiom 1 again. The upshot is that we can derive $A \vee A \Rightarrow A$ using only axioms (axiom schemas) 1, 2, and 8, together with modus ponens: $$\begin{array}{ l l l } \text{a.} & (A \Rightarrow (B \Rightarrow A)) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow A)) & \text{(specialization of axiom 2)} \\ \text{b.} & (A\Rightarrow B)\Rightarrow (A\Rightarrow A) & \text{(a. and axiom 1, using modus ponens)} \\ \text{c.} & A\Rightarrow (A\Rightarrow A) & \text{(specialization of axiom 1)} \\ \text{d.} & (A\Rightarrow (A\Rightarrow A)) \Rightarrow (A\Rightarrow A) & \text{(specialization of b.)} \\ \text{e.} & A\Rightarrow A & \text{(c. and d., using modus ponens)} \\ \text{f.} & (A \Rightarrow A) \Rightarrow ((A \Rightarrow A) \Rightarrow (A \vee A \Rightarrow A)) & \text{(specialization of axiom 8)} \\ \text{g.} & (A \Rightarrow A) \Rightarrow (A \vee A \Rightarrow A) & \text{(e. and f., using modus ponens)} \\ \text{h.} & A \vee A \Rightarrow A & \text{(e. and g., using modus ponens)} \\ \end{array}$$
I'm not certain I understand d. as a specialization of b, it looks like you used a specialization of c to get $B\Rightarrow(B\Rightarrow B)$ which then leads to $(A\Rightarrow(B\Rightarrow B))\Rightarrow(A\Rightarrow A)$? –  Stephen Oct 4 '12 at 17:00
d. is a specialization of b. obtained by taking $B$ to be the formula $(A \Rightarrow A)$. –  mjqxxxx Oct 4 '12 at 17:01