Definable power set ($\mathcal{D}(X)$)

The definable power set $\mathcal{D}(X)$ consists of the subsets of $X$ definable over the structure $(X,\in )$ by a first-order formula with parameters from $X$.

The constructible hierarchy is defined byfor limit ordinals $\lambda$. Its union is the constructible universe $L$.

A condensation sentence is a fixed first-order sentence $\sigma$ such that every transitive set satisfying $\sigma$ is $L_{\lambda }$ for a limit ordinal $\lambda$. It combines a sufficiently strong finite fragment of set theory, the assertion that every set is constructible, and the absence of a largest ordinal.

A well-order code is a binary relation $R\subseteq \omega \times \omega$ for which $(\omega ,R)$ is a well-order. Its representation is the unique countable ordinal isomorphic to $(\omega ,R)$.

A level $L_{\lambda }$ is a coding level when $\lambda$ is a limit ordinal, the representation of every well-order code in $L_{\lambda }$ is below $\lambda$, and every ordinal below $\lambda$ has a well-order code in $L_{\lambda }$.