Relational Proofs with Fitch Systems I need to prove:
$\forall x.p(x) \Rightarrow \neg \exists x.\neg p(x)$
I know I probably have to assume $\exists x.\neg p(x)$ to reach a contradiction. However, I am not quite sure about how to reach the contradiction.
The premise is that $\forall x.p(x)$, so maybe I had to prove $\exists x.\neg p(x) \Rightarrow \neg \forall x.p(x)$ in this case. However, to get $\neg \forall x.p(x)$ required assuming $\forall x.p(x)$ in advance, which is the same as the premise. Is it feasible? Whether such scenario would cause a endless loop?
I am not sure how could I get a contradiction for this case, any help would be appreciated, thanks!  
 A: Different systems define the Existential Elimination (or Existential Instantiation) differently, but here is a proof in the Fitch system I use:

EDIT
OK, so your system is indeed a good bit different from the one I use above.  Here is a proof in your system:


*

*$\forall x P(x)$ Premise

*$\quad \exists x \neg P(x)$ Assumption

*$\quad \quad \neg P(x)$ Assumption

*$\quad \quad \quad \forall x P(x)$ Reiteration 1

*$\quad \quad \quad \neg P(x)$ Reiteration 3

*$\quad \quad \forall x P(x) \rightarrow \neg P(x)$ $\rightarrow \: I$ 4-5

*$\quad \quad \quad \forall x P(x)$ Assumption

*$\quad \quad \quad P(x)$ $\forall \: E$ 7

*$\quad \quad \forall x P(x) \rightarrow P(x)$ $\rightarrow \: I$ 7-8

*$\quad \quad \neg \forall x P(x)$ $\neg \: I$ 6,9

*$\quad \neg P(x) \rightarrow \neg \forall x P(x)$ $\rightarrow \: I$ 3-10

*$\quad \forall x (\neg P(x) \rightarrow \neg \forall x P(x))$ $\forall \: I$ 11

*$\quad \neg \forall x P(x)$ $\exists \: E$ 2,12

*$\exists x \neg P(x) \rightarrow \neg \forall x P(x)$ $\rightarrow \: I$ 2-13

*$\quad \exists x \neg P(x)$ Assumption

*$\forall x P(x)$ Reiteration 1

*$\exists x \neg P(x) \rightarrow \forall x P(x)$ $\rightarrow \: I$ 15-16

*$\neg \exists x \neg P(x)$ $\neg \: I$ 14,17
A: I may be misunderstanding the question, but it seems like the contradiction follows almost directly from supposing the negation of the conclusion. By negating the conclusion, we have $\exists x$ such that $\neg p(x)$, call it $x_0$. So, by using that particular $x_0$ we have a contradiction to the premise that $p(x)$ for any $x$.
