Definition of "non-constructive proof"

Solution 1:

I apologize if this answer ends up a little vague.

There is no one definition of what "constructive" or "non-constructive" means. Even in the community of mathematical constructivism, there are many disagreements. Just the title of one classic book, "Varieties of constructive analysis", already suggests this.

I can point out two common issues with constructive or non-constructive proofs.

• Constructiveness depends on proof methods. For example, the classical inference rule of double negation elimination ("From $\lnot \lnot P$ derive $P$") is usually viewed as nonconstructive. But a somewhat similar rule of ex falso quodlibet ("From $P$ and $\lnot P$ derive any sentence $Q$") was viewed as acceptable to proponents of intuitionism. The status of the axiom of choice varies greatly from one program of constructive mathematics to another.

• Constructiveness depends on representations. The things that can be done constructively with a mathematical object depend on how the object is represented. For example, in general one cannot prove constructively that for any real number $a$ either $a < 0$, $a = 0$, or $a > 0$. This is because the usual system for representing real numbers does not allow this question to be answered in constructive manner just given a representation for $a$. On the other hand, it is possible in many constructive systems to prove that any integer is "negative, 0, or positive", because the representation of an integer used in such systems is sufficiently nice to allow the answer to be constructively determined from the representation. Note that for some constructivists the "representation" that matters is the mental representation they have.

These two items are related because the constructively permissible proof methods depend greatly on the representations being used. For example, the appropriate forms of the axiom of choice are non-constructive relative to CZF set theory but are constructive relative to Martin-Löf type theory.

Back to the original question. There are many constructive proofs that do not use any methods that imply the entire law of the excluded middle. For example the proof might just use the so-called "lesser limited principle of omniscience" which does not imply excluded middle. In fact I do not know whether there is any one sentence in the language of Heyting arithmetic that implies the entire law of the excluded middle over the rest of HA.

Solution 2:

Two good online resources to start learning about constructive mathematics are Wikipedia and SEP. There are also several nice books and surveys on constructive mathematics and its varieties. Here are some I like more:

Survey:

• A. S. Troelstra, "A History of Constructivism in the 20th Century", 1991

Books:

• A. Heyting, "Intuitionism — An Introduction", 1971

• M. Beeson, "Foundations of Constructive Mathematics", 1985

• D. van Dalen and A.S. Troelstra, "Constructivism in Mathematics: An Introduction", two volumes, 1988

• D. Bridges, F. Richman, "Varieties of Constructive Mathematics", 1987

• Per Martin-Löf "Intuitionistic Type Theory", 1984 (note: this is quite old and Martin-Löf has made several significant changes to this views over time which are to best of my knowledge are not published in a nice form unfortunately.)

For most constructive mathematicians, the essence of mathematics is not formal proofs but constructions. What they mean by construction varies, e.g. for Brouwer these are mental constructions, mathematical objects (particularly infinite mathematical objects) do not have a mind independent existence. So to prove some object exists you should construct it. How can be construct a mental mathematical objects? According to some intuitionist, a mathematician can directly understand what a construction by his/her intuition. There are methods for construction that has been accepted but there is not an a priori bound possible methods, some mathematician can come up with a new method of construction tomorrow. With this in mind it becomes more clear why they expect the justification for nonexistence of an object to be a construction converting a hypothetical construction for it to a construction for contradiction. A good starting point to understand these is the BHK interpretation. As Carl has pointed out there are subtle points about how these constructions are represented, in particular what is the representations for the inputs and the outputs of a functional construction. Many classically identical concepts are not constructively identical, for example there are differences between a function and an operation (see Beeson 1985 for more details). So in constructive mathematics we have more fundamental concepts than we have in classical mathematics where many of these concepts can be reduced to definitions based on other ones and one should be careful about the meaning of statements. When one writes $\forall f \ldots$ is $f$ an operation or a function? and so on.

Other than variations of Bouwer's intuitionism, there are three other active versions of constructivism: 1. Recursive/Computable Mathematics interprets construction as computable function (related to Russian school of constructivism and Markov), 2. Bishop style constructivism which is consistent with classical mathematics and also with intuitionism and computable mathematics, and 3. Martin-Löf's type theory which is more delicate than others (at least IMHO).

So it is not easy how you can rule out that a theorem does not have a constructive proof in the sense of intuitionism (unless one has a constructive proof that would convert such hypothetical proofs to constructive proofs of contradiction) since the possible constructions are not limited to those we have currently, and checking if a given proof is a constructive proof is an intuitive concept which is not defined formally and cannot be checked based on a fixed set of rules (e.g. by a computer program). So in theory, every classical theorem that is not ruled out by a constructive proof can potentially have a constructive proof and it is difficult to give counterexamples to classical reasoning. On the other hand Brouwer developed what is called weak-counter examples, statements that their correctness would imply that we know something at this moment which we don't, e.g. convergence of all Cauchy sequences of rational numbers implies that either we know that GC (Goldbach's Conjecture) is true or that we know GC is false, and right now we don't know either. (GC is not essential for the argument, we can replace it with any $\Pi_1$ formula that we don't know it is true and we don't know it is false).