The "Axiom of choice" in proof of Skolem from equisatisfiability theorem I do not understand the application of the "axiom of choice " in the proof of equisatisfiability of Skolem form.
Can you help show me the understandable format in this case ?
Here is the proof from wiki https://en.wikipedia.org/wiki/Skolem_normal_form in the part "Correctness of Skolemization may be shown on the example formula..."
Sorry about that I am using Chrome and can not just paste all the text here.
 A: Suppose I want to show that "$\forall x\exists yP(x, y)$" is equivalent to "$\exists F\forall x P(x, F(x))$". One direction (from right to left) is trivial; in the other direction, I use choice to define $F$ (for each $x$ I need to "choose" some appropriate $y$ to be $F(x)$, and if there are lots of $x$s and no easy way to describe appropriate $y$s, this is something I might need choice for). So the intuition should be that choice might be needed to show that the Skolem function exists.
And in fact this is correct, in the strongest possible way: the axiom of choice is Skolemization!
Clearly choice lets you Skolemize, so it's the other direction that's interesting. Suppose I have a family $\{A_i: i\in I\}$ of nonempty sets. The axiom of choice tells me that a choice function exists - that is, a map taking each $i\in I$ to some $a_i\in A_i$. 
Now let's think about those two sentences:


*

*Saying "each $A_i$ is nonempty" is just "For all $x$, there is some $y$ such that $y\in A_x$."

*But saying "there is a choice function" is just "There is some $f$ such that for all $x$, $f(x)\in A_x$."
The axiom of choice goes from the nonemptiness statement to the function statement - and this is exactly Skolemization.
A: Fix a structure $M$ of your language, now you can think about every formula with a single free variable as defining a subset of $M$.
The statement that $\exists x\varphi(x)$ means that the set defined by $\varphi$ is non-empty.
But now a Skolem function is a function symbol $F$ such that when we interpret the extended language we get $M\models\exists x\varphi(x)$, then $M\models\varphi(F^M(x))$.
This means that in effect, $F$ is a choice function from all the definable subsets of $M$. But the axiom of choice is certainly needed here!
If $\{A_i\mid i\in I\}$ is any family of non-empty sets, taking the language with predicate symbols $R_i$ for $i\in I$ and the theory $\exists x R_i(x)$, then the structure $M$ whose universe is $\bigcup\{A_i\mid i\in I\}$ and $R_i^M=A_i$ satisfies the theory. And of course, a Skolem function is by definition a choice function from the $A_i$'s.
