A proof is “constructive” if it doesn’t depend (implicitly or explicitly) on proof by contradiction. A roughly equivalent way to say this is, which I think is the reason for the name “constructive”, is that if you want to prove “there exists x such that P(x)” you need to do it by actually exhibiting such an x, rather than by saying “suppose there is none …” and deriving a contradiction.
Some mathematicians outright reject the tactic of proof by contradiction, and correspondingly also reject the “law of the excluded middle” which states that for any p, either p or not-p must be true. (These mathematicians are rather puzzlingly called “intuitionists”. The original motivation for this position was the idea that mathematics is a human creation, that when one asserts a mathematical proposition one is really gesturing towards some sort of mental construction that corresponds to it; so, say the intuitionists, when you assert that some mathematical entity exists, you’d better actually have an instance of it in mind.) Others consider that non-constructive proofs are valid but that constructive proofs are better.
Why would one prefer a constructive proof? The obvious reason is that in some sense it tells you more. If you have a constructive proof that a certain kind of thing exists, you can (in principle) use that to find such a thing; if you only have a non-constructive proof then you might remain unable to do that.
Another reason would be that you actually do want to allow some propositions to have no truth-values, or truth-values other than “true” and “false”. E.g., you might want a system that allows explicitly for ambiguity or uncertainty or something of the kind. Intuitionism kinda falls into this category; the “third” truth value might be called “incomplete” or “unknown” or something.
There are also interesting connections between the kind of restricted logic you need to use to invalidate non-constructive proofs (in which, as I mentioned above, “p or not-p” is not a theorem) and computer programs. Specifically, there’s a thing called the Curry-Howard isomorphism that says that types (in the programming-language sense) correspond to propositions in logic, and then explicit objects of those types correspond to constructive proofs of those propositions.
Disclaimer: it’s years since I studied any of this stuff, so there may be errors in the above; and I have never been an intuitionist nor found intuitionism credible, so I may not have presented it very fairly.
I am very inexperienced in this particular part of formal set theory, but I was always informally told that the main reason the distinction between constructive and non-constructive proofs is related to the Curry-Howard Correspondence, which informally states that constructive proofs can be rewritten into computer algorithms, whereas non-constructive proofs can not.
Can you elaborate? What is a constructive proof? Why should one care?
A proof is “constructive” if it doesn’t depend (implicitly or explicitly) on proof by contradiction. A roughly equivalent way to say this is, which I think is the reason for the name “constructive”, is that if you want to prove “there exists x such that P(x)” you need to do it by actually exhibiting such an x, rather than by saying “suppose there is none …” and deriving a contradiction.
Some mathematicians outright reject the tactic of proof by contradiction, and correspondingly also reject the “law of the excluded middle” which states that for any p, either p or not-p must be true. (These mathematicians are rather puzzlingly called “intuitionists”. The original motivation for this position was the idea that mathematics is a human creation, that when one asserts a mathematical proposition one is really gesturing towards some sort of mental construction that corresponds to it; so, say the intuitionists, when you assert that some mathematical entity exists, you’d better actually have an instance of it in mind.) Others consider that non-constructive proofs are valid but that constructive proofs are better.
Why would one prefer a constructive proof? The obvious reason is that in some sense it tells you more. If you have a constructive proof that a certain kind of thing exists, you can (in principle) use that to find such a thing; if you only have a non-constructive proof then you might remain unable to do that.
Another reason would be that you actually do want to allow some propositions to have no truth-values, or truth-values other than “true” and “false”. E.g., you might want a system that allows explicitly for ambiguity or uncertainty or something of the kind. Intuitionism kinda falls into this category; the “third” truth value might be called “incomplete” or “unknown” or something.
There are also interesting connections between the kind of restricted logic you need to use to invalidate non-constructive proofs (in which, as I mentioned above, “p or not-p” is not a theorem) and computer programs. Specifically, there’s a thing called the Curry-Howard isomorphism that says that types (in the programming-language sense) correspond to propositions in logic, and then explicit objects of those types correspond to constructive proofs of those propositions.
Disclaimer: it’s years since I studied any of this stuff, so there may be errors in the above; and I have never been an intuitionist nor found intuitionism credible, so I may not have presented it very fairly.
https://en.wikipedia.org/wiki/Constructive_proof
I am very inexperienced in this particular part of formal set theory, but I was always informally told that the main reason the distinction between constructive and non-constructive proofs is related to the Curry-Howard Correspondence, which informally states that constructive proofs can be rewritten into computer algorithms, whereas non-constructive proofs can not.