Talk:Nonconstructive proof

To make this into a proper article, we need some examples of nonconstructive proofs, and discussion thereof.

See Votes for deletion for some discussion about the article too :) Dysprosia 10:52, 22 Aug 2003 (UTC)

Same as existence proof?

I removed "or an existence proof" from the opening sentence, because as I see it, constructive proofs are also existence proofs! The existence theorem article distinguishes "pure existence theorems" which are proven by nonconstructive methods; in this terminology, wouldn't a nonconstructive proof just be a "pure existence proof"? -- Oliver P. 11:25, 22 Aug 2003 (UTC)

I put it back - Sorry, I missed the talk. But it is also known as an existence proof as well, but I'll add your point. Dysprosia 11:27, 22 Aug 2003 (UTC)

Okay, fair enough. Thanks. :) -- Oliver P. 11:33, 22 Aug 2003 (UTC)

No problem-o :) Dysprosia 11:34, 22 Aug 2003 (UTC)

Accommodating mathematical constructivism

Also, I'm not sure how far we have to fo to accommodate supporters of mathematical constructivism. If they say that nonconstructive proofs are invalid, do we have to say that they only purport to prove things? -- Oliver P. 11:25, 22 Aug 2003 (UTC)

Nonconstructive proofs always prove something, it just may not be what they purport to prove: any nonconstructive proof of a proposition P can be thought of as a constructive proof of not (not P), that is, a constructive refutation of the impossibility of P. Constructively, it is not the case that not (not P) implies P. William Lovas 04:12, 3 February 2006 (UTC)[reply]

LA example

I think that in linear algebra class we first proved that there existed a function that satiesifed the properties we wanted for the determinant, before showing what it actually was -- Tarquin 11:40, 22 Aug 2003 (UTC)

From VfD

Nonconstructive
- Dictionary definition. -- Oliver P. 10:34, 22 Aug 2003 (UTC)
  - Keep, could redirect to Mathematical proof? (A nonconstructive proof might be thought of as a "not-constructive" proof, then a proof of existence...) Dysprosia 10:47, 22 Aug 2003 (UTC)
  - I think in this context "nonconstructive" is meant as the exact antonym of mathematical constructivism, so it should just redirect there. --Delirium 10:58, Aug 22, 2003 (UTC)
  - NB someone's already made a redirect/move to Nonconstructive proof... Dysprosia 11:13, 22 Aug 2003 (UTC)
- Suggest removal from here, this is now a real stub article...

I'm removing the entry from VfD as I'm sure no-one wants it deleted now. -- Oliver P. 23:06, 22 Aug 2003 (UTC)

Gödel's incompleteness theorem and the intermediate value theorem are both really constructive theorems. Why are they put here? Phys 13:30, 25 Aug 2003 (UTC)

"easier" example

I'm fairly sure the example with x^2 and sqrt(x) is not really an example of a true nonconstructive proof. What is the thing whose existence is proved but not constructed? The sqrt(x) function seems to me to be a specific thing, so it can't be that. What is it then? But, I'd prefer someone more expert in logic to confirm/deny this. Revolver 18:47, 2 September 2005 (UTC)[reply]

I agree this is not an example; I noticed this while reading the article and went to the talk page to leave a note to this effect. Also the Hex example is weak, since Hex is finite. Lambiam 11:53, 14 January 2006 (UTC)[reply]

last example seems odd

The current (ie. as of May 24 2006) revision of this article provides the following as the last example of a nonconstructive proof:

"There exists an algorithm that determines whether Goldbach's conjecture holds or not." Somewhat startlingly, this statement has a quite elementary nonconstructive proof:...

There's something weird about this last example but I can't quite put it in words. Here's my attempt of what I'm trying to complain about:

It's not clear what the precise meaning is for an algorithm to "determine" the truth or falsehood of a conjecture. What kinds of computation does it really need to do? The nonconstructive proof given implies that "determine" merely means the algorithm happens to give the same truth value as the truth value of the conjecture. But then isn't the proof and the statement simply restating the "obvious" of "the conjecture is either true or false"? I mean, the logic presented is totally sound, but the example, in the way I'm trying to understand it, just seems rather trivial and far from startling. 131.107.0.106 02:48, 25 May 2006 (UTC)[reply]

Yeah. In order to write an algorithm which does nothing but output "true" and to call it an algorithm to determine wheter G.'s conjecture holds, one would have to already know that it does hold. Otherwise you can just call it an algorithm to write out "true". (Apparently, the editor who added this has a broader definition of "determining" than mine, they're calling an algorithm to determine wheter x holds any algorithm which outputs "true" if it holds and "false" otherwise. From my POV, it should be added that someone unaware of wheter x holds should be able to write that algorithm, and to know that it'll work. In this case, if G's conjecture holds, Alice is unaware of this, and Alice writes an algorithm to write out "true", she cannot claim to know the algorithm works to determine wheter the conjecture holds. Yes, my definition is less rigorous, but IMO more useful.)--Army1987 13:26, 4 June 2006 (UTC)[reply]

But if we are adding criteria to the algorithm in order for it to qualify as "determining whether G's conjecture holds", then it seems we no longer have a valid nonconstructive proof either, since the "trivial algorithms" (output true/output false) used in the nonconstructive proof do not qualify as "determining whether G's conjecture holds" according to your suggested criteria.

So basically, I just don't think this is a good example for demonstrating nonconstructive proofs. I'm probably going to be bold and remove the example later this week. Maybe I'll replace it with a better, more conventional example if I find one. 67.170.72.189 10:35, 12 June 2006 (UTC)[reply]

I'm neither a professional mathematician nor a native English speaker, and I don't know wheter the verb to determine has any "official" definition in the context of algorithms. I just expressed my common sense understandment of the matter, so don't trust it too seriously. --Army1987 15:09, 12 June 2006 (UTC)[reply]

I understand. Nonetheless, our correspondence at least seems to show that, there is enough indication that the example presented does more to confuse than to educate. Again, I will try to find a replacement in the near future. 24.19.184.243 04:35, 13 June 2006 (UTC)[reply]

I think it would be better to totally remove the last example. In fact, just replace "Goldbach's conjecture" with Continuum hypothesis and the same argument would say "There is an algorithm to determine wether the CH holds or not". This is clearly false, as it's known that the CH is undecidable. Salvatore Ingala 11:17, 16 July 2006 (UTC)[reply]

Sounds good, I'm removing it now. 24.19.184.243 23:07, 16 July 2006 (UTC)[reply]

Same as existence proof ? (redux)

My understanding of an existence proof (or, to be more precise, a pure existence proof) is a proof that goes like this:

Either P or not P. If not P then P. Therefore P.

and so proves P without showing how to find or construct an explicit case of P. For example, Cantor's diagonal argument shows that that no countable list can contain all real numbers; the set of algebraic numbers is countable; therefore there are real numbers that are not algebraic. This is a proof of the existence of transcendental numbers without giving us a clue of how to find or construct one.

Now our axiom of choice article says: "A proof requiring the axiom of choice is always nonconstructive". So the proof in our Banach–Tarski paradox article is nonconstructive since it uses the axiom of choice. Yet that proof gives a very detailed construction for an appropriate dissection of a 3-d ball. The only non-explicit step in that proof is using the axiom of choice to pick exactly one point from every orbit of the group of rotations H. It seems to me that the Banach-Tarski proof does not follow the pattern of a pure existence proof - it says "If you grant me a tool called axiom of choice, I give you an explicit dissection of a 3-d ball with certain non-intuitive properties".

This makes me question whether pure existence proof and nonconstructive proof really are synonomous. It seems to me that pure existence proof has a narrower definition that nonconstructive proof - the Banach-Tarski proof is nonconstructive but is not just a pure existence proof. And so the line in this article that says: "The term pure existence proof is often used as a synonym for nonconstructive proof" should be qualified by explaining that the terms are not in fact synonomous (despite what MathWorld says here). Or maybe nonconstructive proof is used in two slightly different ways, only one of which is synonomous with pure existence proof. Thoughts ? Gandalf61 15:59, 18 June 2007 (UTC)[reply]

The important thing here is what the tool "axiom of choice" does. The axiom of choice tells you that certain sets, namely those formed by making an infinite number of choices, exist and may be defined in terms of this choice. The axiom tells you nothing about how to actually construct this set or make the choices. Thus Banach-Tarski is in fact an existence proof, in that it says there exists some dissection of a sphere into two spheres if you know how to make uncountably many choices. The axiom of choice says it is possible to define a set using uncountably many choices, not how to actually construct such a set.

I suppose you could think of the axiom choice as the "existence axiom" - as it postulates the existence of certain sets that cannot be constructed. Thus any proof using it is both non-constructive (as sets defined using the axiom of choice cannot be constructed) and an existence proof (it is saying something exists but not specifying an example constructively).

When I was taught about this, the emphasis was always on the fact you can't actually get your hands on axiom of choice-defined sets, even if it seems (intuitively) like you could. I hope this helps.Chowell2000 00:32, 28 July 2007 (UTC)[reply]

Need to distinguish between "constructive proof" and "constructivist proof"

A constructive proof is just one that shows the existence of something by explicitly constructing it. These proofs -- as far as most mathematicians are concerned -- often employ the law of the excluded middle in their reasoning (contrary to what the article states).

On the other hand, a constructivist proof is one that uses a different form of logic, which indeed disallows the law of the excluded middle.

This distinction needs to be made clear in the article.Daqu (talk) 20:44, 23 November 2007 (UTC)[reply]