Hay una forma estándar para la construcción de estas cosas en la lógica clásica. Tu pregunta es la misma como "si sabemos que al menos uno de los $x$ satisface $Z$, podemos encontrar un ejemplo de una $x$ que satisface $Z$" y voy a trabajar con la versión positiva.
En primer lugar, elegir algunos bien definido, sin ambigüedades, a cuya verdad no es conocido en el momento. Por ejemplo, P=NP o la conjetura de Hodge. Ahora podemos probar que existe un número natural $x$ con la siguiente propiedad: "Si P=NP, a continuación, $x=1$ e lo contrario $x=0$". Pero no podemos dar un ejemplo claro de una $x$ con esa propiedad.
En realidad podemos hacer que la propiedad incluso más elementales cambiando a "Si ZFC demuestra que P=NP, a continuación, $x=1$ e lo contrario $x=0$". Que sólo tiene un cuantificador, más de ZFC-pruebas, que puede ser considerado como un cuantificador más números naturales si las pruebas son representados por números. Como antes, "P=NP" puede ser reemplazado por cualquier sin resolver, sin ambigüedades, de conjeturas, por ejemplo, la conjetura de Hodge, y la frase final es todavía una frase acerca de los números naturales.
El punto de este ejemplo es que se evita cualquier dificultad con innumerables conjuntos, el axioma de elección, etc. La existencia de ejemplos como el de esta muestra que, como los sistemas de PA y ZFC no tienen el testimonio de la propiedad [1]. Que es, sólo porque usted puede demostrar que una fórmula de la forma $(\exists x)\phi(x)$ no significa que hay un tipo específico de $t$ de manera tal que usted puede probar $\phi(t)$. Uno de los beneficios de los sistemas constructivos es que no tienen el testimonio de la propiedad (lo que significa que usted siempre puede encontrar un $t$) y esta es una razón por la que es interesante preguntarse ¿qué tipo de matemáticas que se puede probar en dichos sistemas.
1: http://en.wikipedia.org/wiki/Disjunction_and_existence_properties