Working on P.D. Magnus. forallX: an Introduction to Formal Logic (pp. 297, exercise C. 3):
$
\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}
\fitch{\forall x(A \vee B(x))}{
\fitch{\neg(A \vee \forall xB(x))}{
\fitch{\neg A}{
A \vee B(c) \qquad (\forall E, 1)\\
\fitch{A}{
\bot \qquad (\neg E, 3, 5)\\
B(c) \qquad (X, 6)\\
}\\
\fitch{B(c)}{
B(c) \qquad (R, 8)
}\\
B(c) \qquad (\vee E, 5-7,8-9)\\
\forall xB(x) \qquad (\forall I, 10)\\
A \vee \forall xB(x) \qquad (\vee I,11)\\
\bot \qquad (\vee I,1, 11)\\
}\\
A \qquad (IP, 3-12)\\
A \vee \forall xB(x) \qquad (\vee I,13)\\
\bot \qquad (\neg E, 1,14)\\
}\\
A \vee \forall xB(x) \qquad (IP, 1-15)\\
}
$
Is this the right approach to this proof ?
Best Answer
$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}$
$\def\context#1#2{[#1]\\\left\lvert{#2}\right.}$ Your proof is valid, but you do not need to assume $\neg A$.
The contradiction you need for your disjunction elimination can be of the assumption $\neg(A\vee\forall x~B(x))$
That will streamline things a little bit.
$$\fitch{~~1.~\forall x~(A\vee B(x))}{\fitch{~~2.~\neg (A\vee\forall x~B(x))}{\hspace{-1ex}\left\lvert \raise{11ex}{{~~3.~A\vee B(c)\hspace{10ex}\forall\mathsf E~1\\\fitch{~~4.~A\hspace{13ex}\textsf{Assume}}{~~5.~A\vee\forall x~B(x)\hspace{2ex}\vee\mathsf I~4\\~~6.~\bot\hspace{13ex}\neg\mathsf E~2,5\\~~7.~B(c)\hspace{11ex}\mathsf X~6}\\\fitch{~~8.~B(c)\hspace{11ex}\textsf{Assume}}{}\\~~9.~B(c)\hspace{14ex}\vee\mathsf E~3,4{-}7,8{-}8}}\right.\\10.~\forall x~B(x)\hspace{12ex}\forall\mathsf I~3{-}9\\11.~A\vee\forall x~B(x)\hspace{7ex}\vee\mathsf I~10\\12.~\bot\hspace{18ex}\neg\mathsf E~2,11}\\13.~\neg\neg (A\vee\forall x~B(x))\hspace{6ex}\neg\mathsf I~2{-}12\\14.~A\vee\forall x~B(x)\hspace{11ex}\neg\neg\mathsf E~13}$$