Finite transitive counterexample for power-set equality (source code)

= Finite transitive counterexample for power-set equality
{title2=$M\models3=\mathcal P(2),\qquad V_4\not\models3=\mathcal P(2)$}

Let $M=4$ be a <Finite von Neumann ordinal> and $N=V_4$. With parameters $x=3$, $y=2$, the transitive structure $M$ satisfies the first-order power-set specification, since its available <subsets> of $2$ are exactly $0,1,2$. In $N$, the additional <subset> $\{1\}$ makes the same specification false. Bounded <logical formulas> are absolute between <transitive sets> by induction, so existential <logical formulas> with bounded matrices are upward absolute. This counterexample therefore rules out an unrestricted logical equivalence of power-set equality with a $\Sigma_1$ <logical formula>.