To make this into a proper article, we need some examples of nonconstructive proofs, and discussion thereof.
To make this into a proper article, we need some examples of nonconstructive proofs, and discussion thereof.
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)
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)
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)
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)
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)
The current (ie. as of May 24 2006) revision of this article provides the following as the last example of a 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)
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)
My understanding of an existence proof (or, to be more precise, a pure existence proof) is a proof that goes like this:
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)
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)
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)
Informasi ini disarikan dari Wikipedia dan disajikan kembali untuk tujuan edukasi. Konten tersedia di bawah lisensi CC BY-SA 3.0. Kami tidak bertanggung jawab atas ketidakakuratan data yang bersumber dari kontribusi publik tersebut.