Statements with no counterexample Is there some proven statement that tells us "not all X satisfy Y", but there are currently no examples of X which do not satisfy Y?
Is it necessarily true that there are always explicit counterexamples? Or are there statements that only guarantee the existence of such counterexamples, whose construction is impossible in ZFC.
 A: The statement "not all X satisfy Y" ($\lnot \forall X\,Y(X)$) is equivalent to "there is an X such that Y is not true of X" ($\exists X\,\lnot Y(X)$), which is equivalent to "there is an X such that 'not Y' is true of X" ($\exists X\,(\lnot Y)(X)$).
That is, for any proposition $Y$, asking for an explicit counterexample for $Y$ is the same as asking for an explicit example of the negation of $Y$.
There are many existence results for which no explicit example is known. In particular, for any such result relying strongly on the Axiom of Choice, we cannot explicitly construct an example. And any such existence result can be rephrased as an example of what you are asking for simply by taking the negation of the property in question.
For example, "There exists a nonmeasurable subset of $\mathbb{R}$" can be rephrased as "Not all subsets of $\mathbb{R}$ are measurable."
A: At least one of the numbers $\pi e$, $\pi+e$ is irrational. But we don't know which (yet).
So in your notation, let $X=\{\pi e,\pi+e\}$, and let $Y$ be the statement "$x$ is rational".
A: 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 [1]. 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. 
1: http://en.wikipedia.org/wiki/Disjunction_and_existence_properties
A: Cheat: both the universal and existential quantifiers require a "universal set" of discussion, although this is often omitted.
If you choose your universal set as the empty set, I the seemingly contradictory conditions are both vacuously true.
