4 ms·

This is a nice proof. I just want to mention that it is also completely constructive - all objects involved are finite and so exhaustive search supplies the nec

by fmap 10y ago

This is a nice proof. I just want to mention that it is also completely constructive - all objects involved are finite and so exhaustive search supplies the necessary instance of excluded middle. We really don't have a good terminology for distinguishing between efficient constructive proofs (those corresponding to efficient algorithms) and inefficient ones...

philtar 10y ago
Isn't computational complexity the terminology you're looking for?
- fmap 10y ago
  Yes, this is a good idea. What I'm concerned about is that there is no standard terminology. The paper - and another comment in here! - is talking about the proof being "non-constructive", when in reality it is a constructive proof in 2-EXPTIME. I'm only nitpicking here, because I'm seeing this a lot...
  - gohrt 10y ago
    By your definition, what's an example of a non-constructive proof (of any theorem ) ?
    - fmap 10y ago
      Any proof using an instance of excluded middle or choice which is not constructively valid. For example, see the first proof on this page: http://www.cut-the-knot.org/do_you_know/irrat.shtml http://www.cut-the-knot.org/do_you_know/irrat.shtml
Chinjut 10y ago
Every proof of this theorem, by any reasoning, would be constructive by the same criteria. You can always do an exhaustive search to determine whether p is a sum of two squares. (Of course, it's not obvious when solutions exist and when they don't; that's what the proof is for. But that doesn't come up in your evaluation of whether the proof is constructive.) This is thus more a property of the theorem than a distinctive property of the proof. But, yes, the theorem is valid even in intuitionistic mathematics.
- 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!
dsp1234 10y ago
The PDF itself seems to say otherwise: "Note that the proof is not constructive: it does not give a method to actually find the representation of p as a sum of two squares"
- Chinjut 10y ago
  This is the terminology distinction fmap is noting with "We really don't have a good terminology for distinguishing between efficient constructive proofs (those corresponding to efficient algorithms) and inefficient ones...". The PDF calls the proof non-constructive in that it does not provide an efficient algorithm; however, fmap calls it constructive in that it does provide an inefficient algorithm.
Ar-Curunir 10y ago
> We really don't have a good terminology for distinguishing between efficient constructive proofs (those corresponding to efficient algorithms) and inefficient ones... We do: the complexity classes P and NP. Ok, technically this is a polynomial time decidable language (does there exist etc. etc.), so perhaps consider FP and FNP (the function variants of P & NP).

by fmap 10y ago

philtar 10y ago

Isn't computational complexity the terminology you're looking for?

fmap 10y ago
Yes, this is a good idea. What I'm concerned about is that there is no standard terminology. The paper - and another comment in here! - is talking about the proof being "non-constructive", when in reality it is a constructive proof in 2-EXPTIME. I'm only nitpicking here, because I'm seeing this a lot...
- gohrt 10y ago
  By your definition, what's an example of a non-constructive proof (of any theorem ) ?
  - fmap 10y ago
    Any proof using an instance of excluded middle or choice which is not constructively valid. For example, see the first proof on this page: http://www.cut-the-knot.org/do_you_know/irrat.shtml http://www.cut-the-knot.org/do_you_know/irrat.shtml

Chinjut 10y ago

Every proof of this theorem, by any reasoning, would be constructive by the same criteria. You can always do an exhaustive search to determine whether p is a sum of two squares. (Of course, it's not obvious when solutions exist and when they don't; that's what the proof is for. But that doesn't come up in your evaluation of whether the proof is constructive.) This is thus more a property of the theorem than a distinctive property of the proof. But, yes, the theorem is valid even in intuitionistic mathematics.

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!

dsp1234 10y ago

The PDF itself seems to say otherwise: "Note that the proof is not constructive: it does not give a method to actually find the representation of p as a sum of two squares"

Chinjut 10y ago
This is the terminology distinction fmap is noting with "We really don't have a good terminology for distinguishing between efficient constructive proofs (those corresponding to efficient algorithms) and inefficient ones...". The PDF calls the proof non-constructive in that it does not provide an efficient algorithm; however, fmap calls it constructive in that it does provide an inefficient algorithm.

Ar-Curunir 10y ago

> We really don't have a good terminology for distinguishing between efficient constructive proofs (those corresponding to efficient algorithms) and inefficient ones... We do: the complexity classes P and NP. Ok, technically this is a polynomial time decidable language (does there exist etc. etc.), so perhaps consider FP and FNP (the function variants of P & NP).