4 ms·

It's a bit more subtle than that. Operationally, the proof will end up being exhaustive search, but you also need a constructive termination proof. This is not

by fmap 10y ago

It's a bit more subtle than that. Operationally, the proof will end up being exhaustive search, but you also need a constructive termination proof. This is not a very helpful way to think about these things though. What I meant is that all principles used in this proof are constructive. You could, for example, literally translate this proof into a proof in type theory.

Chinjut 10y ago
Sure, but any classical proof of the theorem would automatically yield an intuitionistic (i.e., standard type-theory) proof as well; just run it through the double-negation translation, and then eliminate double-negations using the decidability of all relevant properties (i.e., of all instances of sub-formulae of the formula being proven). In some sense, this is just what you were saying, but my point is, this phenomenon ends up arising inevitably from the nature of the proposition being proven itself, and isn't surprising or distinctive for any particular proof of it (even if phrased ostensibly classically, such a proof might well be regarded as implicitly constructive regardless).
- 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 ago
    Sure, 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 ago
      Yeah, 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 ago
      Thanks for that post, that's interesting. Do you by chance have any pointers to a good textbook that covers these things?

by fmap 10y ago

Chinjut 10y ago

Sure, but any classical proof of the theorem would automatically yield an intuitionistic (i.e., standard type-theory) proof as well; just run it through the double-negation translation, and then eliminate double-negations using the decidability of all relevant properties (i.e., of all instances of sub-formulae of the formula being proven). In some sense, this is just what you were saying, but my point is, this phenomenon ends up arising inevitably from the nature of the proposition being proven itself, and isn't surprising or distinctive for any particular proof of it (even if phrased ostensibly classically, such a proof might well be regarded as implicitly constructive regardless).

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 ago
  Sure, 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 ago
    Yeah, 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 ago
    Thanks for that post, that's interesting. Do you by chance have any pointers to a good textbook that covers these things?