An example showing that a Skolem normal form of $A$ can be not logically equivalent to $A.$ I am trying to learn a little about Mathematical Logic.
Precisely now I am reading about Prenex Normal Forms from E. Mendelson, Introduction to Mathematical Logic, 2nd Edition. I would like to know whether I have correctly worked out exercise 2.80 (which is Exercise 2.87 in the 4th Edition):  

Find a Skolem normal form $B$ for $\forall x\exists yA^2_1(x,y)$ and show that $\not\vdash B\leftrightarrow \forall x\exists yA^2_1(x,y).$

What is the context?


*

*Mendelson is working with a pure predicate calculus, i.e. a predicative calculus without individual constant nor function letters, such that for any positive integer $n$ there are infinitely $n$-ary predicate letters.


What I have done?


*

*I have applied the described algorithm to find a Skolem normal form, and I have found $B:=\exists x \exists y \forall z[(A_1^2(x,y)\to P(x))\to P(z)],$ where $P$ is a $1$-ary predicative variable. 

*By Goedel's completeness theorem, I have to show the $B\leftrightarrow \forall x\exists yA^2_1(x,y)$ is not universally valid, i.e. I have to find an interpretation $\mathfrak{A}$ s.t. $\mathfrak A\not\models B\leftrightarrow \forall x\exists yA^2_1(x,y).$

*I have considered the interpretation, with domain $\mathbb N,$ which assigns to $A_1^2(x,y)$ the relation $x>y,$ and to $P(x)$ the relation "x=1".
If I am not wrong then, for any $s\in\mathbb{N}^\omega,$ I have $\mathfrak A\not\models\forall x\exists y A_1^2(x,y)[s]$ while $\mathfrak A\models B[s].$


As obvious, any feedbak is highly appreciated.
 A: It looks alright to me.
Note that a simpler counterexample interpretation would be to make $P({\cdot})$ always true and $A_1^2({\cdot},{\cdot})$ always false.
A: I think there's a simpler example, that doesn't make reference to the example in Mendelson - I hope somebody can confirm this. Consider this formula interpreted wrt. the theory of the Natural numbers ($T_{\mathbb{N}}$)
$T_{\mathbb{N}}\vdash \exists y\forall x. x >= y$
is valid. However, the Skolem equivalent 
$T_{\mathbb{N}}\cup{\{f\}}\vdash\forall x. x >= f$
which is interpreted wrt. the the theory of the naturals plus the constant $f$ is not a valid statement since it does not hold for every possible assignment of $f$ to a nat. In general, validating a Skolemized formula has to consider many more interpretations b/c of the additional Skolem functions (or constant in this case)
A: The example of S.N. is not correct in my opinion since it states the rule to be:
There exist a $y$ so that $y$ is larger than any $x$, that is not correct in $T_n$ nor what he wanted to represent.
The correct representation is $\forall x\exists y \cdot x\ge y$, that is: for every x there is a larger or equal $y$.
If you get to the "Skolemized" normal form you get not a constant anymore for $y$ but a function of the $x$ you are considering; like that: $x\ge g(x)$. 
The above expression holds for any function $g(x)$ mapping $x$ to an equal or greater value than $x$; like $g(x)=x+1$.
