[proofplan] We prove both implications directly from the semantics of the quantifier prefix. Starting from a model of the original prenex sentence, we choose witnesses for each existential quantifier as functions of the preceding universal variables and interpret the new Skolem symbols by those witness functions. Conversely, a model of the Skolemized universal sentence already contains interpretations of the Skolem functions, and these interpretations provide witnesses for the existential quantifiers when the original prefix is evaluated in the reduct to $L$. [/proofplan] [step:Expand a model of the original sentence by choosing Skolem witnesses] Assume that $\mathcal{M}$ is an $L$-structure satisfying $\varphi$. Let $M$ denote the underlying set of $\mathcal{M}$. For each existential index $i$, let \begin{align*} u_i=(x_{j_1},\dots,x_{j_m}) \end{align*} be the ordered tuple of all variables $x_j$ with $j<i$ and $Q_j=\forall$. We define a function \begin{align*} F_i:M^m &\to M \end{align*} as follows. The induction invariant is this: after the functions $F_k$ have been defined for all existential indices $k<i$, then for every assignment of elements of $M$ to the universal variables preceding $x_i$, with each earlier existential variable $x_k$ interpreted as $F_k$ evaluated on its preceding universal variables, the remaining suffix of the original prefix is satisfiable. This invariant holds initially because $\mathcal{M}\models \varphi$. Fix a tuple $a\in M^m$ of values for the variables in $u_i$, together with any values already fixed for earlier universal variables. Because the induction invariant holds at stage $i$, the semantic evaluation of the prefix \begin{align*} Q_1x_1\cdots Q_nx_n\,\theta \end{align*} guarantees that, whenever the previous existential variables have been chosen according to the earlier functions $F_k$ with $k<i$, the set \begin{align*} W_i(a) := \{b\in M : \text{the remaining suffix after }x_i\text{ is satisfiable when }x_i=b\} \end{align*} is nonempty. The family $(W_i(a))_{a\in M^m}$ is therefore an indexed family of nonempty subsets of $M$. Using choice, select one element $b_a\in W_i(a)$ for each $a\in M^m$, and define $F_i(a):=b_a$. By the definition of $W_i(a)$, this selected value preserves truth of the remaining suffix after $x_i$. This recursive construction is well-defined from left to right through the prefix: at stage $i$, all earlier Skolem functions have already been defined, and the induction invariant supplies a witness for the current existential quantifier after the preceding universal values are fixed. The invariant is preserved after defining $F_i$ because $F_i(a)$ was chosen from $W_i(a)$ for each tuple $a$. If the next existential quantifier occurs only after further universal quantifiers, the same invariant remains valid after those universal variables are assigned arbitrary elements of $M$, since satisfiability of the intervening universally quantified part means satisfiability for every such assignment. Now define an $L^{\mathrm{Sk}}$-expansion $\mathcal{M}^{\mathrm{Sk}}$ of $\mathcal{M}$ by interpreting each new function symbol $f_i$ as $F_i$. We claim that $\mathcal{M}^{\mathrm{Sk}}\models \varphi^{\mathrm{Sk}}$. Let an arbitrary assignment of elements of $M$ be given for all universally quantified variables of the original prefix. Evaluate every Skolem term $f_i(u_i)$ in $\mathcal{M}^{\mathrm{Sk}}$ using the corresponding tuple of preceding universal values. By construction, this value is exactly the witness chosen for the existential variable $x_i$ at that stage of the prefix. Therefore the resulting assignment of values to all variables $x_1,\dots,x_n$ satisfies the quantifier-free matrix $\theta$ in $\mathcal{M}$. Since the universal assignment was arbitrary, the universal closure $\varphi^{\mathrm{Sk}}$ is true in $\mathcal{M}^{\mathrm{Sk}}$. [guided] Assume that $\mathcal{M}$ is an $L$-structure with $\mathcal{M}\models\varphi$, and let $M$ be its underlying set. We must define interpretations for the new Skolem symbols. The guiding principle is that an existential quantifier in a prenex formula may choose its witness after seeing all earlier universal variables, but before seeing later universal variables. Therefore the corresponding Skolem function is allowed to depend exactly on the earlier universal variables. Fix an existential quantifier $Q_i x_i=\exists x_i$. Let \begin{align*} u_i=(x_{j_1},\dots,x_{j_m}) \end{align*} be the ordered tuple of universal variables that occur before $x_i$ in the prefix. We need to define a map \begin{align*} F_i:M^m &\to M. \end{align*} The precise invariant is that, once the earlier functions $F_k$ have been defined, every assignment of elements of $M$ to the universal variables preceding $x_i$ leaves the remaining suffix satisfiable when each earlier existential variable $x_k$ is interpreted by the value prescribed by $F_k$. This invariant is exactly the semantic content of $\mathcal{M}\models\varphi$ propagated left to right through the prefix. Take any tuple $a=(a_1,\dots,a_m)\in M^m$ of possible values for these preceding universal variables. The earlier existential variables have already been assigned by the previously constructed Skolem functions. Since $\mathcal{M}\models\varphi$ and the invariant holds at this stage, the semantics of the original prefix says that, after the preceding universal choices have been made and the earlier existential witnesses have been fixed, the witness set \begin{align*} W_i(a) := \{b\in M : \text{the remaining suffix after }x_i\text{ is satisfiable when }x_i=b\} \end{align*} is nonempty. We use choice for the family $(W_i(a))_{a\in M^m}$ of nonempty subsets of $M$: choose $b_a\in W_i(a)$ for each $a\in M^m$, and define $F_i(a_1,\dots,a_m):=b_a$. The condition $b_a\in W_i(a)$ is exactly what ensures that the selected value preserves truth of the remaining suffix of the formula. Proceeding from left to right through the prefix defines every $F_i$. The construction is legitimate because each existential stage uses only information that occurs earlier in the prefix: preceding universal values and earlier existential choices, the latter already being determined by earlier Skolem functions. After $F_i$ is defined, the invariant is preserved for the next stage because the selected value lies in the appropriate witness set. If some universal quantifiers intervene before the next existential quantifier, they cause no additional difficulty: those variables are assigned arbitrary elements of $M$, and the invariant continues to hold because the original universal quantifiers require the remaining suffix to be satisfiable for every such assignment. Now expand $\mathcal{M}$ to an $L^{\mathrm{Sk}}$-structure $\mathcal{M}^{\mathrm{Sk}}$ by interpreting each new symbol $f_i$ as the corresponding function $F_i$. To prove $\mathcal{M}^{\mathrm{Sk}}\models\varphi^{\mathrm{Sk}}$, take an arbitrary assignment of elements of $M$ to all variables that remain universally quantified in $\varphi^{\mathrm{Sk}}$. Each Skolem term $f_i(u_i)$ then evaluates to the witness chosen by $F_i$ for the existential variable $x_i$ under precisely those preceding universal values. Hence, after replacing every existential variable by its Skolem term, the quantifier-free matrix $\theta$ is true in $\mathcal{M}^{\mathrm{Sk}}$. Because the assignment of the universal variables was arbitrary, the universal sentence $\varphi^{\mathrm{Sk}}$ is satisfied. [/guided] [/step] [step:Recover witnesses for the original existential quantifiers from a Skolem model] Conversely, assume that $\mathcal{N}$ is an $L^{\mathrm{Sk}}$-structure satisfying $\varphi^{\mathrm{Sk}}$. Let $\mathcal{N}|_L$ be the reduct of $\mathcal{N}$ to the original language $L$, and let $N$ be the underlying set. We prove that $\mathcal{N}|_L\models\varphi$. Evaluate the original quantifier prefix from left to right. Whenever a universal quantifier $\forall x_i$ is encountered, let its value be an arbitrary element of $N$. Whenever an existential quantifier $\exists x_i$ is encountered, let $u_i=(x_{j_1},\dots,x_{j_m})$ be the tuple of preceding universal variables, and choose the value of $x_i$ to be the interpretation in $\mathcal{N}$ of the Skolem term \begin{align*} f_i(u_i). \end{align*} This choice is an element of $N$ because $f_i^{\mathcal{N}}:N^m\to N$ is a function in the structure $\mathcal{N}$. With these choices, the assignment produced for the variables $x_1,\dots,x_n$ is exactly the assignment obtained when the Skolemized matrix is evaluated under the chosen universal values. Since $\mathcal{N}\models\varphi^{\mathrm{Sk}}$, that matrix is true for every assignment of the universal variables. Therefore the quantifier-free formula $\theta$ is true in the reduct $\mathcal{N}|_L$ under the corresponding assignment of all original variables. This verifies the existential requirements in the original prefix, so $\mathcal{N}|_L\models\varphi$. [guided] Assume that $\mathcal{N}$ is an $L^{\mathrm{Sk}}$-structure satisfying the Skolemized universal sentence $\varphi^{\mathrm{Sk}}$. We must show that the original $L$-sentence $\varphi$ is true after forgetting the added Skolem symbols. Let $\mathcal{N}|_L$ denote this reduct, and let $N$ be its underlying set. Consider the original prefix \begin{align*} Q_1x_1\cdots Q_nx_n. \end{align*} Universal quantifiers are handled by arbitrary choices: if $Q_i=\forall$, the value of $x_i$ may be any element of $N$. For an existential quantifier $Q_i=\exists$, the Skolemized formula tells us exactly which witness to use. If \begin{align*} u_i=(x_{j_1},\dots,x_{j_m}) \end{align*} is the ordered tuple of preceding universal variables, define the value of $x_i$ to be the element of $N$ obtained by evaluating \begin{align*} f_i(u_i) \end{align*} in $\mathcal{N}$. This is a valid existential witness because the interpretation of $f_i$ in $\mathcal{N}$ is a function \begin{align*} f_i^{\mathcal{N}}:N^m &\to N. \end{align*} Now compare this evaluation with the Skolemized sentence. After all universal variables have been assigned values, the Skolemized matrix is obtained from $\theta$ by replacing every existential variable $x_i$ with exactly the term $f_i(u_i)$. Our chosen existential witnesses are precisely the values of those terms. Since $\mathcal{N}\models\varphi^{\mathrm{Sk}}$, the Skolemized matrix is true for every assignment of the universal variables. Therefore the original matrix $\theta$ is true in the reduct $\mathcal{N}|_L$ when the existential variables are interpreted by the witnesses supplied by the Skolem functions. This is exactly the semantic condition for \begin{align*} \mathcal{N}|_L\models Q_1x_1\cdots Q_nx_n\,\theta. \end{align*} [/guided] [/step] [step:Conclude equivalence of satisfiability] The first step shows that every model of $\varphi$ has an expansion to a model of $\varphi^{\mathrm{Sk}}$. The second step shows that every model of $\varphi^{\mathrm{Sk}}$ has an $L$-reduct satisfying $\varphi$. Hence $\varphi$ is satisfiable in the original language $L$ if and only if its Skolemized universal form $\varphi^{\mathrm{Sk}}$ is satisfiable in the expanded language $L^{\mathrm{Sk}}$. [/step]