I was wondering if there is a property that is known to be satisfied for certain "things" but for which we do not know any explicit example.

More explicitly (also more restrictive but possibly easier):

Is there a set $S \subseteq \mathbb{N}$ for which one can prove that $S \neq \varnothing$ and yet there is no known (to us, humans, at this point in time) element of $S$?

  • $\begingroup$ Plenty of singleton sets here: math.stackexchange.com/questions/1315615/… $\endgroup$ – JP McCarthy Jul 21 '15 at 18:29
  • $\begingroup$ Every theorem that states the existence of some constant in a non-effective way would qualify. For example (though in $\Bbb{R}$, and not in $\Bbb{N}$) in 2002 Becher and Figueira showed the existence of some computable normal numbers. While they do provide an algorithm, it is so inefficient that no digits of any of those numbers are known. $\endgroup$ – A.P. Jul 21 '15 at 18:33
  • $\begingroup$ @Pedro: I don't know if this is really about constructive mathematics. $\endgroup$ – Asaf Karagila Jul 21 '15 at 18:35
  • $\begingroup$ @AsafKaragila I voted to reopen... this is not a duplicate of that question... that question is arguably a subquestion of this one. $\endgroup$ – JP McCarthy Jul 21 '15 at 18:37
  • $\begingroup$ We know that non-measurable sets exist, but they are not constructable. $\endgroup$ – Alex S Jul 21 '15 at 18:38

There is a definite difference between two kinds of mathematical proof: construction and existence. A proof is constructive if you claim that there are "things" that satisfy a property and prove this by giving an explicit example of such a "thing." A proof is an existence proof if you claim that there are "things" that satisfy a property but do not show an explicit example of such. The proof of the claim is usually done by showing that if such a thing did not exist, we would have a contradiction. Before the advent of modern computing, many things were shown to exist but not explicitly. One example is from Godel's Incompleteness Theorem, which states that there is a statement in Peano Arithmetic that is true but not provable in Peano Arithmetic (we know its true, but we can't prove it). This was an iconic existence proof, but now there exists an explicit example.

| cite | improve this answer | |

Not the answer you're looking for? Browse other questions tagged or ask your own question.