Ordinal definable

Ordinal definability is a concept which is key in certain aspects of inner model theory. We say a set \(x\) is ordinal-definable iff there is an ordinal \(\beta\) and a collection \(\alpha_1, \alpha_2, \cdots, \alpha_n\) of ordinals so that \(x \in V_\beta\) and there is a first-order formula \(\varphi\) such that, for all \(y \in V_\beta\), \(y = x\) iff \(V_\beta \models \varphi(y, \alpha_1, \alpha_2, \cdots, \alpha_n)\). In other words, it is definable at some initial segment of the von Neumann hierarchy with ordinal parameters. The class of ordinal definable sets is denoted \(\mathrm{OD}\), and \(\mathrm{HOD} = \{x: \mathrm{TC}(x) \in \mathrm{OD}\}\). \(\mathrm{HOD}\) is an inner model and \(V = \mathrm{HOD}\) is equivalent to \(V = \mathrm{OD}\): however, \(\mathrm{OD}\) is rarely talked about because, in the case that \(V \neq \mathrm{OD}\), \(\mathrm{OD}\) may not be transitive, while \(\mathrm{HOD}\) will, trivially, always be. \(\mathrm{HOD}\) is one of the simplest and well-known inner models.

Unlike with other inner models, HOD is not particularly robust: for any model \(M\), there is a forcing extension \(M[G]\) in which all elements of \(M\) become ordinal definable (i.e. \(V = \mathrm{HOD}\)) - in contrast with the fact that e.g. being constructible can not be changed by forcing. On the other hand, HOD is able to accommodate many large cardinals. This is in contrast to the fact that traditional inner models that can accommodate even just supercompact cardinals have not yet been constructed. For example, "there is a measurable cardinal and all sets are constructible, i.e. \(V = L\)" is necessarily inconsistent, while the consistency of an extendible cardinal implies the consistency of "there is a measurable cardinal and all sets are ordinal definable, i.e. \(V = \mathrm{HOD}\)". This follows from the HOD dichotomy. On the more extreme side of things, if the wholeness axioms, an axiomatization of the existence of a nontrivial elementary embedding of the universe into itself which avoid Kunen's inconsistency, are consistent, then they are compatible with the assertion "all sets are ordinal definable".

HOD is a useful inner model and the aforementioned HOD dichotomy gives an analogous result for HOD to the fact that \(0^\sharp\) exists iff L does not have the covering property: however, there is no known sharp for HOD that would lead to HOD being far away from the true universe, primarily due to the fact that it is compatible with all known large cardinals. The reason traditional inner models are preferred is that, as mentioned earlier, not only is HOD non-robust, but it does not have the same fine structure that \(L\) and core models have.