Help in proving ∀x(¬A(x) → B(d)) ⊢ ∀xA(x) ∨ B(d) without using Disjunctive syllogism in the proof

Question

Stuck on a problem of ∀x(¬A(x) → B(d)) ⊢ ∀xA(x) ∨ B(d), however the system I am using does not allow me to use DS in the proof. Here is another method I tried, but it says that it's wrong on the last step. Anyone know how to go about solving this with just the basic rules for FOL and TFL natural deduction?

∀x(¬A(x) → B(d)):PR

-A(c)->B(d):AE 1

-A(c)/\-B(d):AS
-A(c):/\E 3
-B(d):/\E 3
B(d):->E 2,4
_|_:-E 5,6

-(-A(c)/-B(d)):-I 3-7

 -(A(c)\/B(d)):AS
    -A(c):AS
        -B(d):AS
        -A(c)/\-B(d):/\I 10,11
        _|_:-E 8,12
    B(d):IP 11-13
    A(c)\/B(d):\/I 14
    _|_:-E 9,15
--
    A(c):AS
    A(c)\/B(d):\/I 18
    _|_:-E 9,19
A(c):IP 10-16
-A(c):-I 18-20
_|_:-E 21,22

A(c)/B(d):IP 9-23

∀xA(x) ∨ B(d):AI 24

Answer 1

Let $\phi$ be: $$(\neg A \implies B) \implies (A \lor B)$$ You want to prove that $\phi$ is a tautology, using basic natural deduction rules.

\begin{align} (\neg A \implies B) \quad \neg A &&\text{Assumption (1) (2) respectively}\\ \ B \qquad \qquad&& \text{using implies elemination} \\ \ (A \lor B) \quad \neg(A \lor B)&& \text{using or introduction, Assumption (3)} \\ \ \bot \qquad \qquad&& \text{using not elemination} \\ \ A \qquad \qquad && \text{using contradiction elemination, eliminating assumption (1)} \\ \ (A \lor B) \quad \neg(A \lor B)&& \text{using or introduction, same assumption (3)} \\ \bot \qquad \qquad&& \text{using not elemination} \\ \ A \lor B \qquad \quad && \text{using contradiction elemination, eliminating assumption (3) two times}\\ (\neg A\implies B)\implies A\lor B &&\text{using implies introduction , eleminating assumption (1)}\\ \end{align}

Thus we proved $\vdash\phi$ without usign any assumption that is $\phi$ is a tautology (Note that all assumption where eliminated in the proof).