Talk:Constructive proof

Untitled[edit]

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

It seems to me that this, existence theorem and nonconstructive proof all cover the same ground. It would be better to merge all three, I think, and get one substantive article.

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?[edit]

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. 192.75.48.150 15:12, 24 July 2006 (UTC)[reply]

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).

—Toby Bartels (talk) 02:13, 19 November 2007 (UTC)[reply]

Non Constructive Proofs[edit]

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)[reply]

Consistent with[edit]

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. 88.196.63.146 (talk) 18:05, 9 July 2010 (UTC)[reply]

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)[reply]

Is Gelfond constructive?[edit]

The page states that "It turns out that ${\sqrt {2}}^{\sqrt {2}}$ 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)[reply]

Brouwerian weak counterexamples[edit]

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)[reply]

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).

--74.216.224.3 (talk) 16:11, 9 February 2015 (UTC)[reply]

Mistake in section Examples/Non-constructive proofs ?[edit]

I think the part 'all of its prime factors are greater than n' should instead be 'some of its prime factors are greater than n'. Am I mistaken? Notrium (talk) 20:54, 11 April 2015 (UTC)[reply]

The statement holds as written. However, I fail to see why this proof is inconstructive, given that you can take the smallest factor as before. Yecril (talk) 21:48, 26 April 2015 (UTC)[reply]

Assessment comment[edit]

The comment(s) below were originally left at Talk:Constructive proof/Comments, and are posted here for posterity. Following several discussions in past years, these subpages are now deprecated. The comments may be irrelevant or outdated; if so, please feel free to remove this section.

Why doesn't someone write a history of constructive proofs to show how the field has grown and evolved? Robert HoffmanRobert hoffman (talk) 19:11, 7 September 2009 (UTC)[reply]

Last edited at 19:11, 7 September 2009 (UTC). Substituted at 01:55, 5 May 2016 (UTC)

Definition by cases[edit]

Right now, the article says: "Define a function f of a natural number x as follows:

f(x)={\begin{cases}0&{\mbox{if Goldbach's conjecture is false}}\\1&{\mbox{if Goldbach's conjecture is true}}\end{cases}}

Although this is a definition by cases, it is still an admissible definition in constructive mathematics."

Is it? I think usually this sort of example is given by something like f(n)=0 if 2n is the sum of two primes or n is 0 or 1 and f(n)=1 otherwise. This second definition by cases uses a decidable criterion and so demonstrably yields a computable function. If definitions by cases are generally allowed to take the form the article suggests, however, that would seem to imply the existence of noncomputable functions (at least if there are no restrictions on what sorts of cases we can use), which at least some constructive theories outright deny.

I suppose we could, in a constructive theory, postulate the existence of a function such that f(x)=0 for all x if Golbach's conjecture is false and f(x)=1 for all x if it is true and reason about such a function's properties, but it's not even obvious to me that most constructive theories would be able to prove that two such functions are equal (without either proving or disproving Goldbach's conjecture)107.77.211.108 (talk) 19:52, 4 January 2017 (UTC)[reply]

That example was indeed unclear - thank you for pointing it out. Although something was defined, it would not be possible to prove constructively that f was even a function. I changed the example to a more classical one involving the limit of a Cauchy sequence, with a reference to the SEP. — Carl (CBM · talk) 21:15, 4 January 2017 (UTC)[reply]

I'm glad to have helped. I also edited your definition to include the condition that the counterexample is even in the second case, which I believe is necessary unless I'm having a really bad day for thinking clearly. 107.77.212.225 (talk) 18:17, 6 January 2017 (UTC)[reply]

External links modified[edit]

Hello fellow Wikipedians,

I have just modified one external link on Constructive proof. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

Added archive https://web.archive.org/web/20141023060917/http://www.users.waitrose.com/~hindley/Root2Proof2014.pdf to http://www.users.waitrose.com/~hindley/Root2Proof2014.pdf

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 13:51, 12 August 2017 (UTC)[reply]

Unrelated sentences[edit]

"Some non-constructive proofs show that if a certain proposition is false, a contradiction ensues; consequently the proposition must be true (proof by contradiction). However, the principle of explosion (ex falso quodlibet) has been accepted in some varieties of constructive mathematics, including intuitionism."

These two statements are not related to each other. This appears to be an act of vandalism or a mistaken edit, removing some important context relating the two sentences. Comiscuous (talk) 01:31, 11 January 2022 (UTC)[reply]