There is a standard way to construct these things in classical logic. Your question is the same as "if we know that at least one $x$ satisfies $Z$, can we find an example of an $x$ that satisfies $Z$" and I'll work with the positive version.
First, choose some well-defined, unambiguous statement whose truth is not known at the moment. For example, P=NP or the Hodge conjecture. Now we can prove there is a natural number $x$ with the following property: "If P=NP then $x=1$ and otherwise $x=0$". But we can't give an explicit example of an $x$ with that property.
We can actually make the property even more elementary by changing it to "If ZFC proves P=NP then $x=1$ and otherwise $x=0$". That has only one quantifier, over ZFC-proofs, which can be regarded as one quantifier over natural numbers if proofs are represented by numbers. As before, "P=NP" can be replaced with any unsolved, unambiguous conjecture, e.g. the Hodge conjecture, and the final sentence is still a sentence just about natural numbers.
The point of this example is that it avoids any difficulties with uncountable sets, the axiom of choice, etc. The existence of examples like this shows that systems like PA and ZFC do not have the witness property . That is, just because you can prove a formula of the form $(\exists x)\phi(x)$ does not mean that there is a specific $t$ such that you can prove $\phi(t)$. One of the benefits of constructive systems is that they do have the witness property (meaning you always can find such a $t$) and this is one reason that it's interesting to ask what sorts of mathematics can be proved in such systems.