3 ms·
For the vast majority of proofs you are exactly right. There are some exceptions, though, since you don't necessarily have a choice principle, even under a doub
by fmap 10y ago
For the vast majority of proofs you are exactly right. There are some exceptions, though, since you don't necessarily have a choice principle, even under a double negation translation. This is why you need Markov's priniciple in addition to the double negation transform to give a constructive intrepretation to proofs from classical analysis.
You could rewrite this proof using some results from point set topology which typically require choice (the article even gives an outline on how to do this, weirdly enough). This rewritten proof would be non-constructive in a more precise sense, in that you couldn't translate it step-by-step.
- Chinjut 10y agoSure, Markov's principle matters for some things, but it seems to me Markov's principle doesn't really matter for this particular claim ("for every prime p, such-and-such a decidable property phi(p) is true"), since the only unbounded quantifier is the initial universal one. Any classical proof of a Pi_1 (or even Pi_2, using the Friedman translation) proposition can be straightforwardly turned into an intuitionistic proof of the same proposition (technically, I mean specifically that Peano Arithmetic is Pi_2-conservative over Heyting Arithmetic [and I suppose there are similar results for stronger systems but we don't need those]). So there is no surprise that this particular statement's proof is constructive, given that it is classically provable at all [again, technically, I am referring to classical provability in PA, but it would be shocking if Fermat's old proof, or any other anyone bothered with for a statement of this sort, had somehow relied on anything beyond PA]. For other more quantifier-complex classical theorems, it would be of more note to observe whether a particular proof could be made constructive (in the mere sense of intuitionistic mathematics) or not, but for this one, there's nothing to it. Anyway, I think I'm arguing pedantically about something there's no reason for me to argue about at all. Sorry about that! I think we're both in agreement that this is great, its constructiveness is great, math is great. Hooray!
- fmap 10y agoYeah, I don't think we actually disagree here... all I was saying is that there are proofs which are genuinely non-constructive, and this isn't one. You are arguing that this usage of "constructive" is basically meaningless for statements like this. It could only make a difference for artificial examples or artificially complicated proofs. This is definitely true. To be honest, I shouldn't have brought this up in the first place. I know what the author meant by claiming the proof is non-constructive (it doesn't give a formula for computing x,y such that x^2 + y^2 = p), and this is the idiomatic usage of the word non-constructive for this particular field. It's just different from the rest of the world, but that's nothing new.
- oggy 10y agoThanks for that post, that's interesting. Do you by chance have any pointers to a good textbook that covers these things?