Working on P.D. Magnus. forallX: an Introduction to Formal Logic (pp. 297, exercise C. 5):
$
\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}
\def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\}
\def\R#1{\qquad\mathbf{R} \: #1 \\}
\def\ii#1{\qquad\mathbf{\to I} \: #1 \\}
\def\ne#1{\qquad\mathbf{\neg E} \: #1 \\}
$
$
\fitch{}{
\fitch{\color{blue} 1.\, \neg (\exists y A(y) \to A(c))}{
\fitch{\color{blue} 2.\, A(c)}{
\fitch{\color{blue} 3.\, \exists yA(y)}{
\color{blue} 4.\, A(c) \R{2}
}\\
\color{blue} 5.\, \exists yA(y) \to A(c) \ii{3-4}
\color{blue} 6.\, \bot \ne{1,5}
}\\
\ldots\\
\color{blue} k.\, \bot
}\\
\color{blue}{k+1}.\, \exists y A(y) \to A(c)\\
\color{blue}{k+2}.\, \exists x(\exists y A(y) \to A(x)) \\
}
$
Is this a good skeleton for this proof ? How can I derive last contradiction ?
Best Answer
Exploring your route gets you in a tangle where you need to quantify in an illegitimate way halfway through the proof.
Better, assume the negation of the desired conclusion and proceed ...
First let's just (in effect) use brute forcce! A standard proof strategy when you have a supposition of the form $\neg(\alpha \to \beta)$, is to suppose $\neg \alpha$, get a contradiction, proving $P$. OK, here there is an existential quantifier in the way between the negation and the conditional, but let's still try the same dodge, of assuming the negation of the antecedent of the internal conditional. Then let's do the pretty obvious thing at each stage.
$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{} {\fitch{\neg\exists x(\exists yAy \to Ax)} {\fitch{\neg\exists yAy}{\fitch{\exists yAy}{\bot\\ Ac}\\ (\exists yAy \to Ac)\\ \exists x(\exists yAy \to Ax)\\ \bot }\\ \neg\neg\exists yAy\\ \exists yAy\\ \fitch{Ac}{ \fitch{\exists yAy}{Ac}\\ (\exists yAy \to Ac)\\ \exists x(\exists yAy \to Ax)\\ \bot }\\ \bot }\\ \neg\neg\exists x(\exists yAy \to Ax)\\ \exists x(\exists yAy \to Ax) } $
Looking at that proof, though, and seeing the proof ideas involved, we can spot [as noted by the OP] that we can speed things up a bit by doing some things in the opposite order:
$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{} {\fitch{\neg\exists x(\exists yAy \to Ax)} {\fitch{\exists yAy} {\fitch{Ac} {\fitch{\exists y Ay}{Ac}\\ (\exists yAy \to Ac)\\ \exists x(\exists yAy \to Ax)\\ \bot }\\ \bot\\ Ac }\\ (\exists yAy \to Ac) \\ \exists x(\exists yAy \to Ax)\\ \bot }\\ \neg\neg\exists x(\exists yAy \to Ax)\\ \exists x(\exists yAy \to Ax) } $