Natural deduction for predicate logic

Question

I'm trying to solve this problem:

((∀xFx)→¬(∀xPx))∧(¬(∀xPx)→(∀xFx))→∃x((Fx→¬Px)∧(¬Px→Fx))

I tried double negating the ∃x((Fx→¬Px)∧(¬Px→Fx)), but then I'm getting stuck on what to do next.

How would I solve it after the Implication Introduction?

Answer 1

I tried double negating the ∃x((Fx→¬Px)∧(¬Px→Fx)), but then I'm getting stuck on what to do next.

Basically $\forall x~Fx\leftrightarrow\lnot\forall x~Px$ entails that either (1) $\forall x~Fx$ holds and thus $\exists x~\lnot Px$, or else (2) $\forall x~Fx$ does not hold, and thus $\exists x~\lnot Fx$ and $\forall x~Px$, and we can therefore show either case $\exists x~(Fx\leftrightarrow\lnot Px)$ holds.

The full proof looks to be annoyingly long, but here is the skeleton.

$$\def\fitch#1#2{~~\begin{array}{|l} #1\\\hline #2\end{array}} \fitch{}{\fitch{(\forall x~Fx)\leftrightarrow(\lnot\forall x~Px)}{\fitch{\lnot\exists x~(Fx\leftrightarrow \lnot Px)}{\fitch{\forall x~Fx}{\lnot\forall x~Px\\~~\vdots\\\exists x~\lnot Px\\~~\vdots\\\exists x~(Fx\leftrightarrow\lnot Px)\\\bot}\\\lnot \forall x~Fx\\~~\vdots\\\forall x~Px\\~~\vdots\\\exists x~\lnot Fx\\~~\vdots\\\exists x~(Fx\leftrightarrow\lnot Px)\\\bot}\\\lnot\lnot \exists x~(Fx\leftrightarrow\lnot Px)\\\exists x~(Fx\leftrightarrow\lnot Px)}\\((\forall x~Fx)\leftrightarrow(\lnot\forall x~Px))\to\exists x~(Fx\leftrightarrow\lnot Px)}$$