31
$\begingroup$

This question isn't related to any specific research. I've been thinking a bit about how existence theorems are generally proven, and I've identified three broad categories: constructive proofs, proofs involving contradiction/contrapositive, and proofs involving the axiom of choice.

I'm convinced that there must be some existence theorem that can be proven without any of these techniques (and I'm fairly confident that I've probably encountered some myself in the past haha), but I can't come up with any examples at the moment. Can anyone else come up with one? I'd also like to stipulate the following conditions:

  1. The proof can't piggyback on another existence theorem whose proof involves one of the above-mentioned devices.
  2. It has to be a theorem of ZF - no exotic and "high power" axioms allowed!

Now for the interesting question: is there any existence theorem (again in ZF) such that every one of its proofs is of this type? Has anyone investigated something like this? If so, what results exist?

Edit: This issue came up a few times in the comments: here I use "constructive" in its weaker sense (i.e. a constructive proof is merely one that constructs an object and shows that it satisfies the required properties). The stronger sense - that the proof may not use the law of excluded middle or involve any infinite objects - is not what I'm invoking.

Improve this question
$\endgroup$
25
  • 5
    $\begingroup$ To make this question precise, you would need to carefully define what you mean by "constructive proof". $\endgroup$
    – Alex Kruckman
    Commented Oct 10, 2018 at 1:13
  • 9
    $\begingroup$ @Francois The point is that you exhibit an explicit object (in your example, 5). $\endgroup$
    – Andrés E. Caicedo
    Commented Oct 10, 2018 at 2:17
  • 15
    $\begingroup$ Maybe proofs using the probabilistic method might count. They're not constructive and they don't involve the axiom of choice but it's a bit unclear to me how to evaluate whether they use contradiction / contrapositive (these are really not similar at all, by the way; in a proof by contrapositive every statement you write down along the way is still true, unlike in a proof by contradiction). $\endgroup$
    – Qiaochu Yuan
    Commented Oct 10, 2018 at 5:47
  • 6
    $\begingroup$ I would call an existence proof constructive if it constructs an item with the appropriate properties, e.g., if it constructs a real irrational (or trranscendental). Showing a mismatch of cardinality or measure does not construct such a number. Similarly, using the Pigeonhole Principle to prove that in any collection of 13 people there are two who were born in the same month of the year is not (to my way of thinking) constructive, since it does not find the two people, or even the month. $\endgroup$
    – Gerry Myerson
    Commented Oct 10, 2018 at 9:03
  • 7
    $\begingroup$ @Dirk But typical proofs of uncountability do not seem to be by contradiction: given an enumeration, you explicitly exhibit a real not in the list, for instance. (It seems like splitting hairs in any case.) $\endgroup$
    – Andrés E. Caicedo
    Commented Oct 10, 2018 at 11:28

9 Answers 9

Reset to default
51
$\begingroup$

There are probabilistic proofs of existence. Do they fall into one of your three categories?

For example, prove the existence of a real number that is normal in all bases: To do it, we show that "almost all" real numbers (according to Lebesgue measure) have that property. Therefore at least one real number has the property. And the point is: this "almost all" proof is easier than constructing an explicit example.

See some nice examples due to Erdős in the cited Wikipedia page which use only finite probability spaces. If we show that a probability is ${} > 0$, then the set is not empty.

Improve this answer
$\endgroup$
8
  • 4
    $\begingroup$ I thought of that, but it's a kind of proof by contradiction -- the sum (or integral) over the set is positive, so if the set were empty we'd get 0>0. $\endgroup$
    – Noam D. Elkies
    Commented Oct 10, 2018 at 16:04
  • 8
    $\begingroup$ @NoamD.Elkies you could phrase it that way, but I feel these are better described as "nondeterministic constructive proofs". We construct the object via a sequence of choices. Then we show that there exists a sequence of choices we could have made such that the construction satisfies the criteria. (In fact we show the measure of such choices is 1 or is nonzero.) $\endgroup$
    – usul
    Commented Oct 10, 2018 at 18:09
  • $\begingroup$ @usul I think “nondeterministic constructions” definitely have a place in this discussion. I was thinking of such algorithms myself when writing this question myself. There are certainly algorithms of this type that I would call “essentially” constructive. I’d love if someone could present an example of such an algorithm that’s so [abstract?] that its debatable whether it should be thought of as constructive at all $\endgroup$
    – Joseph Granata
    Commented Oct 10, 2018 at 20:35
  • 1
    $\begingroup$ Erdős is spelt with an 'ő', not 'ō'. $\endgroup$
    – AJF
    Commented Oct 11, 2018 at 9:21
  • $\begingroup$ @AJFarmar: Stupid Mac only gives me these choices ô ö ò ó œ ø ō õ so I chose the closest one. Good enough for quick typing. Otherwise I would have to find the one I want in a more complicated way. I now see I could have copied and pasted Erdős from the web page I refer to. Fixed. $\endgroup$
    – Gerald Edgar
    Commented Oct 11, 2018 at 11:46
27
$\begingroup$

There is a famous proof of the existence of two irrational numbers $a$ and $b$ such that $a^b$ is rational. The proof considers two cases: $\sqrt{2}^\sqrt{2}$ is irrational, or it is rational. In either case we can find such $a$, $b$. Then it applies the law of excluded middle to say one of these cases in fact holds. You can see a discussion of the proof here: http://math.andrej.com/2009/12/28/constructive-gem-irrational-to-the-power-of-irrational-that-is-rational/.

You mentioned “proof by contradiction” in your question, but to me this application of the law of the excluded middle is conceptually different than proof by contradiction.

(By the way, as discussed in that blog post, this is certainly not a serious application of the law of excluded middle because there are other ways to prove the result in question. But it is a cute proof.)

EDIT: I believe there might be more serious proofs along these lines in number theory, that go something like “either the Riemann hypothesis holds, or it doesn’t. In the first case...; in the second case...” Or the same but with “Siegel zero existing.” But I don’t know a particular example off the top of my head.

Improve this answer
$\endgroup$
11
  • 1
    $\begingroup$ I was not sure if this counted as a proof by contradiction to the OP, but I also think it is a different kind of proof, just a proof by cases. Similarly, I think there are some results I can't remember where the proof goes by cases depending on whether the continuum hypothesis holds, but in each case the same result is obtained. $\endgroup$
    – Carl Mummert
    Commented Oct 10, 2018 at 16:02
  • 3
    $\begingroup$ Gauss' conjecture on class numbers of imaginary quadratic fields is an example of something that was first proved by showing that it's a consequence of both the (generalized) Riemann hypothesis and of its negation. $\endgroup$
    – Gerry Myerson
    Commented Oct 10, 2018 at 20:49
  • 1
    $\begingroup$ @GerryMyerson, that first proof the class number conjecture was not about GRH and its negation, but more precisely about GRH for $L$-functions of imaginary quadratic fields or its negation. The proof couldn't make any use of a hypothetical counterexample to GRH for some other type of $L$-function. $\endgroup$
    – KConrad
    Commented Oct 11, 2018 at 22:58
  • 1
    $\begingroup$ @CarlMummert The scheme $\bot\to\phi$ is not proof by contradiction, it is the principle of explosion or ex falso quodlibet. Proof of $\neg\phi$ by assuming $\phi$ and deducing $\bot$ is also not a proof by contradiction, although this is often mistaken for proof by contradiction. I don't think this proof principle has a special name, it's just the definition of $\neg$. I guess you could call it negation introduction? $\endgroup$
    – Mario Carneiro
    Commented Oct 11, 2018 at 23:46
  • 1
    $\begingroup$ Here's what's different about this proof and the strategy-stealing one below. Explicitly construct candidate A. Case 1, A satisfies the criteria. Case 2, leverage A to construct new candidate B and proves B works using the assumption that A is a nonexample. We end with a pair of candidates one of which works, but no guarantee which. So it's "partially constructive", especially depending on the magic that gave us B. I think excluded middle is somewhat of a red herring (it can be proven constructively in some cases), as are mere proofs of the form "Assume P. Or assume not P. In both cases Q." $\endgroup$
    – usul
    Commented Oct 12, 2018 at 17:54
22
$\begingroup$

This is the strangest existence proof I know; it is a nonconstructive proof that there exists a proof of a certain statement. In other words, we prove the statement by proving that a proof exists.

I'm thinking of Lob's theorem. The Godel sentence is a number-theoretic assertion $G$ which informally says of itself that it cannot be proven in Peano Arithmetic (PA). Godel showed that if PA is $\omega$-consistent, then $G$ is true but there is no proof of $G$ in PA.

The Lob sentence $L$ is the analogous assertion which informally says of itself that it can be proven in PA. Is it true or false?

It is true. For suppose $L$ cannot be proven in PA. Then the system PA' = PA + $\neg L$ is consistent. But it is clear, and can be proven in PA, that if $L$ is provable in PA then $L$ is true. Since PA' assumes $\neg L$, we can therefore prove in PA' that $L$ is not provable in PA. Thus we can prove in PA' that PA + $\neg L$, i.e., PA' itself, is consistent. By Godel's second incompleteness theorem this is impossible, since we already knew that PA' is consistent (a consistent theory cannot prove its own consistency). Therefore the assumption that $L$ is not provable in PA leads to a contradiction, and we conclude that $L$ is provable in PA.

It's crazy because we know there is a proof of $L$ in PA but we don't know what that proof is!

So what is this mysterious proof of $L$? It is the argument I just gave, which can be formalized in PA.

That is the most bizarre existence proof I know.

Improve this answer
$\endgroup$
8
  • $\begingroup$ If, as you said, the argument you just gave can be formalized in PA, then isn't it in fact just a "proof of L" and not a "nonconstructive proof that there exists a proof of L"? $\endgroup$
    – Sam Hopkins
    Commented Oct 12, 2018 at 10:10
  • 2
    $\begingroup$ If the above argument can be formalized in PA, why is it fair to say that "we don't know what that proof is"? $\endgroup$
    – Qfwfq
    Commented Oct 12, 2018 at 10:31
  • 7
    $\begingroup$ The point is that the argument shows that there is a proof but does not tell us what it is. But it is itself the proof that it nonconstructively finds! So yes, in fact we do know what the proof is, but it does not tell us this. $\endgroup$
    – Nik Weaver
    Commented Oct 12, 2018 at 12:02
  • 3
    $\begingroup$ @Sam_Hopkins: it is both. $\endgroup$
    – Nik Weaver
    Commented Oct 12, 2018 at 12:03
  • 10
    $\begingroup$ Great example. Perhaps one way to answer the questions of Sam Hopkins and Qfwfq is to distinguish between the "informal" argument P that establishes the existence of a PA-proof of L, and the formalization P' of P in PA. The informal argument doesn't tell you how to construct a PA-proof of L. To construct a PA-proof of L, it has to occur to you to take the informal argument P and formalize it as P'. P does not construct its own formalization; rather, just by "being itself" it provides the raw material for a constructive proof. $\endgroup$
    – Timothy Chow
    Commented Oct 12, 2018 at 20:41
16
$\begingroup$

Many existence proofs in analysis / probability follow this line of argument: 1. Construct a family of objects that approximately satisfy some desired property. 2. Show that the family is precompact. 3. Show that every accumulation point must satisfy the desired property. I suppose that to some extent this would often count as a constructive proof since in many cases one can impose additional constraints until the possible limits are reduced to a single point, but this may require some non-trivial amount of work...

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ I was not sure whether this would count as constructive, or whether it would be viewed as using the axiom of choice somehow. Certainly it would be constructive if it was possible to construct approximations to a single limiting object. $\endgroup$
    – Carl Mummert
    Commented Oct 10, 2018 at 19:33
  • $\begingroup$ I too was considering a similar point when writing the question. I think this relates to @usul’s discussion of “nondeteministic constructive algorithm” A few answers up. I’m not sure yet where I stand on whether these are examples or nonexamples $\endgroup$
    – Joseph Granata
    Commented Oct 10, 2018 at 20:55
  • $\begingroup$ I think the key here is how you show the family is precompact, because this is where the exists is. (It claims that every sequence has some accumulation point, or every open cover has a finite subcover, or every filter has a limit point - no matter how you slice it it's an existence claim.) Unless you are using Heine-Borel in which case the construction comes from Heine-Borel itself which is using (countable) choice. $\endgroup$
    – Mario Carneiro
    Commented Oct 12, 2018 at 0:20
14
$\begingroup$

While an informal interpretation of the question seems more appropriate, a formal one is possible, too. We then enter the realm of constructive reverse mathematics.

It is (reasonably) clear what it means that a theorem has a constructive proof.

"All proofs of the theorem make use of contradiction" can be formalized as "the theorem implies some form of double-negation elimination over a weak base system (eg BISH)."

Thus, every non-constructive theorem that does not imply a form of DNE would count as an example.

Famous examples here would be weak Konigs Lemma (every infinite binary tree has an infinite path) and the intermediate value theorem.

Looking at eg the proof of the latter via bisection, we see a hybrid between constructive proof and proof by contradiction. We expect bisection to work, and then see that it can only fail if we hit upon a root one of the midpoints.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Actually, I was hoping to attack the question from a more formal perspective like you are suggesting. I’m not very familiar with proof theory, though - when you say double-negation-elimination, is that not the same as applying the law of excluded middle? I personally don’t view that as a form of contradiction; what’s your perspective on it? $\endgroup$
    – Joseph Granata
    Commented Oct 10, 2018 at 20:49
  • 2
    $\begingroup$ The constructive reading of $\neg \phi$ is $\phi \Rightarrow \bot$, i.e.~ that $\phi$ implies a contradiction. A proof by contradiction shows that $\neg \phi \Rightarrow \bot$, and hence constructively shows that $\neg \neg \phi$ holds. So the gap between a proof by contradiction and a constructive proof is just double-negation elimination, which is being allowed to deduce $\phi$ from $\neg \neg \phi$. $\endgroup$
    – Arno
    Commented Oct 11, 2018 at 7:39
  • 1
    $\begingroup$ @JosephGranata: Let C be classical propositional logic, and M be minimal logic, and EX be Ex Falso, and DNE be double-negation-elimination, and LEM be law of excluded middle. Then M+EX+LEM = M+DNE = C, but M+EX is intuitionistic logic, and M+LEM is not strong enough to prove EX. When you go on to quantifiers, there is an even greater variety of principles such as Markov's principle. $\endgroup$
    – user21820
    Commented Oct 12, 2018 at 16:53
10
$\begingroup$

I would call the proof for the existence of the limit $0$ of the Goodstein sequence pretty weird: it uses infinite ordinals, but the sequence itself is within $\mathbb{N}$. In Peano artithmetic, Goodstein's theorem is unprovable.

Improve this answer
$\endgroup$
6
  • 1
    $\begingroup$ I view this as an example of "moving to a higher space" in order to prove something. In Goodstein's theorem we move from the naturals to the collection of countable ordinals. Another example is in dynamical systems, when we begin with a compact dynamical system and move to the enveloping semigroup, or when we work with the Stone-Cech compactification of the naturals in combinatorics. $\endgroup$
    – Carl Mummert
    Commented Oct 10, 2018 at 16:05
  • $\begingroup$ Related: Kruskal's tree theorem and TREE(3) $\endgroup$
    – Ben Burns
    Commented Oct 10, 2018 at 16:28
  • 3
    $\begingroup$ I'm not too clear on how this type of answer avoids the "no piggy-backing" criterion. Can someone elucidate? $\endgroup$
    – Todd Trimble
    Commented Oct 10, 2018 at 17:24
  • 2
    $\begingroup$ @arsmath: presumably, the fact that every decreasing sequence of ordinals must come to an end, if we view that as an existence theorem. $\endgroup$
    – Carl Mummert
    Commented Oct 12, 2018 at 1:32
  • 1
    $\begingroup$ @CarlMummert That's not so much more than "a well-ordered set has a minimal element", is it? $\endgroup$
    – Hagen von Eitzen
    Commented Oct 13, 2018 at 10:49
6
$\begingroup$

How do you classify the proof that Chomp is a first player win? It's nonconstructive. It uses excluded middle, but it isn't a proof by contradiction.

Improve this answer
$\endgroup$
4
  • 5
    $\begingroup$ "Strategy-stealing" arguments seem to be proof by contradiction to me. Suppose player 2 has a winning strategy, then player 1 can win as follows; contradiction. Would you describe it differently? $\endgroup$
    – usul
    Commented Oct 10, 2018 at 18:35
  • 2
    $\begingroup$ Move X is either a win for the first player or it's a loss for the first player. If it is a loss, then the first player has an alternate move that is a win. $\endgroup$
    – ralphmerridew
    Commented Oct 10, 2018 at 19:58
  • $\begingroup$ @usul And to complete Mark's argument, the determinacy of finite games (which is needed to say "Move X is either a win for the first player or it's a loss for the first player") is constructive: it's just induction on rank. $\endgroup$
    – Noah Schweber
    Commented Oct 11, 2018 at 15:35
  • $\begingroup$ Okay great, now I agree! (I think you can improve your answer by adding some detail/clarification.) Maybe we can consider this proof strategy similar to the answer of Sam Hopkins mathoverflow.net/a/312480/29697 $\endgroup$
    – usul
    Commented Oct 11, 2018 at 17:36
5
$\begingroup$

There are many existence proofs that are "constructive" in the weak sense that they show that if you perform some kind of exhaustive search for the object then the search will always succeed, but are "nonconstructive" in the sense that they do not describe an explicit example of the object in question, and typically the exhaustive search is infeasible in practice. Probabilistic proofs, mentioned in another answer, are an example, but there are others.

  1. Counting arguments. Others have mentioned some of these; another example is the proof of the existence of a bijection between the set of conjugacy classes of a finite group and the set of non-isomorphic irreducible finite-dimensional complex representations of the group. This is usually proved by showing that irreducible characters form a basis for class functions, which is a dimension-counting argument. But the proof does not yield an explicit bijection and in general there is no canonical bijection.

  2. Pigeonhole arguments. One lesser-known example that I like arises in the proof of Rota's Basis Conjecture in the cases where the Alon–Tarsi conjecture is known. The conclusion is that a certain arrangement of vectors in a matrix must exist, but a key step in the argument is that a sum of exponentially many determinants is nonzero, and so at least one of the determinants must be nonzero. The proof does not yield a feasible algorithm for the desired arrangement.

  3. Parity arguments. Any finite graph has an even number of odd-degree nodes. This can be used to prove, for example, that a graph whose vertices all have odd degree must have an even number of Hamiltonian cycles. So if you are given one Hamiltonian cycle, the theorem tells you there is another one, but does not give you an efficient way of finding another one.

There are several other types of nonconstructive arguments known, e.g., using the combinatorial Nullstellensatz, or fixed-point theorems. See for example Noga Alon's paper on nonconstructive proofs in combinatorics. For one final example, I like the paper by Belkale and Brosnan that disproves a conjecture of Kontsevich that certain functions associated with finite graphs are always polynomials. Their proof shows that the space spanned by all such functions is much larger than the space of polynomials, but it does not yield an explicit graph whose function is not a polynomial. An explicit counterexample was not obtained until much later by Brown and Schnetz.

Improve this answer
$\endgroup$
2
  • $\begingroup$ One of the conditions set by the OP was that the argument does not use contradiction, and I think anything involving the pigeonhole principle is in some sense relying on a proof by contradiction: if $f : A \rightarrow B$ and $|A| > |B|$ then $f$ can't be injective, because if $f$ were injective then $|A| \leq |B|$ and we have a contradiction. I was considering posting an argument with the pigeonhole principle earlier but chose not to due to the OP's desire not to see proofs that somehow involve contradiction. $\endgroup$
    – KConrad
    Commented Oct 13, 2018 at 4:49
  • $\begingroup$ @KConrad : Provided one takes some care in formulating the pigeonhole principle, one can prove it (by induction) in Heyting arithmetic, and hence in a certain precise sense it does not rely on proof by contradiction. See for example "Ramsey's theorem and the pigeonhole principle in intuitionistic mathematics" by Veldman and Bezem. $\endgroup$
    – Timothy Chow
    Commented Apr 2, 2019 at 2:53
2
$\begingroup$

C. De Lellis & L. Székelyhidi proved the existence of weird solution of the Euler solutions for an incompressible perfect fluid. These solutions violate the conservation of energy in an arbitrary way. The proof, based on so-called "convex integration" uses in a crucial way Baire's category theorem. Notice that the result does not depend upon the axiom of choice. Whether the proof is constructive depends on how much you consider Baire as a constructive argument.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged .