Given ∃x.¬p(x), use the Fitch System to prove ¬∀x.p(x).
What I am thinking was I need two formulas,
AX.p(X) => something
AX.p(X) => ~ something
I guess something maybe is the p(x) and the other is ~p(x) since we was given EX.~p(x)..But actually it can't work for me. And I guess maybe is EX.~p(x) and ~EX.~p(x)..But if I am doing that then the it will go to deadend..so I give up..;(
Wish someone can help me.
For note about EE:
1: EX.p(X)
2: AX.(p(X) => something)
3: something EE1,2
But something cann't have the free variable from p..in this sample, then soemthing cannot including X..so if something is p(X) it cannot use EE, but if p(Y) then can use EE.
Here is my solution:
$1.~\exists X~\lnot p(X)\quad $ Premise
$2.~\quad \lnot p(c)\quad$ Existential Elimination:1, Witness Assumed: $[c]$
$3.~\qquad\forall X~p(X)\quad$ Assumption
$4.~\qquad p(c)\quad$ Universal Elimination:3
$5.~\quad \forall X~p(X) \implies p(c)\quad$ Implication Introduction 3-4
$6.~\qquad\forall X~p(X)\quad$ Assumption
$7.~\qquad\lnot p(c)\quad$ Reiteration:2
$8.~\quad\forall X p(X) \implies \lnot p(c)\quad$ Implication Introduction: 6-7
$9.~\quad\lnot \forall X~p(X)\quad$ Negation Introduction 5,8
$10.~\lnot \forall X~p(X)\quad$ Witness Eliminated 2-9
Given your EE rule, you need to prove $\forall x (\neg p(x) \rightarrow \neg \forall x \ P(x))$, which you do by a universal introduction on $\neg p(x) \rightarrow \forall x \ p(x)$, which on its turn you prove by a conditional Introduction on a subproof that assumes $\neg p(x)$ and derives $\neg \forall x \ p(x)$ .. and the latter you get by a proof by contradiction as you yourself surmised. So:
$\exists x \neg p(x)$ Premise
$\quad \neg p(x)$ Assumption
$\quad \quad \forall x \ p(x)$ Assumption
$\quad \quad p(x)$ $\forall$ Elim 3
$\quad \forall x \ p(x) \rightarrow p(x)$ $\rightarrow$ Intro 3-4
$\quad \quad \forall x \ p(x)$ Assumption
$\quad \quad \neg p(x)$ Reiteration 2
$\quad \forall x \ p(x) \rightarrow \neg p(x)$ $\rightarrow$ Intro 6-7
$\quad \neg \forall x \ p(x)$ $\neg$ Intro 5,8
$\neg p(x) \rightarrow \neg \forall x \ p(x)$ $\rightarrow$ Intro 2-9
$\forall x (\neg p(x) \rightarrow \neg \forall x \ p(x))$ $\forall$ Intro 10
$\neg \forall x \ p(x)$ $\exists$ Elim 1, 11