[proofplan] We prove the theorem by structural induction on first-order formulas. Atomic formulas are already prenex. For the induction steps, we use three syntactic operations: alpha-renaming of bound variables to avoid capture, dualizing quantifier prefixes under negation, and pulling quantifier prefixes across Boolean connectives when the quantified variable is not free in the other factor. These operations preserve truth in every structure under every assignment, so iterating them produces an equivalent formula consisting of a quantifier prefix followed by a quantifier-free matrix. [/proofplan] [step:Fix the syntactic conventions and the meaning of equivalence] A formula is in prenex normal form if it has the form \begin{align*} Q_1 x_1\, Q_2 x_2 \cdots Q_m x_m\, \theta, \end{align*} where $m \geq 0$, each $Q_i \in \{\forall,\exists\}$, each $x_i$ is a variable, and $\theta$ is quantifier-free. When $m=0$, the formula is just the quantifier-free formula $\theta$. For formulas $\alpha$ and $\beta$, write $\alpha \equiv \beta$ to mean logical equivalence: for every $\mathcal{L}$-structure $\mathcal{M}$ and every variable assignment $s$ in $\mathcal{M}$, \begin{align*} \mathcal{M},s \models \alpha \iff \mathcal{M},s \models \beta. \end{align*} We use that bound variables may be renamed to fresh variables without changing logical equivalence. Since the variable supply is infinite and every formula contains only finitely many variables, whenever finitely many variables must be avoided, a fresh variable exists. [/step] [step:Record the quantifier movement equivalences] Let $A$ and $B$ be $\mathcal{L}$-formulas, let $x$ be a variable not occurring free in $B$, and let $\star \in \{\land,\lor\}$. Then \begin{align*} (\forall x\,A)\star B &\equiv \forall x\,(A\star B),\\ (\exists x\,A)\star B &\equiv \exists x\,(A\star B),\\ B\star(\forall x\,A) &\equiv \forall x\,(B\star A),\\ B\star(\exists x\,A) &\equiv \exists x\,(B\star A). \end{align*} We verify one representative case; the others follow from the same semantic calculation using the truth tables for $\land$ and $\lor$. Suppose $\star=\land$ and consider $(\forall x\,A)\land B$. For any $\mathcal{L}$-structure $\mathcal{M}$ and assignment $s$, \begin{align*} \mathcal{M},s \models (\forall x\,A)\land B &\iff \mathcal{M},s \models \forall x\,A \text{ and } \mathcal{M},s \models B \\ &\iff \text{for every } a \in M,\ \mathcal{M},s[x\mapsto a]\models A,\text{ and } \mathcal{M},s\models B. \end{align*} Because $x$ is not free in $B$, the satisfaction of $B$ is unchanged when only the value assigned to $x$ is altered. Hence \begin{align*} \mathcal{M},s \models (\forall x\,A)\land B &\iff \text{for every } a \in M,\ \mathcal{M},s[x\mapsto a]\models A\land B \\ &\iff \mathcal{M},s \models \forall x\,(A\land B). \end{align*} Negation dualizes quantifiers: \begin{align*} \neg\forall x\,A &\equiv \exists x\,\neg A,\\ \neg\exists x\,A &\equiv \forall x\,\neg A. \end{align*} Indeed, for every $\mathcal{M}$ and $s$, \begin{align*} \mathcal{M},s \models \neg\forall x\,A &\iff \text{not for every } a\in M,\ \mathcal{M},s[x\mapsto a]\models A \\ &\iff \text{there exists } a\in M \text{ such that } \mathcal{M},s[x\mapsto a]\models \neg A \\ &\iff \mathcal{M},s \models \exists x\,\neg A, \end{align*} and the existential case is analogous. [/step] [step:Put negations of prenex formulas into prenex form] Let \begin{align*} P = Q_1x_1\,Q_2x_2\cdots Q_mx_m \end{align*} be a quantifier prefix, and let $\theta$ be quantifier-free. Define the dual quantifier $Q_i^\perp$ by \begin{align*} Q_i^\perp = \begin{cases} \exists, & Q_i=\forall,\\ \forall, & Q_i=\exists. \end{cases} \end{align*} Then \begin{align*} \neg\bigl(Q_1x_1\,Q_2x_2\cdots Q_mx_m\,\theta\bigr) \equiv Q_1^\perp x_1\,Q_2^\perp x_2\cdots Q_m^\perp x_m\,\neg\theta. \end{align*} This follows by induction on $m$ using the two negation equivalences from the previous step. Since $\theta$ is quantifier-free, $\neg\theta$ is also quantifier-free. Therefore the negation of any prenex formula is equivalent to a prenex formula. [/step] [step:Combine two prenex formulas through a Boolean connective] Let \begin{align*} \alpha &= Q_1x_1\,Q_2x_2\cdots Q_mx_m\,\theta,\\ \beta &= R_1y_1\,R_2y_2\cdots R_ny_n\,\eta \end{align*} be prenex formulas, where $\theta$ and $\eta$ are quantifier-free. By alpha-renaming bound variables, assume that the variables $x_1,\dots,x_m,y_1,\dots,y_n$ are pairwise distinct, none of the $x_i$ occurs free in $\beta$, and none of the $y_j$ occurs free in $\alpha$. For $\star\in\{\land,\lor\}$, repeated use of the quantifier movement equivalences gives \begin{align*} \alpha\star\beta &\equiv Q_1x_1\,Q_2x_2\cdots Q_mx_m\,(\theta\star\beta)\\ &\equiv Q_1x_1\,Q_2x_2\cdots Q_mx_m\,R_1y_1\,R_2y_2\cdots R_ny_n\,(\theta\star\eta). \end{align*} The matrix $\theta\star\eta$ is quantifier-free because both $\theta$ and $\eta$ are quantifier-free. Hence the conjunction or disjunction of two formulas equivalent to prenex formulas is again equivalent to a prenex formula. [/step] [step:Run structural induction on formulas] We prove by structural induction on $\varphi$ that $\varphi$ is equivalent to a prenex formula. If $\varphi$ is atomic, then $\varphi$ is quantifier-free, hence already prenex with empty prefix. Suppose $\varphi=\neg A$. By the induction hypothesis, there is a prenex formula \begin{align*} A' = Q_1x_1\,Q_2x_2\cdots Q_mx_m\,\theta \end{align*} such that $A\equiv A'$. Therefore $\neg A\equiv \neg A'$. By the negation step, \begin{align*} \neg A' \equiv Q_1^\perp x_1\,Q_2^\perp x_2\cdots Q_m^\perp x_m\,\neg\theta, \end{align*} which is prenex. Suppose $\varphi=A\land B$ or $\varphi=A\lor B$. By the induction hypothesis, choose prenex formulas $A'$ and $B'$ such that $A\equiv A'$ and $B\equiv B'$. Then $\varphi$ is equivalent to $A'\land B'$ or $A'\lor B'$, respectively. The Boolean combination step puts this formula into prenex form. Suppose $\varphi=\forall x\,A$. By the induction hypothesis, choose a prenex formula \begin{align*} A' = Q_1x_1\,Q_2x_2\cdots Q_mx_m\,\theta \end{align*} with $A\equiv A'$. After alpha-renaming bound variables inside $A'$ if needed, assume $x$ does not clash with the prefix variables. Then \begin{align*} \forall x\,A \equiv \forall x\,A' = \forall x\,Q_1x_1\,Q_2x_2\cdots Q_mx_m\,\theta, \end{align*} which is prenex. The case $\varphi=\exists x\,A$ is identical, giving \begin{align*} \exists x\,A \equiv \exists x\,Q_1x_1\,Q_2x_2\cdots Q_mx_m\,\theta. \end{align*} Thus every formula built from atomic formulas using negation, conjunction, disjunction, universal quantification, and existential quantification is equivalent to a formula in prenex normal form. Any additional Boolean connective such as $\to$ or $\leftrightarrow$ is first replaced by its standard quantifier-free Boolean abbreviation, so the same conclusion applies to arbitrary first-order formulas. This completes the proof. [/step]