A countable ordinal which is $\Sigma_n$-definable in first-order ZFC, but not $\Sigma_m^1$-definable in full second-order arithmetic

Question

Let us say that a $\Sigma_m^1$-formula $\phi$ defines a countable ordinal $\alpha$ if it defines a type-$1$ object (i.e. a real) $x$ that encodes a well-ordering of $\mathbb{N}$ of order type $\alpha$ (assuming that there is a fixed way to interpret a real as a well-ordering of $\mathbb{N}$).

Does there exist a countable ordinal $\alpha$ that satisfies both of the following two properties?

1. There exists an integer $n$ such that $\alpha$ is $\Sigma_n$-definable (without parameters) in the language of first-order ZFC (by a formula in the Lévy hierarchy) over $L_{\omega_1}$;
2. There does not exist an integer $m$ such that $\alpha$ is $\Sigma_m^1$-definable (without parameters) in the language of full second-order arithmetic (over the standard model).

If no, why? If yes, what is the smallest such $\alpha$? Can its value depend on whether we accept some additional assumptions or axioms?

Answer 1

No, there is no such ordinal (or even set).

Actually we need to be a bit careful; what does it mean to talk about the definability of an ordinal in the context of arithmetic? Below, I'm assuming that by "$\alpha$ is $\Sigma^1_n$" we mean "the set of reals coding relations on $\mathbb{N}$ which are isomorphic to $\alpha$ is $\Sigma^1_n$," but there is some flexibility here; e.g. maybe you want a specific code for $\alpha$ to be so definable.

The reason is that elements of $L_{\omega_1}$ (or even $H_{\omega_1}$) can be "reasonably" coded by real numbers. There are several ways to do this; my personal favorite is to say that the codes of a set $x$ are the reals coding (in some reasonable way) the membership graph of $tc(\{x\})$, which is a countable graph and so can be coded by a real. The important thing to check is that $(i)$ the set of reals which are codes for sets and $(ii)$ the relation of "$r$ and $s$ code the same set" are each projectively definable, but this isn't hard. At a quick glance, the set $C_\alpha$ of codes for an ordinal $\alpha$ which is $\Sigma_n$-definable in $L_{\omega_1}$ is itself $\Sigma^1_{2n}$.

If memory serves, details appear in Sacks' book Higher recursion theory.