Height of minimal model of ZFC What do we know about the height of the minimal (transitive) model of ZFC, that is, about the least α such that Lα is a model of ZFC? Call this ordinal μ. It is countable, since otherwise we could build L inside the collapse of a countable elementary submodel of Lμ to obtain a lesser such α. Moreover, as I learned here on MO, μ is Δ12 definable in V.
 A: I claim that the ordinal $\mu$, if it exists, is actually
$\Pi^1_1$ definable, which improves on your $\Delta^1_2$
claim. What I mean by this is that the set of reals coding
a relation on $\omega$ having order type $\mu$ is a
$\Pi^1_1$ set of reals. Even more, I claim that it is a
$\Delta^1_1$ property about reals, among those that do code
well-orders. That is, the set of codes for $\mu$ is the
intersection of WO with a hyperarithmetic set.
First, let's show that the set of reals $x$ coding a
relation $\lhd$ of order type $\mu$ has complexity
$\Pi^1_1$. It is well-known to be a $\Pi^1_1$ property of
$x$ to assert that the relation $\lhd$ it codes on $\omega$
is a well-order, of some order type $\alpha$. I claim that
$x$ is coding $\mu$ if and only if, in addition, for every
countable structure $M$, if $M$ satisfies V=L and the
ordinals of $M$ have an initial segment isomorphic to
$\alpha+1$, then $M$ thinks that the $\alpha$-th ordinal is
the height of the minimal model of ZFC.
This additional property is indeed $\Pi^1_1$. To see this,
note first that the assertion that $M$ satisfies a certain
theory is an arithmetic property about $M$, and the
existence of the order-isomorphism from $\lhd$ to an
initial segment of $M$ is a $\Sigma^1_1$ assertion, but it
appears in the hypothesis of an implication here, so
altogether the assertion is $\Pi^1_1$. The critical fact we
are using here is that we don't assert that $M$ is fully
well-founded, but only that it is well-founded beyond the
height of the order coded by $x$, which is sufficient to
determine whether $x$ codes $\mu$ or not.
Let us now argue that this property does indeed define the
codes of $\mu$. If $x$ does code $\mu$, then any model $M$
satisfying V=L and well-founded up to $\mu+1$ will agree
that $\mu$ is the height of the minimal model of ZFC, so
$x$ will pass this definition. Conversely, if $x$ codes a
well-order of order type $\alpha$ and any model $M$ thinks
that $\alpha$ is the height of the minimal model, then it
will be right.
What the argument shows is that the set of codes is a
$\Delta^1_1$ property, that is, a hyperarithmetic property,
on the set WO of codes for well orders. Given that $x$
codes a well-order, then we can say that $x$ codes $\mu$ if
and only if, every countable $M$ satisfying V=L and
well-founded beyond the height of the ordinal $\alpha$
coded by $x$ agrees that $\alpha$ is $\mu$; and also, if
and only if there is such an $M$. So we've got a $\Pi^1_1$
and a $\Sigma^1_1$ characterization, provided that we
already know that $x$ is coding a well-order.
We can get a unique code, rather than a set of codes, by
observing that if $\mu$ exists, then not only is it
countable, but it is countable in $L$, and so there is an
$L$-least code for $\mu$. This code is also
$\Pi^1_1$-definable, since $z$ is this $L$-least code if
and only if it does code a well-order of type $\alpha$, and
all countable models of V=L that are well-founded at least
that high and that think that that ordinal $\alpha$ is
countable, think that $z$ is the $L$-least code of
$\alpha$. The point again is that such models, even if
ill-founded up high, will be right about this information.
