Given $\exists x.\lnot p(x)$, use the Fitch System to prove $\lnot \forall x.p(x)$

Question

This is what I've come up with so far, but I'm stuck at step 11:

\begin{align} &(1)\quad \exists x.\lnot p(x) & \text{Premise}\\ &(2)\quad \lnot p(x) & \text{Assumption}\\ & (3)\quad \forall x.p(x) &\text{Assumption}\\ &(4)\quad p(x) & \text{Universal Elimination: 3}\\ & (5)\quad \forall x.p(x)\rightarrow p(x) & \text{Implication Introduction: 3, 4}\\ & (6)\quad \forall x.p(x) & \text{Assumption}\\ & (7)\quad \lnot p(x) & \text{Reiteration: 2}\\ & (8) \quad \forall x.p(x) \rightarrow \lnot p(x) & \text{Implication Introduction: 6, 7}\\ & (9) \quad \lnot \forall x.p(x) & \text{Negation Introduction: 5, 8}\\ & (10) \quad \lnot p(x) \rightarrow \lnot \forall x.p(x) & \text{Implication Introduction: 2, 9}\\ & (11) \quad \forall x.(\lnot p(x) \rightarrow \lnot \forall x.p(x)) & \text{Universal Introduction: 10} \end{align}

I figured Existential Elimination would be step 12, but all I get is $\lnot p([c6])$.

Any help? Thank you.

Answer 1

Hint:

$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}$ Try proof by contradiction, work backward that we will need $$\fitch{1.\exists x(\neg P(x))}{\fitch{2.~\forall x(P(x))}{3.\\4.\\5.\\6.~\bot\hspace{20ex}\text{???}}\\7.\neg\forall x(P(x))\hspace{15ex}\text{$\neg$ Intro}~2-6}$$ Observe that from assumption we have $\exists x(\neg P(x))$, clearly will contradict with $\forall x(P(x))$.

Answer:

$$\fitch{1.\exists x(\neg P(x))}{\fitch{2.~\forall x(P(x))}{\fitch{3.~\boxed{a}~\neg P(a)}{4.~P(a)\hspace{13.5ex}\forall\text{ Elim}~2\\5.~\bot\hspace{16ex}\bot\text{ Intro}~3,4}\\6.~\bot\hspace{20ex}\text{$\exists$ Elim }1,3-5 }\\7.\neg\forall x(P(x))\hspace{15ex}\text{$\neg$ Intro}~2-6}$$

Update: