Exercise on constructible universe: computing the L-rank of Th(HF) Below is exercise II.6.8 from Kunen's Set Theory (2011 edition):

Prove that $\text{Th(HF)}\in V_{\omega+1}\setminus L_{\omega+1}$, and $\rho(\text{Th(HF)})=\omega+1$, while rank$(\text{Th(HF)})=\omega$.

The first part of the exercise follows directly from Tarski's Theorem on the undefinability of truth since $\text{Th(HF)} \notin \mathcal{D}(\text{HF})$. The more difficult part lies in verifying $\text{Th(HF)}\in \mathcal D(L_{\omega+1})$. Kunen suggests that we can use Tarski's definition of truth within the model $L_{\omega+1}$ to define $\text{Th(HF)}$. Although this approach might seem promising, Kunen adds the caveat that, since $L_{\omega+1}$ isn't a model of any reasonable set theory (e.g. the Axiom of Pairing fails), we need some tricky coding arguments to implement this definition inside $L_{\omega+1}$. I understand that as $L_{\omega+1}$ doesn't satisfy enough ZF axioms, the usual recursive definition of truth is not justified. And even if the definition makes sense, it is not absolute. However, I have no idea what "coding arguments" Kunen has in mind, can someone provide a hint? Thanks in advance.
 A: The key issue is the choice of pairing function. Contra our usual experiences, in this case the way we implement pairing is quite crucial, and we need to use an approach whose existence is quite non-obvious: a "constructibly flat" pairing function.
A flat pairing function is a pairing function which does not increase rank unnecessarily: that is, such that $$rank(\langle a,b\rangle)=\max\{rank(a),rank(b),\omega\}$$ (we need to throw $\omega$ in their for cardinality reasons: there just aren't enough sets of rank $n$ for $n<\omega$ to have flatness at finite ranks). The usual example of a flat pairing function is the Quine-Rosser pairing function (but there are others).
Here we need a twist on flatness, which luckily Quine-Rosser also satisfies: namely, that $L_\alpha$ is closed under it whenever $\alpha$ is infinite. That is, we want a pairing function which doesn't increase $L$-rank (instead of $V$-rank). 
This lets us construct "finite type objects over $L_\alpha$" in $L_{\alpha+1}$; for example, using the Quine-Rosser approach we have that each definable function $L_\alpha\times L_\alpha\rightarrow L_\alpha$ literally is an element of $L_{\alpha+1}$. The objects we want in this case are witnesses to satisfaction. There are various ways to approach the definition of "$F$ witnesses that $\varphi$ is true in $L_\omega$," including:


*

*Skolem functions.

*Appropriate subtrees of the "big syntax tree" of $\varphi$ ("big" in the sense that we unfold all quantifiers as infinite conjunctions/disjunctions).

*Winning strategies in the "truth game."
The point is that each of the above approaches can be implemented in $L_{\omega+1}$: if $L_\omega\models\varphi$ then a witness to this exists in $L_{\omega+1}$. This then lets us built the set of all $\varphi$ for which witnesses to $L_\omega\models\varphi$ exist at $L_{\omega+2}$.

This leaves aside the issue of actually defining the relation "$F$ witnesses that $\varphi$ is true in $L_\omega$" (whichever of the approaches above we take). However, while technically the hard bit this isn't particularly counterintuitive - the naive approach (brute force) actually works. The counterintuitive feature was the implementation of ordered pairs in such a way that the $L$-rank could be kept low, which ironically was the technically trivial-ish part.
