Question: Is it provable in ZFC that every structure that is ordinal definable up to isomorphism has an ordinal definable isomorphic copy? If not, what are some counterexamples? All structures are set-sized.
In other words, if we define a structure up to isomorphism (as mathematical definitions often do), can we always provably define a specific example of an isomorphic structure?
A positive answer would likely generalize to a definable procedure for the following: Given a nonempty set $S$ of isomorphic structures, choose a structure, possibly outside of $S$, that is isomorphic to an element of $S$.
Here is an illustration of some of the subtleties. Assuming GCH, up to isomorphism, there is a unique $ω_2$-saturated elementary extension of second order arithmetic (equivalently, $(ℝ,ℕ,+,⋅,=)$) of cardinality $ω_2$. But defining a specific example of the extension seems problematic — every nonstandard integer in real analysis gives a nonprincipal ultrafilter on $ℕ$, and consistently with ZFC, no such ultrafilters are definable. Still, A definable nonstandard model of the reals unconditionally gives a definable countably saturated elementary extension.
We can also consider restricting the domain of the definable isomorphic copy:
- If the copy must be in HOD, then there are counterexamples, such as the second order arithmetic (assuming $ℝ∉\text{HOD}$).
- If the domain of the copy must consist of sets of ordinals, then the copy still has an ordinal definable (OD) linear ordering, so under appropriate assumptions, third order arithmetic would be a counterexample. I think there is even a symmetric generic extension of $V$ with an OD non-linearly-orderable countable set of countable sets of reals.
- Requiring the domain of the copy to consist of sets of sets of ordinals does not affect existence of a definable copy.
