Given $∃y.∀x.p(x,y)$, use the Fitch system to prove $∀x.∃y.p(x,y)$

Question

Given $\exists y. \forall x. p(x,y)$, use Fitch-style natural deduction system to prove $\forall x.\exists y.p(x,y)$.

I know this question has been asked before, but based on that answer I'm not able to move forward from step 3 below. I'm using Stanford's platform as a proof assistant by the way, maybe that's the issue. Any help is very much appreciated.

1.  EY:AX:p(X,Y)     Premise
2.  AX:p(X,Y).       Assumption
3.  p(X,Y).          Universal Elimination: 2

Answer 1

I guess Stanford's platform you use is this one (in my opinion, not the best proof assistant in Fitch-style natural deduction).

In such a system, the elimination rule for the existential quantifier is a little unusual, since it uses Skolem terms (see here for an explanation), so there is no need for a further assumption.

The correct formalization of a proof of $\forall x \exists y \, p(x,y)$ from $\exists y \forall x \, p(x,y)$ in Stanford's platform is the following:

By the way, your approach is essentially correct if you use a more standard Fitch-style natural deduction system, such as the one implemented by this proof assistant (which, in my opinion, is very intuitive to use). As @Bram28 said in his comment (and this is the reason why, in my opinion, your question is not a duplicate of that one),

different systems may have different formalizations, even if the rules are called the same.

In such a "more standard" Fitch-style system, the correct formalization of a proof of $\forall x \exists y \, p(x,y)$ from $\exists y \forall x \, p(x,y)$ is essentially the continuation of your attempt:

$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall \, Elim}: #1 \\} \def\Ai#1{\qquad\mathbf{\forall \, Intro}: #1 \\} \def\Ee#1{\qquad\mathbf{\exists \, Elim}: #1 \\} \def\Ei#1{\qquad\mathbf{\exists \, Intro}: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=Intro}\\} \def\qe#1{\qquad\mathbf{=Elim} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg Elim} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg Intro} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\} $ $ \fitch{1.\, \exists y \forall x \,P(x,y)}{ \fitch{2.\, \forall x \, P(x,b)}{ 3.\, P(a,b) \Ae{2} 4.\, \exists y \, P(a,y) \Ei{3} 5.\, \forall x \exists y \, P(x,y) \Ai{4} }\\ 6.\, \forall x \exists y \, P(x,y) \Ee{1, 2{-}5} } $