# Non-constructive proofs vs. efficient algorithms

My question concerns what is meant by "nonconstructive", and whether it has ever been defined in terms of computational complexity.

The wikipedia article on constructive proof begins, "a constructive proof is a method of proof that demonstrates the existence of a mathematical object by creating or providing a method for creating the object." On the other hand, the wiki article on the probabilistic method states, "the probabilistic method is a nonconstructive method [...] for proving the existence of a prescribed kind of mathematical object." I believe these two statements are at odds with one another.

Consider Erdős's celebrated proof of the lower bound of the Ramsey number. This proof shows that as long as $\binom{n}{r} < 2^{\binom{r}{2} - 1}$, there is some coloring of the edges of $K_n$ with $2$ colors that has no monochromatic sub-$K_r$. The proof offers no idea what such a coloring looks like; however, it does lead to a "method for creating" the object in question: try all possible colorings. The proof guarantees that this naive algorithm terminates. Of course, this algorithm quickly becomes computationally infeasible. But in principle, via exhaustive search, any proof of the existence of an object in some finite collection admits of a "method for creating" the object.

Imagine now that we had a different proof of the lower bound of the Ramsey number. This new proof constructs two possible edge-$2$-colorings of $K_n$ and shows that at least one must result in no monochromatic sub-$K_r$, although it remains silent about which of the two colorings works. I think this would also qualify as a "non-constructive" proof (based on analogy to the wiki example with $\sqrt{2}^{\sqrt{2}}$), and yet it would lead to a wonderfully efficient method for finding such colorings. For any $r$, this hypothetical proof says we have to check only two candidates to get the object we're looking for. I think this even gives us a polynomial time algorithm for finding such a coloring (but this depends on how quickly we can verify a coloring.) At any rate, I hope the distinction I am trying to draw is clear.

Does it makes sense to say that a constructive proof is a proof that leads to an efficient algorithm for creating an object with a desired set of properties? Has there been any work related to such a definition? The above is most relevant to statements in discrete math.

-
–  András Bátkai Dec 30 '12 at 0:57
The use of the word "nonconstructive" in the article on the probabilistic method doesn't refer to the meaning of this word in logic. If you want to avoid the confusion, go with the notions "effective" (for the logical meaning of "constructive", i. e., the proof gives a construction) vs. "efficient" (for the meaning used in the probabilistic method article, i. e., the proof gives a fast algorithm). –  darij grinberg Dec 30 '12 at 0:58
Strictly speaking, Wikipedia is wrong to say (if this is what it says) that Erdős's proof is nonconstructive, if it means this in the sense of constructive mathematics. It is a perfectly valid proof in constructive mathematics (although perhaps not in ultrafinitist mathematics). This is because it proves that the obvious method of search (try everything, as you said) must work. Your hypothetical alternative proof would also be constructive. –  Toby Bartels Dec 30 '12 at 1:04
The reason that the nonconstructive proof of the $\sqrt{2}^{\sqrt{2}}$ theorem is nonconstructive is not that it offers a choice but that it gives us no way to actually compute which option works. –  Toby Bartels Dec 30 '12 at 1:26
I'd vote up your first comment more than once if I could, Toby. –  Todd Trimble Dec 30 '12 at 3:02

As others have noted there are several different meanings for constructive.

I. Constructive proof in the sense of constructive mathematics

This meaning views an object as existing if we have a description of how to construct the objects (though we don't really need to carry it out), and there are several distinct constructive views. Saying a proof is constructive or not can be ambiguous without specifying which school of constructive mathematics we are talking about.

By the way, it can be the case that we can convert a non-constructive proof to a constructive one (Georg Kreisel's unwinding program or Ulrich Kohlenbach's proof mining program). That does not make the original proof constructive!

Note that algorithmic computability is just one of several constructive perspectives. For example, in intuitionism there are objects which are not algorithmically computable. A way of understanding this is to remember that Churth-Turing thesis is not an axiom that is accepted by all constructivist, there can be constructions which are not algorithmic in the instuitionistic view.

II. Constructive in the sense of complexity theory

This is a more recent meaning. We mean a proof of existence of an object is constructive if it gives directly a method of efficiently computing/constructing the object. This is the more common meaning of the word in combinatorics these days, e.g. in Robin A. Moser's "A constructive proof of the Lovasz Local Lemma" paper from 2008.

Constructive is used in the sense of efficient algorithms in complexity theory, for example, constructive in Alexander Razborov and Steven Rudich's "Natural Proofs" paper means that the property used in the lower-bound proof is efficiently computable.

Note that the proof itself can be non-constructive in the sense of meaning I while remaining constructive in this sense. You can give an efficient algorithm to compute some object and the correctness and efficiency proofs can be non-constructive. We don't have many interesting examples, but a good example would be the Robertson-Seymour theorem. See also Are there non-constructive algorithm existence proofs?

III. Proof complexity perspective

This is kind of the intersection of the previous two, though I don't recall anyone refer to it as "constructive proof" (probably because they are aware of both previous meanings and don't want to confuse people further :).

Here not only the object should be computable efficiently but the correctness and efficiency proofs must use only efficient concepts. The Robertson-Seymour theorem is an example of an efficient algorithm where we don't have a proof using only efficient concepts. I can give more artificial examples to distinguish between this and the meaning in the previous section but I don't recall any other natural ones.

-
Thank you, I think this is the most comprehensive and clear answer. –  Sam Hopkins Apr 12 '13 at 2:46

The terms "constructive" and "non-constructive" proofs have much wider application than discrete mathematics and algorithms for finite sets. And they can have have several meanings. A non-constructive proof proves that something exists but gives no way to construct the object. For example, one can prove existence of transcendentasl numbers by a simple countability argument. This proof does not give you a single example, it is non-constructive. And such proofs are actually abundant in mathematics. See, for example MR1852188 M. Kontsevich, D. Zagier, Periods.

Liouville's proof of existence of transcendental numbers is constructive. Some results do not have any constructive proof at all, I mean the things related to Hahn-Banach. For example, every vector space has a basis. But you cannot really give an example of a basis of the vector space R over Q. By giving an example, I mean you define the set in the sense that for every number you can tell whether it is in the set or not.

Another example, of different sort. There are famous theorems in number theory which say that certain inequalities or equations have finitely many solutions. But sometimes the proof does not tell in principle how to obtain ANY upper estimate. These are non-constructive proofs. Then people spend a lot of efforts to give an explicit estimate. Here constructive proofs sometimes exist, sometimes not.

In Analysis, we all know that every continuous function on a compact set has a maximum. But there are plenty of interesting continuous functions on interesting compact sets, for which we know nothing else (how many maxima? Is the absolute maximum less than 10 or not, and don't know how to answer these questions). Here existence of a maximum is a typical non-constructive proof.

In the beginning of XX century some mathematicians did not recognize non-constructive proofs as valid. In particular, they did not accept unlimited application of the axiom of choice. Some did not accept uncountable sets at all.

This gave the origin to a kind of mathematics which in known under the names Constructive mathematics in USSR and Intuitionism elsewhere. Roughly speaking in Intuitionism only those existence proofs are recognized which give an algorithm to construct them. For example, in Intuitionist mathematics it is not always true that a bounded increasing sequence has a limit.

If you are interested, there is a nice little book

MR0075147 Heyting, A. Intuitionism. An introduction. North-Holland Publishing Co., Amsterdam, 1956. viii+133 pp.

which gives a very readable introduction.

When I was a student in 1970-s, some ordinary mathematicians (I mean non-logicians) in some places were still concerned with these issues.

-
Regarding your example, the proof of the existence of transcendental numbers via the cardinality argument actually is constructive: we enumerate the algebraic numbers, and then by diagonalization we construct a specific real number not on the list. –  Joel David Hamkins Dec 30 '12 at 2:19
The diagonal procedure is constructive: for any countable list of real numbers $r_0,r_1,r_2,\ldots$, one may construct a real number $d$ not on the list by specifying that the $n^{th}$ digit of $d$ is $5$, if the $n^{th}$ digit of $r_n$ is not $5$, and otherwise $7$. Historically, Cantor was careful to frame his argument in these constructive terms. Cantor's proof of the existence of transcendental numbers is completely constructive. Of course, it also can be given as a proof by contradiction, as you mention, but that way of doing the argument, to my mind, leaves something out. –  Joel David Hamkins Dec 30 '12 at 4:16
In particular, Cantor gave a constructive enumeration of the algebraic numbers by enumerating all finite sequences of integers, and considering the roots of associated polynomials. Then, the diagonal real is constructed to avoid that set. I once saw a Math Monthly article that carried out Cantor's specific enumeration, and the title of the piece was something like, "$5.75575777555\cdots$ is transcendental." (But I don't now recall exactly.) –  Joel David Hamkins Dec 30 '12 at 4:21
Regarding periods, it appears that any period has complexity at most $\Delta^1_1$ in the descriptive set-theoretic hierarchy, which is to say that they are situated rather low in the hierarchy, and so there are abundant examples of specific non-period numbers (in addition to the examples constructed simply by diagonalization). For example, the real number whose binary digits are the characteristic function of the true $\Sigma^1_2$ statements is not a period, simply because it cannot be $\Delta^1_1$. –  Joel David Hamkins Dec 30 '12 at 4:36
Alexandre, yes, there is a completely explicit enumeration of the algebraic numbers. They are computable, in the sense of computable analysis---one can provide a Turing machine program to enumerate them, computing any desired digit of any one of them---and the Cantor diagonal transcendental number is also computable. For periods, it seems that every computable number is a period, so one cannot be extremely explicit about this, but it seems that there are $\Delta^1_1$) numbers that are not periods, which would provide relatively explicit examples. (But I defer to the period experts.) –  Joel David Hamkins Dec 30 '12 at 23:50

Here is my very personal perspective, particularly as applied to the examples given. Constructive mathematics can be a technique of value to understanding. It is possible to use it sometimes and not others. Sometimes being constructive amounts to no more than more carefully examining what it is that your proof proves.

The diagonal argument on reals really proves that given a countable list of real numbers it can not be that every real number is on the list. Less turgidly (but also less precisely) you give me the list and I will provided you a number not on the list, my exception will be provided to you as quickly as you provide the list. You must provide the members of the list as decimals (or at least appropriate nested intervals), however I will allow you to give the members of the list to a finite precision, say the $k$th accurate to $10^{-k}$. Thinking about that for a while you generalize to saying: Given a countable list of open intervals, each inside $(0,1)$, with the $k$th one of diameter $10^{-k}$, over $88\\%$ of that interval is uncovered. I feel that I got an important insight into the difference between $\mathbb{Q}$ and the rest of $\mathbb{R}$ when I realized that, not only is there an irrational between every two rationals and vice versa, in fact we can cut out all the open intervals $(p/q-1/(2q)^3,p/q+1/(2q)^3)$ and still leave "most" of the real line behind. What is left is only irrational numbers and each one is actually separated from each rational. I would not have that insight unless I struggled with the "real" meaning of the diagonal argument.

As I remarked, you don't have Erdős's probabilistic result quite right. The result is that when $\binom{n}{r} < 2^{\binom{r}{2} - 1}$ there is a $2$-coloring of the edges of $K_n$ with no monochromatic $K_r$. So a graph with $5001$ vertices can be $2$-colored to avoid a monochromatic $K_{20}$. Of course there are over $12,500,000$ edges there so just getting a coloring would take a very long time, let alone checking it. Actually you could get close to $n=6000$. With $n=5000$ there is a better than $95\\%$ chance that a "random" coloring will avoid a monochromatic $K_{20}.$ But if I tell you that I colored a random $K_{20}$ red and then colored the other edges randomly, you would have a very hard time deciding within a year if I was telling the truth.

It is known that $n=\binom{38}{19} \gt 10^{10}$ is enough to be sure of a monochromatic $K_{20}.$ That would be a lot of edges.

-
Two comments about the second paragraph of your answer: (1) In the first sentence "it cannot be that every real number is on the list" is correct, but the proof actually gives the (equivalent in classical logic but stronger in constructive logic) conclusion "there is a real number that is not on the list." (2) The more detailed considerations in the rest of this paragraph actually lead (at least in classical logic) fairly naturally to the Baire category theorem. –  Andreas Blass Dec 30 '12 at 21:42
I'm sure that you are right on both counts. 1) The set of "constructable" numbers is countable so there "is" a non-constructable real. I realize that we don't know when (if ever) a certain algorithm will spit out the next digit or increment of precision but... 2) Yes you can can think constructively and privately feel virtuous while your classical friend just thinks you have good insights (when she doesn't think you are being pointlessly perverse..). –  Aaron Meyerowitz Dec 30 '12 at 22:48
Also, carried in another direction one is lead to Diophantine approximation. Find a real in that set. Better: find the best replacement $\frac{1}{cq^{\theta}}$ for $\frac{1}{8q^3}$ and a real for that. –  Aaron Meyerowitz Dec 31 '12 at 0:01

As a personal view - there are lots of different meanings to 'constructive'. At one end, there is the distinction between objects which can be proven to exist in ZFC but not ZF (with finer distinctions if you like logic). At the other, one has the Erdos-idea of constructive, which isn't really formally defined but should certainly imply a polynomial time algorithm which further doesn't apply brute force checking in its running. In particular this excludes for example taking a Szemeredi partition of a graph and then brute-force testing the associated (bounded size) cluster graph for some property, even though this is a valid polynomial algorithm. And then there are all the shades in between - one definition of 'constructive' is 'I know it when I see it'.

Usually the meaning of 'constructive' is just 'useful for my further proof' - so an object constructed via the axiom of choice will probably not come with any extra properties one can use to prove further facts, while an object which comes from some number-theoretical construction, even one which isn't polynomial-time constructible, usually comes with a host of extra facts one can use. And an object which has a nice cubic time algorithm to construct, but where the cubic algorithm uses brute force on a Szemeredi partition somewhere, is probably not easy to work with. A probabilistic construction is somewhere intermediate - if it's really an easy construction (take a random graph and with high probability it works) then you can read off a bunch of extra properties, but more complex constructions (nibble method, or local lemma, et cetera) don't necessarily keep properties and one has to check that the proof goes through with the extra conditions.

-
The distinction between working in ZF and working in ZFC is actually NOT the main issue in non-constructivity of a proof. The main issue resides in the background logic one is working with: is it classical or intuitionistic? The key difference is whether one's arguments rely on the law of excluded middle or not (see a more detailed answer below). –  katz Mar 17 '13 at 13:13

Not a very serious answer, but maybe there is a little more than "how fast you can construct" to it when it comes to constructive proofs in some cases.

A typical combinatorial design is often described as a set $\mathcal{B}$ (called block set) of subsets of some other set $V$ (called point set). The size of $V$ is the order of the design.

If you use some probabilistic method to prove the existence of a design with certain properties, it's typically considered nonconstructive while good constructive proofs ideally give good algorithms to explicitly list the elements of $\mathcal{B}$ that satisfies the required conditions.

Now it's not rare that it's easier to give a good constructive proof if order $\vert V \vert$ is prime because we have more combinatorial/algebraic/number theoretic tools. So you may be able to give a good constructive proof that for any prime order, there exists a design with the desired properties.

One approach to solving the remaining cases (i.e., the case when the order is a composite number) is to give a certain product type construction, where if you have a pair of designs of order $v_0$ and $v_1$, you can systematically construct a new design with the desired properties of order $v_0v_1$. In other words, you prove that if there exist the kind of design you want of order $v_0$ and $v_1$, there also exists the same kind of design of order $v_0v_1$ by giving an algorithm. This way, in an ideal world, you can cover all possible orderes because you already have the kind of design you want for all prime orders.

If everything worked out like magic, your construction for prime orders and product type one are both super fast algorithms that give explicit examples very quickly.

Now you tell an engineer that you found super fast and explicit constructions for the kind of design he wanted. You say your proofs are perfectly constructive and very fast algorithms that work for any order he likes.

The engineer gets excited and asks you to get him the design of $\vert V \vert = 12873891274647018937561708356916501047777612653914909670721635802187$ real quick. And you don't have a quantum computer to factor that number into primes yet.

-
61 * 1181 * 3580901 * 15589577 * 43349897 * 73844029763182929501705249453515800152103 = 12873891274647018937561708356916501047777612653914909670721635802187 –  Thomas Klimpel Dec 30 '12 at 19:08
Look, folks. This is what you get for using a weak key for your public-key chryptography when you're surrounded by mathematicians. (Dear diary, Thomas is a meanie. A biiig meanie!) –  Yuichiro Fujiwara Dec 30 '12 at 20:51

I would like to elaborate a bit on Alexandre Eremenko's answer. He cited Heyting's book on intuitionistic mathematics. From this point of view, the simplest definition of a constructive proof is a proof that does not rely on the Law of Excluded Middle (LEM for short).

LEM is a key ingredient in every proof by contradiction. One may or may not agree with such a definition of constructive proof, but it's the most common one in the literature. To give an example, a probabilistic proof of the existence of a certain object will show that if there is no such object, a contradiction results. From this one customarily deduces that the object does exist. The step mentioned in the last sentence involves a use of LEM. To put it another way, if $P$ is a proposition, then in classical logic $\neg\neg P$ is the same as $P$. However, in an intuitionistic logic, they are different.

Some constructive mathematicians have compared the suppression of LEM from the background logic, to the suppression of the axiom of commutativity in passing from abelian group theory to the theory of arbitrary groups. The argument is that sometimes the suppression of an axiom results in a more interesting theory. Whether or not this is the case for LEM is of course controversial.

-
Even intuitionists agree that LEM holds for the equality predicate on natural numbers. Arguments using probability (or counting) on finite sets, such as Erdős’s proof mentioned in the question, are easily formalizable in, say, Heyting arithmetic. Thus this does not explain the concept of constructibility the OP is looking for. –  Emil Jeřábek Mar 14 '13 at 18:16
I wonder what the scope is of your claimed intuitionistic translation of "probabilistic" proofs. Thus, a result about lattices in Euclidean n-space says that there exist unimodular lattices whose Hermite constant grows linearly in n. The proof uses p-adics and Siegel's formula, showing that the "average" lattice has this asymptotic behavior. However, nobody has been able to construct such lattices. This is an example of a non-constructive "probabilistic" proof (because the last step uses LEM). If your claimed translation covers this case, one could probably extract a construction out of it. –  katz Mar 17 '13 at 12:40
Emil wrote (my emphasis): "Arguments using probability (or counting) on finite sets, such as Erdős’s proof mentioned in the question, are easily formalizable in, say, Heyting arithmetic." –  François G. Dorais Apr 5 '13 at 14:27
Unimodular lattices can similarly be taken to have integer entries. it is remarkable that one can obtain asymptotic results about them using deep results about p-adics. Conway and Thompson constructed lattices with optimal behavior this way, as reported in Milnor and Husemoller. –  katz Apr 6 '13 at 19:49