Vrftsjtryk

How to show $(exists x)( forall y)varphirightarrow( forall y)(exists x)varphi $ is logically valid

Here is my attempt:

Assume it's not logically valid. Then, there's an interpretation $mathscr{M}$ for which it's not true. Hence, there's a sequence $vec a$ in the domain $M$ of $mathscr{M}$ such that 1) $ vec a$ satisfies $(exists x)( forall y)varphi$ and 2) $vec a$ doesn't satisfy $( forall y)(exists x)varphi$

1) $vec a$ satisfies $(exists x)( forall y)varphi$ $iff$ $vec a$ doesn't satisfy $(forall x)( exists y)negvarphi$ $iff$ $vec a$ doesn't satisfy $( exists y)negvarphi$ $iff$ $vec a$ satisfies $( forall y)varphi$ $iff$ $vec a$ satisfies $varphi$

2) $vec a$ doesn't satisfy $( forall y)(exists x)varphi$ $iff$ $vec a$ doesn't satisfy $(exists x)varphi$ $iff$ $vec a$ satisfies $(forall x)negvarphi$ $iff$ $vec a$ satisfies $negvarphi$

Since $vec a$ satisfies both $varphi$ and $negvarphi$, which is a contradiction, then the formula must be valid.

Is it correct to show it this way?

Edit:
1) If $vec a$ satisfies $(exists x)( forall y)varphi$, i.e $neg forall x(negforall y(varphi))$, then we have $vec a$ does not satisfy $forall x(negforall y(varphi))$ . Then, there is at least one sequence $vec a'$ differing from $vec a$ in at most the ith component not satisfying $negforall y(varphi)$. Then, that means $vec a'$ satisfies $( forall y)varphi$.
2) If $vec a$ doesn't satisfy $( forall y)(exists x)varphi$, i.e $( forall y)neg(forall x)(negvarphi)$, then there is at least one sequence $vec a''$ differing from $vec a$ in at most the jth component not satisfying $neg(forall x)(negvarphi)$. Then, that means $vec a''$ satisfies $(forall x)negvarphi$.

Now, we have $vec a'$ satisfies $( forall y)varphi$ and $vec a''$ satisfies $(forall x)negvarphi$. Then, there is at least one sequence $vec a'''$ differing from $vec a$ in at most the $i$th and $j$th component satisfying $varphi$ and satisfying $negvarphi$, which is a contradiction, then the formula must be valid.

This is from the book, so I applied what's written in $2$ actually

You're forgetting to use from item 4 the part that says the sequence differs in at most the $i$th component.

For instance, say you have a sequence $a$ satisfying a formula $psi = exists xforall y(varphi)$. Mendelson uses only the universal quantifier, then, actually, the above rendering of $psi$ is only syntactic sugar for $neg forall x(negforall y(varphi))$.

For a sequence $a$ to satisfy $psi$, it means that, by item 2, $a$ does not satisfy $forall x(negforall y(varphi))$.

For $a$ to not satifsy $forall x(negforall y(varphi))$, by item 4, it means that there is at least one sequence $a'$ differing from $a$ in at most the $i$th component (in wich $i$ is the index of the variable $x$) not satisfying $negforall y(varphi)$.

As for your edit, what you can get is actually

1. A sequence $a'$ differing from $a$ in at most the $i$th position ($i$ being the index of $x$) satisfying $forall y (varphi)$.


2. A sequence $a''$ differing from $a$ in at most the $j$th position ($j$ being the index of $y$) satisfying $forall x(negvarphi)$.

for $x$ and $y$ can be different variables.

To obtain a contradiction from this you can use item 4 (from Mendelson) to obtain another sequence, say $a'''$, differing from $a$ in at most the $i$th and $j$th position that will work for both 1. and 2. above.