I want to build a proof for $\vdash \exists y \forall P(x,y) \rightarrow \forall x \exists y P(x,y)$ using the software Fitch...
I have the above proof and I want to test it to be sure I have done that right, however I cannot prove anything in such software as I cannot even get started since I do not have any premises for the sequent...
Edit
That's everything I have so far... Could some of you help me validate if the proof tree is true and help me build such a proof in the Fitch?
Edit 2
$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}$ In Fitch systems, the existential elimination rule references an existential statement, and a subproof, whose assumption is a witness for that statement, that concludes with a statement that does not contain the witness variable.$$\boxed{~~a.~~\exists x~\phi\\\fitch{~~b.~~\boxed\alpha ~\phi[x\backslash\alpha]}{~~~~\vdots\\~~c.~~\psi}\\~~d.~~\psi\qquad\exists \mathsf E~a,b{-}c}$$
Thus you are looking to build $$\fitch{}{\fitch{~~1.~~\exists y~\forall x~P(x,y)}{\fitch{~~2.~~\boxed a~\forall x~P(x,a)}{\quad\vdots\\~~\mathrm m.~~\forall x~\exists y~P(x,y)}\\~~\mathrm n.~~\forall x~\exists y~P(x,y)\hspace{18ex}\exists\mathsf E~1,2{-}\mathrm m}\\~~\mathrm o.~~\exists y~\forall x~P(x,y)\to\forall x~\exists y~P(x,y)\qquad{\to}\mathrm I~1{-}\mathrm n}$$
Note: Line 2 is an assumption, with fresh variable $a$.