|WikiProject Mathematics||(Rated Start-class, Mid-priority)|
Alan Kay and other computer scientists use the term "Existence Proof" to mean proof by example, e.g. demonstrating a red car is proof that some cars are red. I think this article should add this second connotation. --Mcandre
Charles Matthews 17:37, 10 Nov 2003 (UTC)
A good section on Boyer-Moore theory and the Boyer-Moore theorem prover would help here. There's a whole area of sucessful constructive mathematics that needs to be covered.
One big problem with constructive proofs is that they tend to require case analysis and become bulky. With machine assistance, this is less of a problem.
John Nagle 13:37, 21 Feb 2006 (PST)
Why is the proof based on uncountability nonconstructive?
The statement that the set of algebraic numbers is countable is equivalent to the statement that there exists an algorithm that enumerates them all with increasing precision, i.e. it outputs the decimal approximation of each consecutive number with precision growing by 1 in each turn. We can now use diagonalization to construct a decimal expansion of a real number where each digit is different from the respective digit of the respective algebraic number in the enumerating sequence. This procedure produces a transitive number and it is well-defined: it can produce any digit of the decimal expansion upon request. That allows us to compare the number to any rational number and to create a Dedekind section out of it. What is nonconstructive here?
- Well, sure, but that's a diagonal argument, and it is not the same as the proof based on uncountability. As the article says:
- We may distinguish three different problems. The first is that of proving the existence of transcendental numbers (without necessarily providing a specimen). The second is that of giving an example of a transcendental number by a construction specially designed for the purpose. The third, which is much more difficult, is that of proving that some number given independently ... is transcendental.
- So "algebraics are countable, reals are uncountable, therefore transcendentals exist" is a (non-constructive) solution to the first, your proof is a solution to the second (we could include it in the article as such), and a proof that pi is transcendental is a solution to the third. On the other hand, perhaps we should just find a better example. 220.127.116.11 15:12, 24 July 2006 (UTC)
The anon has a good point here. While you might argue that the countability proof is nonconstructive as it stands, if it can trivially be made constructive, then there is not much to its nonconstructivity.
Indeed, constructive treatments of analysis (like that by Errett Bishop) will prove (constructively) that the set of real numbers is uncountable in a strong sense: that given any countable set A of real numbers, there exists a real number which is distinct from every element of A; this is what Cantor's diagonal argument naturally shows. In that case, once you've proved the countability of the algebraic numbers (which has no surprises), then it's obvious that a transcendental number exists.
To be sure, you could sabotage Cantor's proof of the uncountability of the reals to produce a weaker result: the mere fact that the set of real numbers cannot be countable. In that case, the proof that there exists a transcendental number is not constructive; it only proves that there can't not be a transcendental number. But to a constructivist, this interpretation is perverse; the word "uncountable" naturally takes the stronger meaning.
This sort of example is commonly used by nonconstructive mathematicians that (in my opinion) don't really understand costructivism (and so can't appreciate the finer points of the nonconstructivity of proofs). Constructive mathematicians themselves often use the example in Nonconstructive proof, a proof that the irrational numbers aren't closed under exponentiation. But that example is less satisfying (especially since even the example in the nonconstructive proof can easily be decided: (√2)√2 is irrational by the Gelfond–Schneider theorem).
Non Constructive Proofs
The article should be rewritten completely because the approach used in this article is academic. The concept of non-constructive proof is different from constructive proof and it (non constructive proof) should have a separate article. arsalan... (talk) 19:20, 22 December 2009 (UTC)
I don't understand the sentence "Since intuitionistic logic is consistent with classical logic, it is impossible to disprove non-constructive statements that are classically valid." What does it mean for for some logic to be 'consistent with' another? I have only heard consistency used with respect to a particular logic. I.e. in a consistent logic you cannot derive a contradiction (e.g. 0 = 1). Should it instead say that adding a classical principe (say excluded middle) is a 'conservative extension' of intuitionistic logic? Meaning that by adding excluded middle we would only get a system in which all classical theorems hold but nothing more, i.e. we don't end up with something inconsistent. Please correct me if I am wrong. 18.104.22.168 (talk) 18:05, 9 July 2010 (UTC)
- We say that a theory S extending a theory T is a conservative extension of T if everything that is in the language of T and provable in S is already provable in T. So classical logic is not a conservative extension of intuitionistic logic.
- However, there are problems with the wording of that section. Some constructive systems do assume principles that are false in classical mathematics. For example, these systems may assume that every function from ω to ω is computable, or assume every function from R to R is continuous. Not every constructive system assumes such things; some constructive systems are consistent with classical mathematics.
- In any case, I reworded the section to avoid this issue and avoid the "consistent with" terminology. — Carl (CBM · talk) 19:58, 9 July 2010 (UTC)
Is Gelfond constructive?
The page states that "It turns out that is irrational because of the Gelfond–Schneider theorem, but this fact is irrelevant to the correctness of the non-constructive proof". Does anyone know whether the theorem is valid in a constructive framework? Tkuvho (talk) 15:06, 27 February 2012 (UTC)
Brouwerian weak counterexamples
I just changed in section Constructive proof#Brouwerian counterexamples the sentence "Such counterexamples do not disprove a statement, however; they only show that, at present, the statement has no constructive proof" into "... at present, no constructive proof of the statement is known". On second thought, I don't understand either version of the sentence: A mathematical proof cannot yield a result about the current state of knowledge of the human scientific community, can it?
In the Goldbach example, it could be possible that the thinking along the lines of defining f etc. just leads to the proof (or disproof) of Goldbach's conjecture. So the sentence "Because no such proof [of Goldbach's conjecture] is known, the quoted statement [about f] must also not have a known constructive proof" is wrong imho; instead, a constructive proof of the quoted statement about f could well be found and, in turn, would lead to a proof of Goldbach's conjecture.
(Of cource, I don't expect a Goldbach proof to be found this simplistic way; this is just a thought experiment.) I wonder what Brouwer and/or Troelstra originally said about this, but I can't get access to Troelstra's book and don't even have a reference for Brouwer (the article should provide one). The SEP page externally linked seems to suggest that Brouwer considered mathematical truth to be changing in time (and from person to person), according to current knowledge, but doesn't elaborate on that. - Jochen Burghardt (talk) 11:50, 12 October 2013 (UTC)
- Yeah, this article could be clearer. I may fix it myself, but don't hold your breath. Briefly:
- Of course such things are templates, if one problem is solved one simply substitutes the next unsolved problem.
- I'm sure Brouwer had this template in mind. Although he predates Church's thesis and the terms "co-c.e." or "Pi_1", he knew (and the article misses this point) that there is an effective procedure which terminates if and only if Goldbach's conjecture is false. (I seem to remember also "999999999 does not appear in the decimal expansion of pi", also Pi_1.)
- As for mathematical truth changing in time and all that, Brouwer and others take that view. But it is not necessary for constructivism. If you assume Church's thesis (constructive mathematics), and substitute the halting problem for Goldbach's conjecture, then you've actually disproved the law of the excluded middle. Church's Thesis is a (Pi_2) conservative extension of arithmetic, and even of set theory (while the law of the excluded middle is conservative over arithmetic but not over set theory).
- --22.214.171.124 (talk) 16:11, 9 February 2015 (UTC)