Prove $\forall x(A \vee B(x)) \therefore A \vee \forall xB(x)$.

Question

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 ?

Answer 1

$\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}$$

Answer 2

You might try to prove the contrapositive along these lines (using a form of natural deduction that does not assume a non-empty universe):