I am given the following expression: ∀x∃y R(x, y) ⊢ ∃y∀x R(x, y) and I have attempted solving it as:
∀x∃y R(x,y) premise
| ∀x R(x,y0) assumption
| | x0
| | R(x0,y0) ∀xe 2
| ∀x R(x,y0) ∀xi 4
| ∃y∀x R(x,y) ∃yi 5
∃y∀x R(x,y) ∃ye 1, 2--5
My concern is the first assumption, and therefore the use of the ∃y-elimination rule. Is this a valid approach?
No, you have to apply the rules for the outermost operator first. Logically, you are saying that there is one $y_0$ satisfying $R(x,y_0)$ for all $x$ which is a wrong deduction.