Proving $A \to \exists x B(x) \therefore \exists x(A \to B(x))$

logicnatural-deduction

Working on P.D. Magnus. forallX: an Introduction to Formal Logic (pp. 297, exercise C. 2), appears the following exercise:

$
\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}
\fitch{A \to \exists x B(x)}{
\fitch{\neg \exists x(A \to B(x))}{
\fitch{A}{
\exists xB(x)\\
\fitch{B(c)}{
\ldots
}
}
}
}
$

The next step would be to use Repetition rule in order to derive $B(c)$ but that move is forbidden since $c$ appears in an undischarged assumptions. How can I continue the proof?

Best Answer

I gave a proof here ... but the OP's eventual version at the end of the comments below is snappier and to be preferred!!

Related Solutions

Proving $A \to (B \vee C) \therefore (A \to B) \vee (A \to C)$

$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}$ Remark: Your subproof is somewhat convoluted. Compare: $$\fitch B{\fitch{\neg (A\to B)}{\fitch AB\\A\to B\\\bot}\\\neg\neg(A\to B)\\A\to B\\(A\to B)\vee(A\to C)}\qquad\raise{7.25ex}{\fitch B{\fitch AB\\A\to B\\(A\to B)\vee(A\to C)}}$$

There are two ways to derive a disjunction.

constructively derive one of the disjuncts, or
use an indirrect proof (reduce the negation to absurdity).

You are having trouble doing (1), therefore you should attempt an indirect proof.

Assume $\neg((A\to B)\vee(A\to C))$ and place your proof inside this context.

$$\fitch{~~1.~A\to(B\vee C)}{\fitch{~~2.~\neg((A\to B)\vee(A\to C))}{\fitch{~~3.~A}{~~4.~B\vee C\hspace{20ex}\textsf{Conj.Elim 3,1}\\\fitch{~~5.~B}{\fitch{~~6.~A}{~~7.~B\hspace{20ex}\textsf{Reiteration 5}}\\~~8.~A\to B\hspace{17ex}\textsf{Conj.Intro. 6-7}\\~~9.~(A\to B)\vee (A\to C)\hspace{4ex}\textsf{Disj.Intro. 8}\\10.~\bot\hspace{22.5ex}\textsf{Neg.Elim. 9,2}\\11.~C\hspace{22.5ex}\textsf{Explosion 10}}\\\fitch {12.~C}{}\\13.~C\hspace{25ex}\textsf{Disj.Elim. 4,5-11,12-12}}\\14.~A\to C\hspace{22ex}\textsf{Conj.Intro 3-13}\\15.~(A\to B)\vee(A\to C)\hspace{9ex}\textsf{Disj.Intro 14}\\16.~\bot\hspace{27.5ex}\textsf{Neg.Elim. 2,15}}\\17.~\neg\neg((A\to B)\vee(A\to C))\hspace{6.5ex}\textsf{Neg.Intro. 2-16}\\18.~(A\to B)\vee(A\to C)\hspace{11.5ex}\textsf{Double Neg.Elim. 17}}$$

Using $\exists$ Elimination rule to prove an argument (Fitch-style)

$a$ does not occur in any undischarged assumption, but in $\mathcal{B} : Ha \land \neg Fa$, which is also not allowed according to the $\exists E$ rule specification.
So at the point where you leave the subproof and do an existential elimination, $a$ must already have been converted into a bound variable.

The solution is to prepone the $\exists I$ on line 10 to inside the subproof to get a conclusion in which $a$ no longer occurs, and then apply $\exists E$ on that existential conclusion as the very last step:

...
 8 | | Ha ^ Fa       ^I, 4,7
 9 | | ∃x(Hx ^ Fx)   ∃I, 8
10 | ∃x(Hx ^ Fx)     ∃E, 2,3-9

As a rule of thumb, it often is the case that $\exists E$ is (or can be made) the last step in a natural deduction proof.

Best Answer

Related Solutions

Proving $A \to (B \vee C) \therefore (A \to B) \vee (A \to C)$

Using $\exists$ Elimination rule to prove an argument (Fitch-style)

Related Question