I am trying to figure out how ∃x∃yf xy -> ∃y∃xf xy is supposed to work, using natural deduction.
I know how to use the exist elimination rule, but I usually end up somewhere where I don't know how to continue.
Here's my best guess:
$\qquad\large\begin{array}{lclcr}1:&\{1\}&\exists x\exists y~Rxy&\hspace{20ex}&\mathsf A\\2:&\{2\}&Rab&&\mathsf A\\3:&\{2\}&\exists x~Rxb&&\exists\mathsf E(x/a)~2\\4:&\{\}&Rab\to\exists x~Rxb&&{\to}\mathsf E~2!,3\\5:&\{2\}&\exists x~Rxb&&\exists\mathsf B~3,4\\6:&\{2\}&\exists y\exists x~Rxy&&\exists\mathsf E(y/b)~5\end{array}$
Help would be greatly appreciated, got my exam tomorrow :)
Best regards, Sam!
Here is an outline natural deduction proof set out Fitch-style, indenting when new assumptions are made. Can you see where steps of existential quantifier introduction and elimination are being made?
$\exists x\exists yFxy\\ \quad | \quad\exists yFay\\ \quad | \quad | \quad Fab \\ \quad | \quad | \quad \exists xFxb \\ \quad | \quad | \quad \exists y\exists xFxy \\ \quad | \quad \exists y\exists xFxy \\ \exists y\exists xFxy \\ $
If you want more on existential quantifier rules, check out Ch 32 of An Intro to Formal Logic downloadable at https://www.logicmatters.net/ifl. This very proof is done on p. 311. If you are using a slightly different proof layout, the principles will be the same.