[proofplan] The proof uses Shoenfield normal form in its ordinal-witness form: for the fixed $\Sigma^1_2$ formula there is a uniform first-order condition on levels of $L[a]$, formalized in the chosen fragment, whose witnesses are ordinals rather than arbitrary reals. The key point is that if two transitive models have the same ordinals and contain the same parameter $a$, then the recursion defining $L_\alpha[a]$ gives the same structure at every common ordinal $\alpha$. Thus the ordinal witness transfers both from $N$ to $M$ and from $M$ to $N$. The $\Pi^1_2$ case follows by applying the $\Sigma^1_2$ equivalence to negations, and the forcing corollary is the standard class version of Shoenfield absoluteness. [/proofplan]

[step:Fix the internal meaning of projective truth]Let $\mathbb{R}^{P}$ denote $P \cap \omega^\omega$ for a transitive model $P$. For a projective formula $\psi$ with real parameter $a \in P \cap \omega^\omega$, the notation \begin{align*} P \models \psi(a) \end{align*} means that all first-order quantifiers over natural numbers are interpreted in $\omega$, all real quantifiers are interpreted over $\mathbb{R}^{P}$, and all arithmetical relations on reals are interpreted externally on the actual functions $\omega \to \omega$. Because $M$ and $N$ are transitive and contain $a$, the real $a$ has the same values in $M$, in $N$, and in the ambient universe. Also, since $\omega$ is absolute for transitive models of the stated fragment, every arithmetical statement about finitely many reals belonging to both models has the same truth value in $M$ and in $N$.[/step]

[guided]We first remove an ambiguity that often hides the main issue. A projective formula contains quantifiers over reals, and a transitive model may have fewer reals than a larger transitive model. Thus, for a model $P$, define \begin{align*} \mathbb{R}^{P} := P \cap \omega^\omega. \end{align*} When we write $P \models \psi(a)$, the real quantifiers in $\psi$ range over $\mathbb{R}^{P}$, not over all reals in the ambient universe. The parameter $a$ belongs to $M \cap \omega^\omega$, and $M \subseteq N$, so $a$ is also a real of $N$. Since both models are transitive, the statement “$a(n)=m$” has the same meaning in $M$, in $N$, and externally. Therefore any purely arithmetical assertion about $a$ and other shared reals is absolute between the two models. This is the basic arithmetical absoluteness for transitive models; in the terminology of the dependency list, it is the Absoluteness of Arithmetical Truth for Transitive Models, and it is being used here as a prerequisite not yet linked in the wiki.[/guided]

[step:Put the $\Sigma^1_2$ statement into Shoenfield normal form]We use the Shoenfield ordinal-normal-form theorem in the uniform internal form stipulated in the theorem statement. For the fixed $\Sigma^1_2$ formula $\varphi(v)$, the theorem supplies a single first-order formula $\Theta_\varphi(v)$ in the language of set theory expanded by a unary predicate for $v$ such that the fragment $\mathrm{ZFC}^{-}_0$ proves, for every transitive model $P$ of the fragment and every real $b \in P \cap \omega^\omega$, \begin{align*} P \models \varphi(b) \Longleftrightarrow P \models \exists \alpha\, \bigl(\alpha \text{ is an ordinal and } L_\alpha[b] \models \Theta_\varphi(b)\bigr). \end{align*} The same formula $\Theta_\varphi$ is used in $M$ and in $N$; only the ambient model $P$ changes. The assertion $L_\alpha[b] \models \Theta_\varphi(b)$ is first-order satisfaction in the set-sized structure $(L_\alpha[b],\in,b \cap L_\alpha[b])$, not an arithmetical assertion in a real code for an arbitrary ordinal. The hypotheses of this normal-form theorem are met because $\varphi$ is a projective $\Sigma^1_2$ formula, $a$ is a real parameter, and $M$ and $N$ satisfy the fragment stipulated in the theorem statement. Apply this normal form to $P=N$ and $b=a$. Since $N \models \varphi(a)$, there exists an ordinal $\alpha \in \operatorname{Ord}^{N}$ such that \begin{align*} N \models L_\alpha[a] \models \Theta_\varphi(a). \end{align*}[/step]

[guided]The normal-form theorem is doing the main descriptive-set-theoretic work. It does not merely say that a witness can be coded in some convenient way; it gives a fixed first-order formula $\Theta_\varphi$ depending only on the projective formula $\varphi$, and the fragment $\mathrm{ZFC}^{-}_0$ proves the equivalence uniformly for every transitive model $P$ of the fragment and every real parameter $b \in P \cap \omega^\omega$. Applying this internal theorem with $P=N$ and $b=a$ is legitimate because $N$ is one of the transitive models assumed to satisfy $\mathrm{ZFC}^{-}_0$, and $a \in M \cap \omega^\omega \subseteq N \cap \omega^\omega$. Since $N \models \varphi(a)$, the right-hand side of the normal-form equivalence holds in $N$. Thus there is an ordinal $\alpha \in \operatorname{Ord}^{N}$ such that \begin{align*} N \models L_\alpha[a] \models \Theta_\varphi(a). \end{align*} This formulation is important because the witness is now the ordinal $\alpha$, not an arbitrary real of $N$.[/guided]

[step:Identify the same relativized constructible level inside both models]Because $\operatorname{Ord}^{M}=\operatorname{Ord}^{N}$, the ordinal $\alpha$ found in $N$ belongs to $\operatorname{Ord}^{M}$. We claim that $M$ and $N$ compute the same set $L_\alpha[a]$. This is proved by induction on $\beta \leq \alpha$. At $\beta=0$, both models have the same empty initial level relative to $a$. At successor stages, the defining recursion is \begin{align*} L_{\beta+1}[a]=\operatorname{Def}(L_\beta[a],\in,a\cap L_\beta[a]), \end{align*} where $\operatorname{Def}(X,\in,A)$ denotes the set of all subsets of $X$ first-order definable over the structure $(X,\in,A)$ from parameters in $X$. Since the induction hypothesis gives the same structure $L_\beta[a]$ in $M$ and $N$, and first-order satisfaction for the set-sized structure $(L_\beta[a],\in,a\cap L_\beta[a])$ is absolute between transitive models containing that structure, both models form the same definable subsets. At limit stages $\lambda \leq \alpha$, both models take the union \begin{align*} L_\lambda[a]=\bigcup_{\beta \in \lambda} L_\beta[a], \end{align*} and the index set $\lambda$ is the same ordinal in both models. To justify the successor step more explicitly, fix $\beta<\alpha$ and assume $L_\beta[a]^M=L_\beta[a]^N$. The formulas used in the definability operation are finite strings of natural numbers, so $M$ and $N$ have the same formula codes. The parameters are exactly elements of the common set $L_\beta[a]$. First-order satisfaction for the set-sized structure $(L_\beta[a],\in,a\cap L_\beta[a])$ is absolute between transitive models containing that structure, because its satisfaction relation is obtained by the usual finite recursion on formula complexity. Therefore a subset of $L_\beta[a]$ is definable over this structure from allowed parameters in $M$ if and only if it is definable in $N$. The Separation and Replacement instances included in $\mathrm{ZFC}^{-}_0$ ensure that both models collect exactly these externally characterized definable subsets at stage $\beta+1$, so their internal $\operatorname{Def}$ operations agree. Hence \begin{align*} L_\alpha[a]^M = L_\alpha[a]^N. \end{align*}[/step]

[guided]We prove equality of the two relativized constructible levels by induction on $\beta \leq \alpha$. The base stage is the same in both models, since $L_0[a]=\varnothing$. Assume $L_\beta[a]^M=L_\beta[a]^N$. At the successor stage the recursion is \begin{align*} L_{\beta+1}[a]=\operatorname{Def}(L_\beta[a],\in,a\cap L_\beta[a]), \end{align*} where $\operatorname{Def}(X,\in,A)$ is the collection of subsets of $X$ definable over $(X,\in,A)$ from parameters in $X$. The formula codes are finite strings of natural numbers, so the two transitive models have the same formula codes. The allowed parameters are exactly the elements of the common set $L_\beta[a]$. Satisfaction for the fixed set-sized structure $(L_\beta[a],\in,a\cap L_\beta[a])$ is computed by finite recursion on formula complexity, so the same formulas with the same parameters define the same subsets in $M$ and in $N$. The Separation and Replacement instances in $\mathrm{ZFC}^{-}_0$ are precisely what lets each model collect those definable subsets into the next level. Therefore $L_{\beta+1}[a]^M=L_{\beta+1}[a]^N$. If $\lambda \leq \alpha$ is a limit ordinal and the equality has been proved for all $\beta \in \lambda$, then both models form \begin{align*} L_\lambda[a]=\bigcup_{\beta \in \lambda} L_\beta[a]. \end{align*} The index ordinal $\lambda$ is the same in $M$ and $N$ because the models have the same ordinals, and the earlier levels agree by induction. Hence the unions agree. This completes the induction and gives \begin{align*} L_\alpha[a]^M=L_\alpha[a]^N. \end{align*}[/guided]

[step:Transfer the normal-form witness through satisfaction absoluteness]The assertion \begin{align*} L_\alpha[a] \models \Theta_\varphi(a) \end{align*} is first-order satisfaction in the set-sized structure $(L_\alpha[a],\in,a\cap L_\alpha[a])$. The previous step shows that $M$ and $N$ have the same such structure, and first-order satisfaction for a fixed set-sized structure is absolute between transitive models containing the structure. Therefore \begin{align*} M \models L_\alpha[a] \models \Theta_\varphi(a). \end{align*} Since $\alpha \in \operatorname{Ord}^{M}$, the Shoenfield normal form applied inside $M$ gives \begin{align*} M \models \varphi(a). \end{align*} The same argument with the roles of $M$ and $N$ reversed proves the converse implication: if $M \models \varphi(a)$, then the normal form supplies an ordinal witness $\alpha \in \operatorname{Ord}^{M}=\operatorname{Ord}^{N}$, the same structure $L_\alpha[a]$ exists in $N$, and hence $N \models \varphi(a)$.[/step]

[guided]This is the point where the proof avoids the common mistake of trying to move an arbitrary real witness from $N$ down to $M$. A $\Sigma^1_2$ statement may originally have the form “there exists a real $x$ such that for every real $y$ an arithmetical condition holds.” If $N$ has more reals than $M$, the witness $x$ supplied by $N$ need not belong to $M$. Shoenfield normal form replaces that fragile real witness by an ordinal-stage witness. From $N \models \varphi(a)$ we obtained an ordinal $\alpha$ such that \begin{align*} N \models L_\alpha[a] \models \Theta_\varphi(a). \end{align*} The ordinal $\alpha$ belongs to $M$ because $M$ and $N$ have the same ordinals. The structure $L_\alpha[a]$ is also the same in both models, because the relativized constructible hierarchy is built by a first-order definability recursion from the same parameter $a$ along the same ordinals. Now the remaining assertion is first-order satisfaction in the shared set-sized structure $(L_\alpha[a],\in,a\cap L_\alpha[a])$. Satisfaction for this fixed structure is absolute between the two transitive models because the structure, the formula $\Theta_\varphi$, and the parameter $a$ are the same in both models. Hence \begin{align*} M \models L_\alpha[a] \models \Theta_\varphi(a). \end{align*} Applying the same Shoenfield normal-form equivalence inside $M$ yields \begin{align*} M \models \varphi(a). \end{align*} The reverse implication is identical with $M$ and $N$ interchanged: an ordinal witness from $M$ is also an ordinal of $N$, and the corresponding $L_\alpha[a]$ is the same structure in both models. Thus the witness that transfers is not an arbitrary real; it is the ordinal $\alpha$ together with the common structure $L_\alpha[a]$.[/guided]

[step:Derive the $\Pi^1_2$ absoluteness statement]Let $\psi(a)$ be a $\Pi^1_2$ statement. Its negation $\neg \psi(a)$ is a $\Sigma^1_2$ statement. The previous steps proved full $\Sigma^1_2(a)$ equivalence between $M$ and $N$, so \begin{align*} M \models \neg\psi(a) \quad \Longleftrightarrow \quad N \models \neg\psi(a). \end{align*} Taking negations in the two-valued projective semantics gives \begin{align*} M \models \psi(a) \quad \Longleftrightarrow \quad N \models \psi(a). \end{align*} Therefore $\Pi^1_2(a)$ truth is absolute between $M$ and $N$.[/step]

[guided]A $\Pi^1_2(a)$ statement is the negation of a $\Sigma^1_2(a)$ statement. Let $\psi(a)$ be $\Pi^1_2(a)$. Then $\neg\psi(a)$ is $\Sigma^1_2(a)$, so the equivalence already proved gives \begin{align*} M \models \neg\psi(a) \Longleftrightarrow N \models \neg\psi(a). \end{align*} Projective truth in each model is two-valued for the fixed internal semantics over its own reals. Therefore negating both sides gives \begin{align*} M \models \psi(a) \Longleftrightarrow N \models \psi(a). \end{align*} This proves the $\Pi^1_2(a)$ case without using a one-directional absoluteness argument.[/guided]

[step:Apply the class form to forcing extensions]Let $\mathbb{P} \in V$ be a forcing notion, and let $G$ be $V$-generic for $\mathbb{P}$. The ground model $V$ and the forcing extension $V[G]$ are transitive proper classes with \begin{align*} V \subseteq V[G]. \end{align*} Forcing does not add ordinals, so \begin{align*} \operatorname{Ord}^{V}=\operatorname{Ord}^{V[G]}. \end{align*} The real parameter $a$ belongs to $V \cap \omega^\omega$, hence also to $V[G] \cap \omega^\omega$. The preceding proof was written for transitive set models, but every ingredient used after fixing $a$ and the projective formula is set-sized: the ordinal witness $\alpha$, the set $L_\alpha[a]$, and the first-order satisfaction relation for $(L_\alpha[a],\in,a\cap L_\alpha[a])$. The Shoenfield ordinal-normal-form theorem is a theorem of the ambient set theory and therefore applies to the class semantics of $V$ and $V[G]$ with projective real quantifiers ranging over $V\cap\omega^\omega$ and $V[G]\cap\omega^\omega$, respectively. The recursion defining $L_\alpha[a]$ is absolute between these classes because they have the same ordinals and the same parameter $a$, and satisfaction for the resulting set-sized structure is absolute once the structure is fixed. Thus the same ordinal-witness transfer applies to the class pair $V \subseteq V[G]$. Therefore every $\Sigma^1_2(a)$ statement has the same truth value in $V$ and $V[G]$. Applying the previous step to negations gives the same conclusion for every $\Pi^1_2(a)$ statement. This proves the forcing-extension consequence.[/step]

[guided]The forcing consequence is the class analogue of the set-model argument. Let $\mathbb{P} \in V$ be a forcing notion and let $G$ be $V$-generic for $\mathbb{P}$. The classes $V$ and $V[G]$ are transitive, $V \subseteq V[G]$, and [forcing preserves ordinals](/theorems/6539): \begin{align*} \operatorname{Ord}^{V}=\operatorname{Ord}^{V[G]}. \end{align*} The real parameter $a$ belongs to $V \cap \omega^\omega$, so it is also a real of $V[G]$. The earlier proof only used set-sized objects after the formula and parameter were fixed: an ordinal witness $\alpha$, the set $L_\alpha[a]$, and first-order satisfaction for the set-sized structure $(L_\alpha[a],\in,a\cap L_\alpha[a])$. The Shoenfield ordinal-normal-form theorem applies in the ambient set theory to the projective semantics of both classes, with real quantifiers ranging over the reals of the relevant class. The recursion defining $L_\alpha[a]$ is the same in $V$ and $V[G]$ because the parameter $a$ and the ordinals are the same, and the satisfaction relation for that set-sized structure is absolute once the structure is fixed. Hence the same ordinal-witness transfer proves $\Sigma^1_2(a)$ absoluteness between $V$ and $V[G]$. Applying the $\Pi^1_2$ reduction to negations gives the corresponding $\Pi^1_2(a)$ absoluteness.[/guided]