Constructible-level absoluteness over ZF
= Constructible-level absoluteness over ZF
{title2=$L_\alpha^M=L_\alpha$}
If $M$ is a <transitive model> of <ZF>, its internally computed $L_\alpha$ is the actual $L_\alpha$ for each <ordinal> $\alpha\in M$. At a successor stage use absoluteness of satisfaction for the same <set> structure, formula codes and parameters; at a limit stage take the union of the already identical earlier stages. Choice is not required.