Relational Proofs with Fitch Systems

Question

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!

Answer 1

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:

1. $\forall x P(x)$ Premise

2. $\quad \exists x \neg P(x)$ Assumption

3. $\quad \quad \neg P(x)$ Assumption

4. $\quad \quad \quad \forall x P(x)$ Reiteration 1

5. $\quad \quad \quad \neg P(x)$ Reiteration 3

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

7. $\quad \quad \quad \forall x P(x)$ Assumption

8. $\quad \quad \quad P(x)$ $\forall \: E$ 7

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

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

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

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

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

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

15. $\quad \exists x \neg P(x)$ Assumption

16. $\forall x P(x)$ Reiteration 1

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

18. $\neg \exists x \neg P(x)$ $\neg \: I$ 14,17

Answer 2

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$.