# Give a deduction showing that ∃x∀yRxy syntactically implies ∀y∃xRxy

I know it's true but I have no idea how to write the deduction as there is no ∃ elimination rule that I know of. Am I supposed to use some kind of substitution?

• Like you say, you need rules ... are you working with a specific proof system? May 13 at 19:42
• @Bram28 I don't think so. The rules are in pages 137-138 of this book: mileti.math.grinnell.edu/MathematicalLogic.pdf May 13 at 19:53
• Oh! So the rules are right there: two Existential rules and two Universal rules… you’ll probably need all 4 May 13 at 20:24
• How am I supposed to remove the ∃x though? May 13 at 21:46
• Follow the rule of $\exists\mathsf P$.$$\dfrac{\mathcal S, \varphi^c_x\vdash \psi}{\mathcal S, \exists x~\varphi\vdash \psi}{\small\text{ where c is not free in \mathcal S, \exists x~\varphi, \psi and is a valid substituent for x in \varphi}}$$ So $\small\dfrac{\dfrac{\ddots}{\forall y~Rcy\vdash \forall y~\exists x~Rxy}}{\exists x~\forall y~Rxy\vdash \forall y~\exists x~Rxy}{(\exists\mathsf P)}$ May 14 at 3:32

$$\dfrac{\mathcal S, \varphi^c_x\vdash \psi}{\mathcal S, \exists x~\varphi\vdash \psi}{(\exists P)}{\small\text{ where c is not free in \mathcal S, \exists x~\varphi, \psi and is a valid substituent for x in \varphi}}$$
$$\dfrac{\dfrac{\vdots}{~~~~~~\forall y~Rcy\vdash \forall y~\exists x~Rxy}}{\exists x~\forall y~Rxy\vdash \forall y~\exists x~Rxy}{(\exists\mathsf P)}$$