Editing Constructive proof (section)

==Brouwerian counterexamples==

In [[constructive mathematics]], a statement may be disproved by giving a [[counterexample]], as in classical mathematics. However, it is also possible to give a '''Brouwerian counterexample''' to show that the statement is non-constructive.<ref>{{Cite journal|last=Mandelkern|first=Mark|date=1989|title=Brouwerian Counterexamples|journal=Mathematics Magazine|volume=62|issue=1|pages=3–27|doi=10.2307/2689939|issn=0025-570X|jstor=2689939}}</ref> This sort of counterexample shows that the statement implies some principle that is known to be non-constructive. If it can be proved constructively that the statement implies some principle that is not constructively provable, then the statement itself cannot be constructively provable. 

For example, a particular statement may be shown to imply the law of the excluded middle. An example of a Brouwerian counterexample of this type is [[Diaconescu's theorem]], which shows that the full [[axiom of choice]] is non-constructive in systems of [[constructive set theory]], since the axiom of choice implies the law of excluded middle in such systems. The field of [[constructive reverse mathematics]] develops this idea further by classifying various principles in terms of "how nonconstructive" they are, by showing they are equivalent to various fragments of the law of the excluded middle.

Brouwer also provided "weak" counterexamples.<ref>A. S. Troelstra, ''[https://books.google.com/books?id=V1l7CwAAQBAJ&q=brouwer Principles of Intuitionism]'', Lecture Notes in Mathematics 95, 1969, p. 102</ref> Such counterexamples do not disprove a statement, however; they only show that, at present, no constructive proof of the statement is known. One weak counterexample begins by taking some unsolved problem of mathematics, such as [[Goldbach's conjecture]], which asks whether every even natural number larger than 4 is the sum of two primes.  Define a sequence ''a''(''n'') of rational numbers as follows:<ref>Mark van Atten, 2015, "[https://plato.stanford.edu/entries/brouwer/weakcounterex.html Weak Counterexamples]", Stanford Encyclopedia of Mathematics</ref>
:<math>a(n) =
 \begin{cases} (1/2)^n  & \mbox{if every even natural number in the interval } [4,n] \mbox{ is the sum of two primes}, \\ 
(1/2)^k & \mbox{if } k \mbox{ is the least even natural number in the interval } [4,n] \mbox{ which is not the sum of two primes}
\end{cases}</math>

For each ''n'', the value of ''a''(''n'') can be determined by exhaustive search, and so ''a'' is a well defined sequence, constructively. Moreover, because ''a'' is a [[Cauchy sequence]] with a fixed rate
of convergence, ''a'' converges to some real number &alpha;, according to the usual treatment of real numbers in constructive mathematics. 

Several facts about the real number &alpha; can be proved constructively. However, based on the different meaning of the words in constructive mathematics, if there is a constructive proof that "&alpha; = 0 or &alpha; &ne; 0" then this would mean that there is a constructive proof of Goldbach's conjecture (in the former case) or a constructive proof that Goldbach's conjecture is false (in the latter case). Because no such proof is known, the quoted statement must also not have a known constructive proof. However, it is entirely possible that Goldbach's conjecture may have a constructive proof (as we do not know at present whether it does), in which case the quoted statement would have a constructive proof as well, albeit one that is unknown at present. The main practical use of weak counterexamples is to identify the "hardness" of a problem. For example, the counterexample just shown shows that the quoted statement is "at least as hard to prove" as Goldbach's conjecture. Weak counterexamples of this sort are often related to the [[limited principle of omniscience]].