Return to Answer

If ZF is consistent, then the answer is no.

ZF proves that there is an $x$ such that $P(x)$: either $x$ is an $L$-generic Cohen real or there is no $L$-generic such real. (Here, by $L$ I mean the constructible universe of Gödel.)

In a universe with $L$-generic Cohen reals, $P$ holds only of them, but in a universe without any $L$-generic Cohen reals, $P$ holds of everything.

But if ZF is consistent, then it cannot prove that there is a definable such object satisfying $P(x)$, because we may consider the forcing extension $L[c]$ obtained by adding an $L$-generic Cohen real. In such a model $L[c]$, which still satisfies ZF, the predicate $P$ holds only of the $L$-generic Cohen reals, but no such real is definable in $L[c]$ because the forcing is almost homogeneous, and consequently all ordinal definable objects of $L[c]$ are in the ground model $L$.

Since these are also ZFC models, they also serve to establish the claim you had made about ZFC having this phenomenon. Indeed, there can be no (parameter-free) definable well-ordering of the reals in $L[c]$, since in this case there would be a definable $L$-generic Cohen real, namely, the least one to appear in the well ordering. Meanwhile, in $L$ there is a $c$-definable well-ordering of $\mathbb{R}$, of complexity $\Delta^1_2(c)$, just as in $L$ there is a parameter-free $\Delta^1_2$ definable well ordering of $L$.

But actually, I've realized that any example from the ZFC case can be transformed to the ZF case by this procedure. In other words, suppose that $P$ has your property for ZFC. Let $P'(x)$ assert "either $P(x)$ or there are no instances of $P$". So ZF proves the existence of $x$ for which $P'(x)$. But there can be no $Q$ that ZF proves to define such an $x$, since such a $Q$ would also ZFC-provably define an $x$ for which $P(x)$, which we had assumed was not the case.

Indeed, as mentioned by Rodrigo in the comments, any subtheory of ZFC at all proves $\exists x\ P'(x)$, but no such theory can prove that there is a definable such $x$, since we assumed that ZFC itself does not prove that there is a definable $x$ for which $P(x)$.

If ZF is consistent, then the answer is no.

ZF proves that there is an $x$ such that $P(x)$: either $x$ is an $L$-generic Cohen real or there is no $L$-generic such real. (Here, by $L$ I mean the constructible universe of Gödel.)

In a universe with $L$-generic Cohen reals, $P$ holds only of them, but in a universe without any $L$-generic Cohen reals, $P$ holds of everything.

But if ZF is consistent, then it cannot prove that there is a definable such object satisfying $P(x)$, because we may consider the forcing extension $L[c]$ obtained by adding an $L$-generic Cohen real. In such a model $L[c]$, which still satisfies ZF, the predicate $P$ holds only of the $L$-generic Cohen reals, but no such real is definable in $L[c]$ because the forcing is almost homogeneous, and consequently all ordinal definable objects of $L[c]$ are in the ground model $L$.

Since these are also ZFC models, they also serve to establish the claim you had made about ZFC having this phenomenon. Indeed, there can be no (parameter-free) definable well-ordering of the reals in $L[c]$, since in this case there would be a definable $L$-generic Cohen real, namely, the least one to appear in the well ordering. Meanwhile, in $L[c]$ there is a $c$-definable well-ordering of $\mathbb{R}$, of complexity $\Delta^1_2(c)$, just as in $L$ there is a parameter-free $\Delta^1_2$ definable well ordering of $L$.

But actually, I've realized that any example from the ZFC case can be transformed to the ZF case by this procedure. In other words, suppose that $P$ has your property for ZFC. Let $P'(x)$ assert "either $P(x)$ or there are no instances of $P$". So ZF proves the existence of $x$ for which $P'(x)$. But there can be no $Q$ that ZF proves to define such an $x$, since such a $Q$ would also ZFC-provably define an $x$ for which $P(x)$, which we had assumed was not the case.

Indeed, as mentioned by Rodrigo in the comments, any subtheory of ZFC at all proves $\exists x\ P'(x)$, but no such theory can prove that there is a definable such $x$, since we assumed that ZFC itself does not prove that there is a definable $x$ for which $P(x)$.

If ZF is consistent, then the answer is no.

ZF proves that there is an $x$ such that $P(x)$: either $x$ is an $L$-generic Cohen real or there is no $L$-generic such real. (Here, by $L$ I mean the constructible universe of Gödel.)

In a universe with $L$-generic Cohen reals, $P$ holds only of them, but in a universe without any $L$-generic Cohen reals, $P$ holds of everything.

But if ZF is consistent, then it cannot prove that there is a definable such object satisfying $P(x)$, because we may consider the forcing extension $L[c]$ obtained by adding an $L$-generic Cohen real. In such a model $L[c]$, which still satisfies ZF, the predicate $P$ holds only of the $L$-generic Cohen reals, but no such real is definable in $L[c]$ because the forcing is almost homogeneous, and consequently all ordinal definable objects of $L[c]$ are in the ground model $L$.

Since these are also ZFC models, they also serve to establish the claim you had made about ZFC having this phenomenon. Indeed, there can be no (parameter-free) definable well-ordering of the reals in $L[c]$, since in this case there would be a definable $L$-generic Cohen real, namely, the least one to appear in the well ordering. Meanwhile, in $L$ there is a $c$-definable well-ordering of $\mathbb{R}$, of complexity $\Delta^1_2(c)$, just as in $L$ there is a parameter-free $\Delta^1_2$ definable well ordering of $L$.

But actually, I've realized that any example from the ZFC case can be transformed to the ZF case by this procedure. In other words, suppose that $P$ has your property for ZFC. Let $P'(x)$ assert "if AC holds, then $P(x)$". So ZF proves the existence of $x$ for which $P'(x)$. But there can be no $Q$ that ZF proves to define such an $x$, since such a $Q$ would also ZFC-provably define an $x$ for which $P(x)$, which we had assumed was not the case.

This argument shows that removing finitely many axioms cannot destroy your property.

If ZF is consistent, then the answer is no.

ZF proves that there is an $x$ such that $P(x)$: either $x$ is an $L$-generic Cohen real or there is no $L$-generic such real. (Here, by $L$ I mean the constructible universe of Gödel.)

In a universe with $L$-generic Cohen reals, $P$ holds only of them, but in a universe without any $L$-generic Cohen reals, $P$ holds of everything.

But if ZF is consistent, then it cannot prove that there is a definable such object satisfying $P(x)$, because we may consider the forcing extension $L[c]$ obtained by adding an $L$-generic Cohen real. In such a model $L[c]$, which still satisfies ZF, the predicate $P$ holds only of the $L$-generic Cohen reals, but no such real is definable in $L[c]$ because the forcing is almost homogeneous, and consequently all ordinal definable objects of $L[c]$ are in the ground model $L$.

Since these are also ZFC models, they also serve to establish the claim you had made about ZFC having this phenomenon. Indeed, there can be no (parameter-free) definable well-ordering of the reals in $L[c]$, since in this case there would be a definable $L$-generic Cohen real, namely, the least one to appear in the well ordering. Meanwhile, in $L$ there is a $c$-definable well-ordering of $\mathbb{R}$, of complexity $\Delta^1_2(c)$, just as in $L$ there is a parameter-free $\Delta^1_2$ definable well ordering of $L$.

But actually, I've realized that any example from the ZFC case can be transformed to the ZF case by this procedure. In other words, suppose that $P$ has your property for ZFC. Let $P'(x)$ assert "either $P(x)$ or there are no instances of $P$". So ZF proves the existence of $x$ for which $P'(x)$. But there can be no $Q$ that ZF proves to define such an $x$, since such a $Q$ would also ZFC-provably define an $x$ for which $P(x)$, which we had assumed was not the case.

Indeed, as mentioned by Rodrigo in the comments, any subtheory of ZFC at all proves $\exists x\ P'(x)$, but no such theory can prove that there is a definable such $x$, since we assumed that ZFC itself does not prove that there is a definable $x$ for which $P(x)$.

If ZF is consistent, then the answer is no.

ZF proves that there is an $x$ such that $P(x)$: either $x$ is an $L$-generic Cohen real or there is no $L$-generic such real. (Here, by $L$ I mean the constructible universe of Gödel.)

In a universe with $L$-generic Cohen reals, $P$ holds only of them, but in a universe without any $L$-generic Cohen reals, $P$ holds of everything.

But if ZF is consistent, then it cannot prove that there is a definable such object satisfying $P(x)$, because we may consider the forcing extension $L[c]$ obtained by adding an $L$-generic Cohen real. In such a model $L[c]$, which still satisfies ZF, the predicate $P$ holds only of the $L$-generic Cohen reals, but no such real is definable in $L[c]$ because the forcing is almost homogeneous, and consequently all ordinal definable objects of $L[c]$ are in the ground model $L$.

Since these are also ZFC models, they also serve to establish the claim you had made about ZFC having this phenomenon. Indeed, there can be no (parameter-free) definable well-ordering of the reals in $L[c]$, since in this case there would be a definable $L$-generic Cohen real, namely, the least one to appear in the well ordering. Meanwhile, in $L$ there is a $c$-definable well-ordering of $\mathbb{R}$, of complexity $\Delta^1_2(c)$, just as in $L$ there is a parameter-free $\Delta^1_2$ definable well ordering of $L$.

If ZF is consistent, then the answer is no.

ZF proves that there is an $x$ such that $P(x)$: either $x$ is an $L$-generic Cohen real or there is no $L$-generic such real. (Here, by $L$ I mean the constructible universe of Gödel.)

In a universe with $L$-generic Cohen reals, $P$ holds only of them, but in a universe without any $L$-generic Cohen reals, $P$ holds of everything.

But if ZF is consistent, then it cannot prove that there is a definable such object satisfying $P(x)$, because we may consider the forcing extension $L[c]$ obtained by adding an $L$-generic Cohen real. In such a model $L[c]$, which still satisfies ZF, the predicate $P$ holds only of the $L$-generic Cohen reals, but no such real is definable in $L[c]$ because the forcing is almost homogeneous, and consequently all ordinal definable objects of $L[c]$ are in the ground model $L$.

Since these are also ZFC models, they also serve to establish the claim you had made about ZFC having this phenomenon. Indeed, there can be no (parameter-free) definable well-ordering of the reals in $L[c]$, since in this case there would be a definable $L$-generic Cohen real, namely, the least one to appear in the well ordering. Meanwhile, in $L$ there is a $c$-definable well-ordering of $\mathbb{R}$, of complexity $\Delta^1_2(c)$, just as in $L$ there is a parameter-free $\Delta^1_2$ definable well ordering of $L$.

But actually, I've realized that any example from the ZFC case can be transformed to the ZF case by this procedure. In other words, suppose that $P$ has your property for ZFC. Let $P'(x)$ assert "if AC holds, then $P(x)$". So ZF proves the existence of $x$ for which $P'(x)$. But there can be no $Q$ that ZF proves to define such an $x$, since such a $Q$ would also ZFC-provably define an $x$ for which $P(x)$, which we had assumed was not the case.

This argument shows that removing finitely many axioms cannot destroy your property.