# Proving ⊢ A∨(A→B) using Hilbert system

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

Attempt

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.

• 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 – Mauro ALLEGRANZA Jul 5 '20 at 16:48
• @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. – 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)$$.

• 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. – user383527 Jul 6 '20 at 22:35