I was wondering if it is possible to define exactly what a non-constructive (nc) proof is. I have often seen the concept associated with the use of principles such as the axiom of choice or the law of excluded middle, (and the former implies the latter, this is Diaconescu's theorem). Would it be correct to say that a nc proof is a proof which uses something that implies the principle of excluded middle? Here are another couple of doubts I have on the subject:
-
Often certain types of theorems in analysis are said to be "non-constructive". For example, the Picard–Lindelöf theorem on the existence and uniqueness of solutions for certain types of differential equations is often characterized as such, since it doesn't provide an explicit analytic expression for the solution. However it doesn't seem as though the proof for this theorem relies on any nc principles, rather it relies on the Banach fixed point theorem, which provides a sequence defined by a recurrence relation which converges pointwise to the solution. Although analytically useless, shouldn't this way of defining the solution be formally as constructive as any?
-
Are proofs by contradiction nc? For example, as discussed in this post Is there an intuitionist (i.e., constructive) proof of the infinitude of primes?, the classical proof of the infinitude of primes is nc if it only reaches a contradiction, but as pointed out in the answers it can easily be modified so it defines an algorithm which comes up with the (n+1)th prime. If proofs by contradiction are nc, what is the nc principle that they use?
Best Answer
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.