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

Question

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_6: B \to B \lor C$
• $L_7: 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 \to 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.

Answer 1

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:

5. $\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:

6. $\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)$.

Answer 2

For the fun of it, I looked for smaller proofs using my own tool pmGenerator – which exhaustively generates minimal condensed detachment proofs.
It turned out that a minimal such proof is 13 steps long (with all its formulas being distinct), so a proof with less than 13 formulas only exists if it references the same line (i.e. uses the same formula) multiple times.

Proof System

It should be noted that according to page 23 in section "Omitting Parentheses" of the referenced textbook

the order of precedence of operators in $\{\land,\lor,\to\}$ is $~\land,\lor~\prec~{\to}$.
For example, $L_6: B \to B \lor C$ means $B \to (B \lor C)$, which is CpApq in Polish notation (a most concise prefix notation with $(\to,\lnot,\land,\lor)=($C,N,K,A$)$). All axioms from the question in Polish notation are
$L:=\{$CpCqp, CCpCqrCCpqCpr, CpApq, CpAqp, CCpqCCrqCAprq, CCpqCCpNqNp, CNpCpq, ApNp$\}$,
and there are additionally

• $L_3:$ CKpqp $=B\land C\to B$
• $L_4:$ CKpqq $=B\land C\to C$
• $L_5:$ CpCqKpq $=B\to(C\to B\land C)$

allowed in the book's exercise, which define the $\land$-connective.

For condensed detachment, there is the so-called D-rule, which takes two formulas as arguments, on which it applies tree unification to form their most general unifiers of $\psi\to\varphi$ and $\psi$, respectively, then applies Modus Ponens, which results in $\varphi$.

Axioms in condensed detachment proofs are referred to by 1,2,…,9,a,b,…,z in their given order.

Solution (automated)

A minimal D-proof for ApCpq $=A\lor(A\to B)$ under $L$ is DDD53DD2D1478 (length 13), which translates to:

1. $A∨¬A$ $\ $---$\ \ L_{11}$
2. $¬A→(A→B)$ $\ $---$\ \ L_{10}$
3. $(A→B)→(A∨(A→B))$ $\ $---$\ \ L_7$
4. $((A→B)→(A∨(A→B)))→(¬A→((A→B)→(A∨(A→B))))$ $\ $---$\ \ L_1$
5. $¬A→((A→B)→(A∨(A→B)))$ $\ $---$\ \ \textit{MP}:3,4$
6. $(¬A→((A→B)→(A∨(A→B))))→((¬A→(A→B))→(¬A→(A∨(A→B))))$ $\ $---$\ \ L_2$
7. $(¬A→(A→B))→(¬A→(A∨(A→B)))$ $\ $---$\ \ \textit{MP}:5,6$
8. $¬A→(A∨(A→B))$ $\ $---$\ \ \textit{MP}:2,7$
9. $A→(A∨(A→B))$ $\ $---$\ \ L_6$
10. $(A→(A∨(A→B)))→((¬A→(A∨(A→B)))→((A∨¬A)→(A∨(A→B))))$ $\ $---$\ \ L_8$
11. $(¬A→(A∨(A→B)))→((A∨¬A)→(A∨(A→B)))$ $\ $---$\ \ \textit{MP}:9,10$
12. $(A∨¬A)→(A∨(A→B))$ $\ $---$\ \ \textit{MP}:8,11$
13. $A∨(A→B)$ $\ $---$\ \ \textit{MP}:1,12$

I obtained it as follows.

1. Generate all representative proofs of up to 13 steps, via
   $ ./pmGenerator -c -n -s CpCqp,CCpCqrCCpqCpr,CpApq,CpAqp,CCpqCCrqCAprq,CCpqCCpNqNp,CNpCpq,ApNp -g 13
2. Search for ApCpq in generated files via
   $ ./pmGenerator -c -n -s CpCqp,CCpCqrCCpqCpr,CpApq,CpAqp,CCpqCCrqCAprq,CCpqCCpNqNp,CNpCpq,ApNp --search ApCpq -n,
   resulting in output:

   Found [0] : "A0C0.1" (originally "ApCpq")
           in line 131392 - DDD53DD2D1478:A0C0.1
           of 'dProofs13.txt'.
   

3. Parse DDD53DD2D1478 with formulas in infix notation (unicode, -u) via
   $ ./pmGenerator -c -n -s CpCqp,CCpCqrCCpqCpr,CpApq,CpAqp,CCpqCCrqCAprq,CCpqCCpNqNp,CNpCpq,ApNp --parse DDD53DD2D1478 -u,
   resulting in output:

    1. 0∨¬0  (8)
    2. ¬0→(0→1)  (7)
    3. (0→1)→(0∨(0→1))  (4)
    4. ((0→1)→(0∨(0→1)))→(¬0→((0→1)→(0∨(0→1))))  (1)
    5. ¬0→((0→1)→(0∨(0→1)))  (D):3,4
    6. (¬0→((0→1)→(0∨(0→1))))→((¬0→(0→1))→(¬0→(0∨(0→1))))  (2)
    7. (¬0→(0→1))→(¬0→(0∨(0→1)))  (D):5,6
    8. ¬0→(0∨(0→1))  (D):2,7
    9. 0→(0∨(0→1))  (3)
    10. (0→(0∨(0→1)))→((¬0→(0∨(0→1)))→((0∨¬0)→(0∨(0→1))))  (5)
    11. (¬0→(0∨(0→1)))→((0∨¬0)→(0∨(0→1)))  (D):9,10
    12. (0∨¬0)→(0∨(0→1))  (D):8,11
    13. 0∨(0→1)  (D):1,12
   

4. Use {(1)↦$L_1$, (2)↦$L_2$, (3)↦$L_6$, (4)↦$L_7$, (5)↦$L_8$, (6)↦$L_9$, (7)↦$L_{10}$, (8)↦$L_{11}$} for translation.

More

Using $L\cup\{L_3,L_4,L_5\}$ via CpCqp,CCpCqrCCpqCpr,CKpqp,CKpqq,CpCqKpq,CpApq,CpAqp,CCpqCCrqCAprq,CCpqCCpNqNp,CNpCpq,ApNp resulted in DDD86DD2D17ab, which by axiom translations {(1)↦$L_1$, …, (9)↦$L_9$, (a)↦$L_{10}$, (b)↦$L_{11}$} is the same proof. (I'd recommend instead of -g 13 to use -g 9 -g 13 -u here, to avoid long filtering durations. I used -g 11 -g 13 -u, which ran over an hour.)
So there is no shortcut over $\land$-formulas.

I generated the top 5000 list of smallest conclusions provable from $\textit{MP},L_1,\dots,L_{11}$ in up to 13 steps (including minimal proofs) via
$ ./pmGenerator -c -n -s CpCqp,CCpCqrCCpqCpr,CKpqp,CKpqq,CpCqKpq,CpApq,CpAqp,CCpqCCrqCAprq,CCpqCCpNqNp,CNpCpq,ApNp --variate 1 -s --extract -t 5000 -s.
It includes all conclusions of symbolic lengths up to 11 (which are provable in up to 13 steps), and can be used as a resource to check for great solutions to many of the other exercises.