MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).
show/hide this revision's text 1 [made Community Wiki]

There is the standard example involving Fermat's Last Theorem, except that we now have a good idea what the set is. So let's replace it with "the smallest positive integer n which is a multiple of 4 and for which no Hadamard matrix of order n exists, or 1 if Hadamard matrices of all possible orders exist." This defines a singleton set, which is decidable. You could argue that in principle it is constructive, whereas I would argue that since we still don't know maximal determinants for small orders less than 100, you and your putative great-grandchildren will not see a value for n, so you will have a hard time showing to me that a construction based on this definition exists, as there is no guarantee of termination of the construction.

Alternatively, any finite set which is arrived at by nonconstructive means (E.g. encodings of counterexamples to Frankl's union-closed families conjecture, where the presumed proof that there are only finitely many is nonconstructive) should count as an example.

Better answers will arise once a good notion of nonconstructive has been specified. As to such a notion, I'll leave the philosophical wrangling to others.

Gerhard "Ask Me About System Design" Paseman, 2010.02.10