Working on P.D. Magnus. forallX: an Introduction to Formal Logic (pp. 297, exercise C. 4):
$
\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}
\fitch{}{
\fitch{\neg \exists x (A(x) \to \forall y(A(y))}{
\fitch{¬A(c)}{
\fitch{A(c)}{
\bot\\
\forall yA(y)\\
} \\
A(c) \to \forall yA(y)\\
\exists x (A(x) \to \forall y(A(y))\\
\bot\\
}\\
A(c)\\
\ldots\\
\bot
}\\
\exists x (A(x) \to \forall y(A(y))
}
$
Am I heading in the right direction? How can I fill the dots?
Best Answer
Your subproof has so far derived that for any $c$ that $A(c)$ (under its assumption).
Therefore you may derive $\forall y~(A(y))$ by universal introduction under the assumption of $A(b)$ and viola.
So you should just tuck your subproof inside an existential elimination subproof and tie things up with a nice bot.
Note: The statement $\exists x~(A(x)\to\forall y~A(y))$ will be vacuously false in an empty domain, so let us take existential import to be an unstated premise. [We can not prove an existential when no thing exists.]
$$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{\exists x~x=x\hspace{20ex}\text{[existential import: the domain is non-empty]}}{\fitch{\neg\exists x~(A(x)\to\forall y~A(y))}{\fitch{[b]~b=b}{\fitch{A(b)}{\fitch{[c]}{\color{blue}{{\fitch{\neg A(c)}{\fitch{A(c)}{\bot\\\forall y~A(y)}\\A(c)\to\forall y~A(y)\\\exists x~(A(x)\to\forall y~A(y))\\\bot}\\\neg\neg A(c)\\A(c)}}}\\\forall y~A(y)}\\A(b)\to\forall y~A(y)\\\exists x~(A(x)\to\forall y~A(y))\\\bot}\\\bot}\\\neg\neg\exists x~(A(x)\to\forall y~A(y))\\\exists x~(A(x)\to\forall y~A(y))} $$
It seems from the comments that P.D. Magnus book did not properly isolate local variables into their own contexts for use with its existential elimination and universal introduction rules.
Also Existential Import seems to be treated as a inference rule rather than a premise. [In an non-empty domain, if everything satisfies a predicate, then something satisfies that predicate, so therefore $\exists x~P(x)$ may be inferred from $\forall x~P(x)$, or something to that effect.]
$$ \fitch{}{\fitch{\neg\exists x~(A(x)\to\forall y~A(y))}{{\fitch{A(b)}{{\color{blue}{{\fitch{\neg A(c)}{\fitch{A(c)}{\bot\\\forall y~A(y)}\\A(c)\to\forall y~A(y)\\\exists x~(A(x)\to\forall y~A(y))\\\bot}\\\neg\neg A(c)\\A(c)}}}\\\forall y~A(y)}\\A(b)\to\forall y~A(y)\\\forall x~(A(x)\to\forall y~A(y))\\\exists x~(A(x)\to\forall y~A(y))}\\\bot}\\\neg\neg\exists x~(A(x)\to\forall y~A(y))\\\exists x~(A(x)\to\forall y~A(y))} $$