Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.


share|cite|improve this question
up vote 1 down vote accepted

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} $$

share|cite|improve this answer
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
Thanks, I was overcomplicating things. – Stephen Oct 4 '12 at 17:02

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.