Why can't $L_\beta$ contain a real coding a well-ordering of order-type $\beta$, when $\beta$ is a gap ordinal?

Question

In Gaps in the constructible universe, Marek and Srebrny, 1973 a gap ordinal is defined as follows

$\alpha$ is a gap ordinal iff $(L_{\alpha+1}-L_\alpha)\cap \mathcal{P}(\omega) = \emptyset$

Their Lemma 2.4. and its proof are

Let $\alpha$ be a gap ordinal. If $X \in \mathcal{P}(\omega) \cap L_\alpha$ and $X$ is a real well-ordering, then the type of $X$ is less than $\alpha$.

Proof. Assume not. We can construct a tree coding all of $L_\alpha$ within $L_\alpha\cap \mathcal{P}(\omega)$. Now, we apply Cantor's diagonal procedure to obtain a new set of natural numbers.

As usual, by $X$ being a real well-ordering they mean $X = \{ J(m, n) \: | \: \langle m, n \rangle \in R \}$, where $R$ is a well-ordering of the naturals and $J$ a fixed pairing bijection. $X$ is order-isomorphic to $R$.

I'm familiar with Cantor's diagonal procedure, but I don't understand what they mean by a tree coding $L_\alpha$ within $L_\alpha\cap \mathcal{P}(\omega)$, neither know how to make sure it is definable over $L_\alpha$, or how to diagonalize from that.

Answer 1

A proof now appears as lemma 1.21 of the poster's bachelor's thesis "The real numbers in inner models of set theory" (2022, arXiv), however I have a doubt about the proof which is expressed in a comment on the question. In case of the event that the proof as written in the thesis fails, the following is a diagonal-argument-based proof which may be closer to what Marek and Srebrny may have done.

---

Assume that $\alpha$ is a gap ordinal and there is a set $X\in L_\alpha\cap\mathcal P(\omega)$ which codes a well-ordering of order type $\alpha$. From the corollary in Marek and Srebrny after lemma 2.2 we know that $(\omega,L_\alpha\cap\mathcal P(\omega))$ models the second-order arithmetic $\mathcal A_2$, which includes all axioms of the theory $Z_2$ appearing in Simpson's Subsystems of Second-Order Arithmetic (2009). By section VII.4 of Simpson, for every initial segment $X'$ of $X$, the set $L^\omega_{X'}$ can be defined in $\mathrm{ATR}_0$. Given $X$, it is also possible to define in $\mathrm{ATR}_0$ the set $\mathrm{fld}(X)=\{x,y\in\mathbb N \mid (x,y)\in X\}$ (by $\Delta^0_1$-comprehension, as $(x,y)\in X$ iff $\exists p(p=(x,y)\land p\in X)\land\forall p(p\notin X\implies p\neq(x,y))$) and the function $\mathrm{enum}_{\mathrm{fld}(X)}$, where $\mathrm{enum}_{\mathrm{fld}(X)}(n)$ is the $n$th element of $\mathrm{fld}(X)$ in size order (by lemma II.3.6 if $X$ is infinite, and by $\Delta^0_1$-comprehension otherwise). Let $X_i$ be $\{a\in X\mid \langle a,\mathrm{enum}_{\mathrm{fld}(X)}(i)\rangle\in X\}$, i.e. the restriction of $X$ to $\mathrm{enum}_{\mathrm{fld}(X)}(i)$, $\mathrm{ATR}_0$ proves that for all natural numbers $i$, $X_i$ exists, by $\Delta^0_1$-comprehension. Then the function taking $i$ to $X_i$ exists in $L_\alpha\cap\mathcal P(\omega)$. We may then perform a diagonal argument, defining a real $D = \{i\in\mathbb N \mid i\notin X_i\}$ by $\Delta^0_1$-comprehension with the function $i\mapsto X_i$ as a parameter. $\square$

This seems to carry out for any $L_\alpha\cap\mathcal P(\omega)$ that models $\mathrm{ATR}_0$. In fact, by the Well-Ordering Isomorphism Lemma in Gostanian's "The Next Admissible Ordinal" (Annals of Math. Logic, vol. 17, 1979), if $\alpha$ is an ordinal such that $L_\alpha$ satisfies Kripke-Platek set theory, $L_\alpha$ (and thus $L_\alpha\cap\mathcal P(\omega)$) cannot contain any well-ordering $X$ with order type $\alpha$, since if it did, the Mostowski collapse of $X$ would be in $L_\alpha$, namely $\alpha$ would be in $L_\alpha$. Additionally, if $L_\alpha$ is a union of admissible levels of $L$, any $X\in L_\alpha\cap\mathcal P(\omega)$ with order type $\alpha$ would be a member of $L_\beta\cap\mathcal P(\omega)$ for some admissible $\beta<\alpha$, which is a contradiction. I am not aware if there is a result showing any $\alpha$ where $L_\alpha\cap\mathcal P(\omega)$ models $\mathrm{ATR}_0$ must be admissible or a limit of admissibles, but if there is, this admissibility-based method would agree with the above result.