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

Question

I've tried to solve this exercise based on a similar question that was asked some years ago, but I'm stuck in step 5. Any help? Thanks in advance. By the way I'm using Stanford's system.

1.  AX:p(X)            Premise
2.  ~p(X)              Assumption
3.  EX:p(X)            Assumption
4.  ~p(X)              Reiteration: 2
5.  EX:p(X) => ~p(X)   Implication Introduction: 3, 4

Answer 1

The idea is that you assume $\exists x \,\lnot P(x)$ and show that it leads to a contradiction with the premise $\forall x \, P(x)$, by means of the rules for the elimination of existential and universal quantifiers. This means that the negation of the assumption $\exists x \,\lnot P(x)$ holds.

This intuition is a little watered-down in Stanford's platform because its rules for negation introduction and existential elimination are slightly clumsy and unusual for natural deduction.

Anyway, the correct formalization of a proof of $\lnot \exists x \, \lnot P(x)$ from $\forall x \, P(x)$ in the Fitch-style natural deduction system implemented by Stanford's platform is the following: