This question arises from an issue arising in user38200's recent question concerning models of set theory in which [every definable set has a definable element](https://mathoverflow.net/a/180734/1946). In my answer to that question, with François's help, it turned out that $V=\text{HOD}$ is equivalent to the assertion that every $(\Sigma\_2\wedge\Pi\_2)$-definable set has an ordinal-definable element. 


The question here is whether this level of complexity can be reduced to $\Sigma\_2$ or not.


**Question 1.** Is there a model of $\text{ZFC}+V\neq\text{HOD}$ in which every $\Sigma\_2$-definable set has an ordinal definable element? 


In the equivalence to $V=\text{HOD}$, the $\Sigma\_2\wedge\Pi\_2$ level of complexity arises because in any model of $\text{ZFC}+V\neq\text{HOD}$, the set of all minimal-rank non-OD sets is defined by a formula of complexity $\Sigma\_2\wedge\Pi\_2$, but has no ordinal-definable elements. I know that this set cannot in general be defined provably by a $\Sigma\_2$ formula, since we could preserve the truth of any $\Sigma\_2$ formula by forcing up high so as to code sets into the GCH pattern (or some other desired method of coding), and thereby change which sets down low were in OD without affecting that given $\Sigma\_2$ assertion. But it isn't clear to me how that observation answers the question here, since one would seem to need to construct a counterexample model of $V\neq\text{HOD}$, where all $\Sigma\_2$-definable sets had OD members, and forcing to change that one set doesn't seem to do this. 


I am also interested in the case of $\Pi\_2$-definability. 


**Question 2.** Is there a model of $\text{ZFC}+V\neq\text{HOD}$ in which every $\Pi\_2$-definable set has an ordinal-definable element? 



Can $V\neq\text{HOD}$ if every $\Sigma_2$-definable set has an ordinal-definable element?
**Update.** (June, 2017) François Dorais and I have completed a paper growing out of this answer and our others on related posts. 



> 
> F. G. Dorais and J. D. Hamkins, [When does every definable nonempty set have a definable element?](http://jdh.hamkins.org/when-does-every-definable-nonempty-set-have-a-definable-element/) ([arχiv:1706.07285](https://arxiv.org/abs/1706.07285))
> 
> 
> 
> > ***Abstract.** The assertion that every definable set has a definable element is equivalent over ZF to the principle $V=\newcommand\HOD{\text{HOD}}\HOD$, and indeed, we prove, so is the assertion merely that every $\Pi\_2$-definable set has an ordinal-definable element. Meanwhile, every model of ZFC has a forcing extension satisfying $V\neq\HOD$ in which every $\Sigma\_2$-definable set has an ordinal-definable element. Similar results hold for $\HOD(\mathbb{R})$ and $\HOD(\text{Ord}^\omega)$ and other natural instances of $\HOD(X)$.*
> 
> 
> Read more [at the blog post](http://jdh.hamkins.org/when-does-every-definable-nonempty-set-have-a-definable-element/).
> 
> 
> 


$\newcommand\ZFC{\text{ZFC}}
\newcommand\HOD{\text{HOD}}
\newcommand\P{\mathbb{P}}
\newcommand\Q{\mathbb{Q}}$


**Original answer.** It turns out that question 1 has a positive answer, while question
2 has a negative answer.


The reader may find it useful to know of the characterization of
the $\Sigma\_2$ properties as the [semi-local properties](http://jdh.hamkins.org/local-properties-in-set-theory/), those
which are equivalent to an assertion of the form $\exists\theta\
V\_\theta\models\psi$, where $\psi$ can have any complexity. In
particular, whenever a $\Sigma\_2$ property $\varphi(A)$ is true of
a set $A$, it is because there is some $V\_\theta$ satisfying
something about $A$. We may therefore preserve that $\Sigma\_2$
fact about $A$, while forcing over $V$, provided that we only
force up high and preserve $V\_\theta$, the rank-initial-segment of
the universe up to $\theta$.


First, let's consider the positive answer to question 1.


**Theorem 1.** Every model of $\ZFC$ has a forcing extension
satisfying $V\neq\HOD$, in which every $\Sigma\_2$-definable set
has an ordinal-definable element.


Proof idea: perform a forcing iteration, considering each
$\Sigma\_2$ formula in turn, where we try to freeze the set defined
by that formula and then code one of its elements (if any) into
the GCH pattern high above the witness to that $\Sigma\_2$
property. In the end, every nonempty $\Sigma\_2$-definable set will
contain an ordinal-definable element.


**Proof.** Start with $V$ as a ground model. Without loss, by forcing
if necessary, we may assume that $V$ satisfies $V=\HOD$, so that
there is a definable well-ordering of the universe. Enumerate the
$\Sigma\_2$ formulas $\varphi\_0,\varphi\_1,\ldots$, and so on. Note
that we may refer to $\Sigma\_2$-truth since there is a universal
truth predicate for truth of bounded complexity (so there will be
no issues with Tarski's theorem on the non-definability of truth).
We define a full-support forcing iteration $\P$ of length
$\omega$, where the forcing at each stage will become
progressively more highly closed. At the first stage, we consider
the formula $\varphi\_0$, and ask: is there a forcing extension
$V[g\_0]$ in which $\varphi\_0$ holds of a nonempty set $A\_0$? If
so, we perform such a forcing (choose the least poset forcing
this), and let $\lambda\_0$ be the smallest $\beth$-fixed point
above the size of that forcing so that also $\varphi\_0$ is
witnessed in $V\_{\lambda\_0}^{V[g\_0]}$. Next, perform additional
$\leq\lambda\_0$-closed forcing over $V[g\_0]$ to an extension
$V[g\_0][h\_0]$, where $h\_0$ forces to code one of the elements of
$A\_0$ into the GCH pattern above $\lambda\_0$. This preserves the
definition of $A\_0$ by $\varphi\_0$, while ensuring that $A\_0$ has
an ordinal definable element. Now, let $\theta\_1$ be well above
this coding, and continue.


At stage $n$, we have the partial extension
$V^{(n)}=V[g\_0][h\_0]\cdots[g\_{n-1}][h\_{n-1}]$, which performed
forcing below the cardinal $\theta\_n$. We ask whether we can
perform $\leq\theta\_n$-forcing so that $\varphi\_n$ holds of a
nonempty set $A\_n$ in the extension. If so, we do that forcing,
let $\lambda\_n$ be large enough to witness the $\Sigma\_2$ property
for $\varphi\_n$, and then perform GCH coding above that so as to
make an element of $A\_n$ ordinal-definable, and let $\theta\_{n+1}$
larger than all that. (Otherwise, we ignore $\varphi\_n$ and let
$\theta\_{n+1}=\theta\_n$.)


Consider the corresponding extension $V[G]$, where $G\subset\P$ is
$V$-generic. Finally, we force to add a Cohen subset
$H\subset\delta$, where $\delta$ is a regular cardinal above
$\sup\_n\theta\_n$, since this will force $V\neq\HOD$ in $V[G][H]$.
The final desired model is $V[G][H]$. Because we used full
support, it follows that the tail forcing in $\P$ after stage $n$
is $\leq\theta\_n$-closed, as is the forcing to add $H$, and so
preserves sets of rank below $\lambda\_n$. Thus, if $\varphi\_n$
defines a nonempty set in $V[G][H]$, then at stage $n$ we would
have observed that it was possible to force it to hold of a
nonempty set (with forcing that was sufficiently closed), and so
we would have treated it at stage $n$. That is, we would have
forced to code one of its elements into the GCH pattern,
afterwards always preserving that definition and this coding. So
in the case that $\varphi\_n$ does define a nonempty set in
$V[G][H]$, then the stage $n$ forcing exactly ensured that one of
the elements of this set was coded into the GCH pattern of
$V[G][H]$ and was therefore ordinal-definable there. The later
stages of forcing were arranged so as to preserve all these
definitions.


Thus, $V[G][H]$ is a model of $V\neq\HOD$, as the forcing to add
$H$ is weakly homogeneous, such that every $\Sigma\_2$-definable
nonempty set has an ordinal-definable element. **QED**


The argument reminds me of the forcing iteration proof of the
[maximality principle](http://jdh.hamkins.org/maximalityprinciple/), where one forces a given statement to be
true, if it is possible to force it in such a way that it remains
true in all further forcing extensions. The end result is a model
where any statement that could become necessarily true by forcing,
is already true, and this is precisely what the maximality
principle asserts.


Meanwhile, Emil's insightful suggestion in the comments leads to a
negative answer to question 2.


**Theorem 2.** If $V\neq\HOD$, then there is a nonempty
$\Pi\_2$-definable set (with no parameters) containing no
ordinal-definable element.


**Proof.** Let $A$ be the set of minimal-rank non-OD sets. That is,
$A$ consists of all non-OD sets of rank $\alpha$, where $\alpha$
is minimal such that there is any non-OD set of rank $\alpha$. In
[my answer to this related question](https://mathoverflow.net/a/180734/1946), I had proved that $A$ is
characterized by a $\Sigma\_2\wedge\Pi\_2$ property.


Emil's idea was to consider not $A$, but a related set, namely the
set $U=A\times V\_\theta$, where $\theta$ is the smallest ordinal
such that $A\in V\_\theta$ and $V\_\theta\models A$ is the set of
minimal-rank non-OD sets.


The set $U$ is defined by the following property: $U$ consists of
the cartesian product $U=A\times B$ of two sets $A$ and $B$ such
that the set $B$ has the form $B=V\_\theta$ for some ordinal
$\theta$ such that $A\in V\_\theta$ and $V\_\theta\models "A$ is the
set of minimal-rank OD sets and there is no $\theta'<\theta$ for
which $V\_{\theta'}\models A$ is the set of minimal-rank non-OD
sets"; and finally, the elements of $A$ really are not in OD.


This property altogether has complexity $\Pi\_2$, due mainly to the
last clause. The first part, requiring that $U$ has the form
$A\times B$, is $\Delta\_0$. The next part, asserting that $B$ has
the form $B=V\_\theta$ for some ordinal $\theta$ has complexity
$\Pi\_1$, essentially because one need only assert that $B$ is
transitive and satisfies some minimal set theory such that it
thinks it is a $V\_\theta$, and such that $B$ contains all subsets
of any of its elements, so that it is using the true power set
operation. The properties asserting that $V\_\theta$, that is, $B$,
satisfies certain complication assertions has complexity
$\Delta\_0$, since all quantifiers are bounded by $B$ and hence
ultimately by $U$. And finally, asserting that the elements of $A$
are really not ordinal-definable has complexity $\Pi\_2$, since
"$x\in\text{OD}$'' has complexity $\Sigma\_2$, as any instance of
ordinal-definability reflects to some $V\_\theta$ and hence is
locally verifiable; thus, the assertion $\forall x\in A\
x\notin\text{OD}$ has complexity $\Pi\_2$.


So altogether, the set $U=A\times V\_\theta$ is $\Pi\_2$-definable,
but it can have no ordinal-definable elements, since every element
of $U$ has the form $(a,b)$ for some $a\in A, b\in V\_\theta$, and
if the pair $(a,b)$ were ordinal-definable, then $a$ would be
ordinal-definable, contradicting $a\in A$ and the fact that every
member of $A$ is not ordinal-definable. **QED**


Note that the proof is completely uniform, in that the definition
of the set does not depend on the model in any way. Rather, we
have a $\Pi\_2$ definition that $\ZFC+V\neq\HOD$ proves is a
nonempty set disjoint from OD.


