11
$\begingroup$

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.

4 Answers 4

13

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

  • 0
    Question: What if we prove P=NP or the Hodge conjecture or the open problem at hand? Then wouldn't their provability be provable in ZFC (or PA)? And if so wouldn't we be able to find a witness for the statement (either $1$ or $0$)? Or am I missing something?2011-03-10
  • 0
    No, you're not missing anything. The question asked "but there are currently no examples", and I aimed at that here. There is a completely different answer for the question "but there could never be any explicit examples", based on the study of definability.2011-03-10
  • 0
    @Carl: I see. Thanks for clarifying this for me. :)2011-03-10
  • 1
    If you prove the existence of a specific natural number $x$, how can you say "If some condition A, then $x = 1$ otherwise $x = 0$"? That is, you say you can't give an explicit example of such an $x$ but you just argued that it's either $0$ or $1$; aren't one of these an explicit example even if we can't prove which it is?2011-03-16
  • 0
    @Michael Burge, that is not explicit, right? To be explicit, you have to tell me which one, otherwise giving a list of objects and saying one of these is what you are looking for is not explicit.2011-03-17
  • 0
    @Carl, nitpicking: not all "constructive systems" have these properties.2011-03-17
  • 0
    @Kaveh: "constructive" is used in so many ways that it only has meaning in context. However, a wide variety of systems do have the existence and disjunction properties, including examples of constructive arithmetics (e.g. HA), constructive type theories (e.g Martin-Lof), and constructive set theories (e.g. CZF). The BHK interpretation also requires these properties. So if a particular system doesn't have the existence and disjunction properties, its credibility as a "constructive" system is diminished compared to the systems just listed.2011-03-18
  • 0
    @Michael Burge: in the way constructivists would tend to think, an "explicit example" is defined as an object $o$ accompanied by a proof that $o$ is an example of the property in question. That's the way I was using the term here.2011-03-18
  • 0
    @Carl, yes, IIRC, there are a number of examples in van Dalen and Troelstra where the system is constructive but does not satisfy these properties, and again IIRC they argue that these properties should not be the base of judgment for constructiveness of a system.2011-03-18
  • 0
    I don't have the book at hand - can you give an example of such a system that is clearly "constructive"? Do you remember which part of the book this was in - I'm interested to see what they say.2011-03-18
  • 0
    "Many authors have treated ED and DP as necessary (and sometimes also as sufficient) conditions for a system to be "constructive". This view seems to be ill-founded: for example, if a formal system S proves $A \lor B$ and is constructively well motivated, the formal proof in S corresponds to an informal constructive proof of $A \lor B$ and hence there ought to be an informal constructive proof of either $A$ or $B$; but it does not follow that this informal proof of $A$ or $B$ should have a formal counterpart in S; that only follows if S has suitable closure properties.2011-03-18
  • 0
    In Troelstra (1973A) an example, due to Kreisel, is presented of an intuitionistically correct extension of HA which does not satisfy EDN." [vDT88, vol I, page 176]. There is more on that page but I cannot type it all. There is also some discussion on page 139. There might be more but that is what I could find at the moment and I don't have access to vol II right now to check if there is anything there.2011-03-18
  • 0
    Thanks a lot; I will look that up as soon as I can get a copy of the book from the library. Their comment about closure properties is certainly valid: constructive systems that somehow fail to encompass "sufficiently many constructive principles" may not have the properties, but it seems naively that these should be subsystems of stronger constructive theories that do have the properties. I'll need to look at Kreisel's example to see whether it can be extended to a system that does have these properties.2011-03-18
8

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."

  • 0
    You just beat me to it, Alex! And your first paragraph is almost identical to mine...2011-03-10
  • 2
    Note though that the construction, e.g. of a non-measurable subset of $\mathbb R$, is possible in ZFC. (There is some tension in the original question between the expression "explicit counterexample" and issue of whether a "construction is impossible in ZFC".)2011-03-10
0

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.

0

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".