Timeline for Awfully sophisticated proof for simple facts
Current License: CC BY-SA 2.5
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 28, 2013 at 21:42 | comment | added | Todd Trimble | @PeteL.Clark I didn't see any indication from you of different meanings of 'constructive'; you said merely "as I understand the term..." followed by what you expect a constructive proof would look like. It also sounded like you were considering such proofs as being constructive. You should interpret my comment as saying such a proof would not be considered 'constructive' by the vast majority of mathematicians (e.g. Bishop as one point of reference, Brouwer as another) who understand 'constructivist' mathematics as involving avoidance of applications of PEM (principle of excluded middle). | |
| Aug 28, 2013 at 5:15 | comment | added | Pete L. Clark | @Todd: I'm not sure I understand your comment. As I indicated, the term "constructive" in mathematics can have several different technical meanings and can also be used more informally. But what I said was that by any reasonable interpretation of the term, the given argument is not constructive. So what did I say that was wrong? | |
| Aug 26, 2013 at 16:50 | comment | added | Todd Trimble | @TsuyoshiIto: even though you were just joking around, see my comment to Pete. You are correct that Cantor's theorem can be proven constructively, but that the number of functions from $\mathbb{R}$ to itself is of cardinality $2^c$ requires classical logic. | |
| Aug 26, 2013 at 16:43 | comment | added | Todd Trimble | @PeteL.Clark: both you and Tsuyoshi are wrong, because the existence of discontinuous functions on the reals cannot be proven without the use of classical logic. (In your example, you need the law of the excluded middle to decide whether or not a real number is zero.) In brief: just because you have a seemingly explicit construction doesn't mean it's constructive. See also Brouwer's theorem "all functions are continuous" in Mac Lane & Moerdijk's Sheaves in Geometry and Logic, VI.9. | |
| Oct 14, 2011 at 11:22 | comment | added | Max | While this is obviously overkill, the general technique is so useful that perhaps students should see this proof -- when cardinality is introduced, it's not immediately obvious just how useful it is. For example, even before saying what a computer program is (but knowing that they are specified by strings), one can deduce that there are uncomputable sets, and similarly non-regular languages, etc. I'd say the general idea is that we often have countably many descriptions (programs, grammars, restrictions to $\mathbf{Q}$) but uncountably many objects, so most objects cannot be described. | |
| Oct 18, 2010 at 22:41 | comment | added | Tsuyoshi Ito | @Pete: Of course, it is an extremely simple fact that there is a constructive example of a discontinuous real function. This proof is an awfully sophisticated proof of it (because Cantor’s theorem can be proved constructively, if I am not mistaken). But now I know that my joke fell flat…. | |
| Oct 18, 2010 at 11:24 | comment | added | Pete L. Clark | @Tsuyoshi: or do you mean that it doesn't look constructive but can be made so by a diagonalization argument or somesuch? | |
| Oct 18, 2010 at 11:23 | comment | added | Pete L. Clark | @Tsuyoshi: I don't follow. As I understand the term, a constructive proof of the existence of a discontinuous real function would be something like "Consider the characteristic function of the origin. Notice that it is discontinuous at zero because..." Komjath's answer is an exemplar of a nonconstructive proof. | |
| Oct 18, 2010 at 3:55 | comment | added | Tsuyoshi Ito | Also noteworthy is that this is a constructive proof of the existence of a discontinuous real function. | |
| Oct 17, 2010 at 20:40 | comment | added | Gerald Edgar | Same reasoning: there exists a non-Borel real function. Or there exists a non-Borel set of reals. Now it's not so extreme-seeming. | |
| Oct 17, 2010 at 18:42 | history | answered | Péter Komjáth | CC BY-SA 2.5 |