In mathematical set theory, a set S is said to be ordinal definable if, informally, it can be defined in terms of a finite number of ordinals by a first-order formula.
A drawback to the above informal definition is that it requires quantification over all first-order formulas, which cannot be formalized in the standard language of set theory.
However, there is a different, formal such characterization: The latter denotes the set in the von Neumann hierarchy indexed by the ordinal α1.
The class of all ordinal definable sets is denoted OD; it is not necessarily transitive, and need not be a model of ZFC because it might not satisfy the axiom of extensionality.
HOD has been found to be useful in that it is an inner model that can accommodate essentially all known large cardinals.