Fitch Style Proof $\forall x (\neg A(x) \rightarrow B(d)) \therefore \forall x A(x) \lor B(d)$.

Question

I really need some help with the following proof. I want to show that $\forall x (\neg A(x) \rightarrow B(d)) \therefore \forall x A(x) \lor B(d)$.

I tried to proof it with an indirect proof but always ended with something else. I dont know which subproof I should choose to start with. I know that I need one, because I cant do muss with the implication in my premise.

Maybe I can assume $ \neg (\forall x A(x))$ for my indirect proof?

Indirect proof means this (proof per contradiction):

Answer 1

Using material implication you can substitute $\lnot A(x) \to B(d)$ with $ \lnot\lnot A(x) \lor B(d)$ and then, using double negation elimination, with $ A(x) \lor B(d)$. You have then $$ \forall x \big(A(x) \lor B(d) \big)$$ which, using distributivity of the universal quantifier, is equivalent to $$ \big(\forall x A(x)\big) \lor B(d) $$

Answer 2

$\def\fitch#1#2{~~~~\begin{array}{|l}#1 \\\hline #2\end{array}}$

To derive a disjunction you must either derive one of its disjuncts, or use a reduction to absurdity.   This requires the later approach.

To derive a contradiction under the premise and assumption of $\lnot((\forall x~A(x))\lor B(d))$, first derive $\forall x~A(x)$ then use disjunction introduction.

$$\fitch{\forall x~(\lnot A(x)\to B(d))}{\fitch{\lnot((\forall x~A(x))\lor B(d))}{\fitch{\boxed a}{~~\vdots\\A(a)}\\\forall x~A(x)\hspace{20ex}\forall\textsf{I}\\(\forall x~A(x))\lor B(d)\hspace{10.5ex}{\lor}\textsf{I}\\\bot\hspace{26ex}\lnot\textsf{E}}\\(\forall x~A(x))\lor B(d)\hspace{14ex}\textsf{IP}}$$

So, now just derive $A(a)$ for an assumed arbitrary term $a$. (Hint: second verse is much the same as the first).