I'm self-studying mathematical logic from "Introduction to Mathematical Logic" by Detlovs and Podnieks (available free here under CC license). Unfortunately, it doesn't come with any solutions. I'm stuck trying to prove ⊢ A∨(A→B), from Exercise 1.4.2 (i) on page 43. The text appears to be using the Hilbert-style deduction method.

Relevant axioms (classical logic)

  • $L_1: B \to (C \to B)$
  • $L_2: (B \to (C \to D)) \to ((B \to C) \to (B \to D))$
  • $L_3: B \to B \lor C$
  • $L_4: C \to B \lor C$
  • $L_8: (B \to D) \to ((C \to D) \to (B \lor C \to D))$
  • $L_9: (B \to C) \to ((B \to \lnot C) \to ¬B)$
  • $L_{10}: \lnot B \to (B \lor C)$
  • $L_{11}: B \lor \lnot B$

Relevant inference rules

  • Modus Ponens


  1. $(A \to A \lor (A \to B)) \to ((\lnot A \to A \lor (A \to B)) \to (A \lor \lnot A \to A \lor (A \to B)))$ --- $L_8$
  2. $A \to A \lor (A \to B)$ --- $L_6$
  3. $A \lor \lnot A$ --- $L_{11}$
  4. $(\lnot A \to A \lor (A \to B)) \to (A \lor \lnot A \to A \lor (A \to B))$ --- from (1) and (2) by MP
  5. $(\lnot A \to A \lor (A \to B)) \to A \lor (A \to B)$ --- from (3) and (4) by MP
  6. $(\lnot A \to (A \to A \lor (A \to B))) \to ((\lnot A \to A) \to (\lnot A \to A \lor (A \to B)))$ --- $L_2$
  7. $(\lnot A \to (A \to A \lor (A \to B)))$ --- $L_{10}$
  8. $(\lnot A \to A) \to (\lnot A \to A \lor (A \to B))$ --- from (6) and (7) by MP

I'm stuck at this point because $\lnot A \to A$ appears to be a contradiction. I'm also not sure whether this is the right approach. It looks alright at formula 5, but I'm not sure how to prove $\lnot A \to A \lor (A \to B)$, since it requires proving that $A \lor (A \to B)$ is always true, which is what we're trying to prove in the first place.

The text states that it can be solved using 14 formulas, 13 being the shortest yet.

  • $\begingroup$ The "proof strategy" is to use L11: $A \lor \lnot A$ and derive $A \lor (A \to B)$ from $A$ with L6 and from $\lnot A$ with L10. Then use L8 $\endgroup$ – Mauro ALLEGRANZA Jul 5 '20 at 16:48
  • $\begingroup$ @MauroALLEGRANZA I seem to have done the first three steps in my attempt (if I understood correctly); substituting B=A, C=¬A for L8 seems to yield (A→D)→((¬A→D)→D) after simplifying. The only straightforward substitution for D that I haven't tried seems to be D=(¬A→A∨(A→B)) but that leads to a double negation case with L10, which hasn't been proved yet. $\endgroup$ – user383527 Jul 5 '20 at 20:36

I assume that you are forced not tu use the Deduction Theorem.

But you can use the so-called Law of Syllogism (transitivity of $\to$).

If so, here is a sketch of a derivation:

  1. $\vdash A \to (A \lor (A \to B))$ --- L6

  2. $\vdash \lnot A \to (A \to B)$ --- L10

  3. $\vdash (A \to B) \to (A \lor (A \to B))$ --- L7

  4. $\vdash \lnot A \to (A \lor (A \to B))$ --- from 2. and 3. by Syllogism.

Now we can "cook them" together using L8:

  1. $\vdash (A \to (A \lor (A \to B))) \to [(\lnot A \to (A \lor (A \to B))) \to ((A \lor \lnot A) \to (A \lor (A \to B)))]$

Now, from 5., 1. and 4. by MP twice:

  1. $\vdash (A \lor \lnot A) \to (A \lor (A \to B))$

Finally, using L11: $\vdash A \lor \lnot A$, by MP:

$\vdash A \lor (A \to B)$.

  • $\begingroup$ Smart use of the law of syllogism! The text has proved it as a theorem, so it is straightforward to show it from (2) and (3). In total, this gives 13 formulas (verbosely written), which the text says is the shortest proof. $\endgroup$ – user383527 Jul 6 '20 at 22:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy