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:
- $A \Rightarrow (B \Rightarrow A)$
- $(A\Rightarrow(B\Rightarrow C))\Rightarrow((A\Rightarrow B)\Rightarrow(A\Rightarrow C))$
- $A \land B \Rightarrow A$
- $A\land B \Rightarrow B$
- $(A \Rightarrow B)\Rightarrow ((A\Rightarrow C)\Rightarrow (A\Rightarrow B \land C))$
- $A\Rightarrow A\lor B$
- $B\Rightarrow A\lor B$
- $(A\Rightarrow C)\Rightarrow ((B\Rightarrow C)\Rightarrow (A\lor B\Rightarrow C))$
- $(A\Rightarrow B)\Rightarrow(\lnot B \Rightarrow \lnot A)$
- $A \Rightarrow \lnot\lnot A$
- $\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!