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

Question

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?

Answer 1

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

Answer 2

One very nice feature of natural deduction is that the quantifier rules are just generalizations of the propositional rules. For example, $$\begin{array} {c} \dfrac{A \lor B,~ A \to X,~ B \to X}{X} \\ \\ \text{ Generalizes to } \\ \\ \dfrac{A_0 \lor A_1 \lor A_2 \cdots,~ A_0 \to X,~ A_1 \to X,~ A_2 \to X,~ \cdots}{X} \\ \\ \text{ Generalizes to } \\ \\ \dfrac {\exists x . Ax,~ A_k \to X}{X} \\ \end{array}$$

And this is useful, because to get an idea how to prove $A \to \exists x . Bx \vdash \exists x . (A \to Bx)$, first prove $A \to (B_0 \lor B_1) \vdash (A \to B_0) \lor (A \to B_1)$, then generalize everything to quantifiers.

And you should be able to prove every true boolean tautology methodically, algorithmically, no intuition required. This is what completeness proofs are for. Just do a separate case for all $2^n$ possible variable assignments and combine them all with or-elimination:

$$\boxed{\begin{array} {ll} A \to (B_0 \lor B_1) \\ A \lor \lnot A & \text{Law of excluded middle} \\ B_0 \lor \lnot B_0 \\ B_1 \lor \lnot B_1 \\ \\ \text{(Here we have 8 "cases" of variables to do or-elimation on)} \\ \\ \text{First the cases where B_0 asserted} \\ \quad ?A \land B_0 \land ?B_1 & \text{Assumption} \\ \quad B_0 & \land \text{ elimination } \\ \quad A \to B_0 & \text { Weakening } \\ \quad (A \to B_0) \lor (A \to B_1) \\ \\ \text{The cases where B_1 are asserted is handled similarly} \\ \\ \text{Then remaining cases where A holds and B doesn't:} \\ \quad A \land \lnot B_0 \land \lnot B_1 & \text{Assumption} \\ \quad A & \text{And elimination} \\ \quad B_0 \lor B_1 & \text{From theorem's assumption} \\ \\ \quad \quad B_0 & \text{Assumption} \\ \quad \quad (A \to B_0) \lor (A \to B_1) & \text{By contradiction} \\ \\ \quad \quad B_1 & \text{Assumption} \\ \quad \quad (A \to B_0) \lor (A \to B_1) & \text{By contradiction} \\ \\ \quad (A \to B_0) \lor (A \to B_1) & \lor \text{ Elimination} \\ \\ \text{The final case where all variables are false:} \\ \quad \lnot A \land \lnot B_0 \land \lnot B_1 \\ \quad \quad A & \text {Assumption} \\ \quad \quad B_0 & \text {By contradiction} \\ \quad A \to B_0 \\ \quad (A \to B_0) \lor (A \to B_1) & \lor \text { introduction} \\ \\ \text{Put all the cases together:} \\ (A \to B_0) \lor (A \to B_1) & \text{Several } \lor \text{ eliminations } \end{array}}$$

So just generalize that proof to quantifiers:

$$\boxed{\begin{array} {ll} A \to \exists x . Bx \\ A \lor \lnot A & \text{Law of excluded middle} \\ \exists x . Bx \lor \lnot \exists x . Bx \\ \\ \quad \exists x . Bx & \text{Assumption} \\ \quad \quad Bc & \text{ Assumption } \\ \quad \quad A \to Bc & \text { Weakening } \\ \quad \quad \exists x . A \to Bx \\ \quad \exists x . A \to Bx & \exists \text{ elimination }\\ \\ \quad A \land \lnot \exists x . Bx & \text{Assumption} \\ \quad A & \land \text{ elimination} \\ \quad \exists x . Bx & \text{From theorem's assumption} \\ \quad \exists x. A \to Bx & \text{ from contradiction } \\ \\ \quad \lnot A \land \lnot \exists x.Bx \\ \quad \quad A & \text {Assumption} \\ \quad \quad Bx & \text {By contradiction} \\ \quad A \to Bx \\ \quad \exists x . A \to Bx & \exists \text { introduction} \\ \\ \exists x . (A \to Bx) & \text{A few } \lor \text{ and } \exists \text{ eliminations } \end{array}}$$

Anyway the point I'm trying to get across is you can often solve predicate logic problems just by solving the specific propositional logic problem and then generalizing the inferences. It is a very nice feature of natural deduction.

Answer 3

Using another form of natural deduction that does not assume a non-empty universe. A proof by cases, the free variable $x$ is explicitly introduced on line 1.