7 ms·

I find baring the law of the excluded middle an unnecessarily restrictive basis for logic; but regardless, isn't this a simple (A \/ ~A) case? I mean, you may n

I find baring the law of the excluded middle an unnecessarily restrictive basis for logic; but regardless, isn't this a simple (A \/ ~A) case? I mean, you may not be able to prove that Anne is married or prove that Anne is unmarried, but can't you prove by that Anne is either married or unmarried, by the definition of marriege? Moreover, I had the idea that Intuitionistic logic is advocated to curb with non-constructive proofs over non-finite sets rather than the simple case you mentioned.

yodsanklai 12y ago
"I find baring the law of the excluded middle an unnecessarily restrictive basis for logic" I agree that it doesn't seem to make sense in that case. However, there are practical use for constructive proofs, for instance, program extraction. Consider a proposition such that "for all list L, there is a list L' such that L' is sorted and L' is a permutation of L". From a constructive proof of that proposition, you can extract a sorting algorithm. This works basically because the constructive proof has to exhibit a witness. That's the kind of things you can do with the Coq proof assistant. "you may not be able to prove that Anne is married or prove that Anne is unmarried, but can't you prove by that Anne is either married or unmarried, by the definition of marriege?" You can't prove it in constructive logic. You can always add an axiom of the form "for all x, x is married or x is not married". However, if you do that, your proof won't be constructive anymore (unless you provide a decision procedure together with your axiom).
btilly 12y ago
I find baring the law of the excluded middle an unnecessarily restrictive basis for logic... And that attitude combined with a long chain of reasoning will wind up with you accepting that the following are entirely sensible statements. "I accept that there exist real numbers which cannot ever be specified." "I accept that there exists a reasonable computer science problem for which there exists a polynomial time algorithm but for which I cannot ever prove any algorithm correct." If you do accept them as reasonable, it is worth carefully considering what the word "exists" actually means to you, and how someone else might think it should mean something different. IF you come to the conclusion that it should mean something different than what is implied by those statements, then you should take another look at constructivism. :-)
- maaku 12y ago
  There does exist real numbers that cannot be specified in (finite) space or time...
  - sukilot 12y ago
    This is what btilly is talking about. To parahrase: "there exist entities that cannot ever be constructed or named in any Universe like ours"
  - btilly 12y ago
    According to classical mathematics, this is true. I can make the statement even stronger. There are real numbers which not only cannot be specified, but are strongly not compressible. That is, for the first n digits, there is no significantly more efficient way to specify what they are than to just list them. But we are now talking about the existence of something that cannot be specified or written down in any useful way, shape, or form. What does it actually mean to say that this exists? We've demonstrated that no direct evidence of existence can ever be found. This is pretty much the opposite of what a lot of people would actually want "existence" to mean. From a classical point of view what is wrong is your notion of existence. But it is perfectly reasonable to instead conclude that it is classical mathematics which has gone off the rails and they are now using words like "existence" in a nonsensical way. Both points of view are perfectly defensible. In fact it was proven by Goedel that any inconsistency in one leads to an inconsistency in the other. Therefore neither is actually able to claim to have a better grounding in logical consistency than the other. Historically the debate was that classical mathematics is more convenient to work with, while constructivism actually means something more reasonable. But once the set paradoxes faded, and with no difference in consistency, the simplicity of classical mathematics won.
    - darkmighty 12y ago
      So what's constructivism useful for anyway? Why change the basis of logic instead of proving non-constructability within the reasonable existing logics? (E.g. prove a real number isn't constructable instead of foregoing it's existence) There are also cases of interest beyond constructivism: what if a number is non-constructible but can be approximated? Saying it doesn't exist doesn't sound particularly useful.
Rapzid 12y ago
What if Anne is a dog and can't be married? It was never established that three PEOPLE were looking at each other.
- dmitrig01 12y ago
  In that case, Anne is unmarried
  - reader_1000 12y ago
    However, it is not a person.
- phaemon 12y ago
  You posted this same comment twice, and four hours after I originally suggested Anne might be a dog. Could you not at least have gone for a cat?
  - Rapzid 12y ago
    I accidentally replied under the OP when I meant to reply under this thread, so I stripped out the part most relevant and put it here. Dog was the first thing that came to my head that would have a proper noun(Name) that wasn't a person. Didn't see a reason to change it? Interestingly though, I do prefer cats.
- sukilot 12y ago
  That's mincing words, considering the whole prpblem a trick because maybe no one is a person. That resoning also shows that the "next item in a finite sequence" questions can have any equally correct answer. It doesn't hold up to Occam's Razor.
raverbashing 12y ago
Yes, it all depends on the dichotomy of Married/Not Married. If other states are allowed, then it's not possible to determine

yodsanklai 12y ago

"I find baring the law of the excluded middle an unnecessarily restrictive basis for logic" I agree that it doesn't seem to make sense in that case. However, there are practical use for constructive proofs, for instance, program extraction. Consider a proposition such that "for all list L, there is a list L' such that L' is sorted and L' is a permutation of L". From a constructive proof of that proposition, you can extract a sorting algorithm. This works basically because the constructive proof has to exhibit a witness. That's the kind of things you can do with the Coq proof assistant. "you may not be able to prove that Anne is married or prove that Anne is unmarried, but can't you prove by that Anne is either married or unmarried, by the definition of marriege?" You can't prove it in constructive logic. You can always add an axiom of the form "for all x, x is married or x is not married". However, if you do that, your proof won't be constructive anymore (unless you provide a decision procedure together with your axiom).

btilly 12y ago

I find baring the law of the excluded middle an unnecessarily restrictive basis for logic... And that attitude combined with a long chain of reasoning will wind up with you accepting that the following are entirely sensible statements. "I accept that there exist real numbers which cannot ever be specified." "I accept that there exists a reasonable computer science problem for which there exists a polynomial time algorithm but for which I cannot ever prove any algorithm correct." If you do accept them as reasonable, it is worth carefully considering what the word "exists" actually means to you, and how someone else might think it should mean something different. IF you come to the conclusion that it should mean something different than what is implied by those statements, then you should take another look at constructivism. :-)

maaku 12y ago
There does exist real numbers that cannot be specified in (finite) space or time...
- sukilot 12y ago
  This is what btilly is talking about. To parahrase: "there exist entities that cannot ever be constructed or named in any Universe like ours"
- btilly 12y ago
  According to classical mathematics, this is true. I can make the statement even stronger. There are real numbers which not only cannot be specified, but are strongly not compressible. That is, for the first n digits, there is no significantly more efficient way to specify what they are than to just list them. But we are now talking about the existence of something that cannot be specified or written down in any useful way, shape, or form. What does it actually mean to say that this exists? We've demonstrated that no direct evidence of existence can ever be found. This is pretty much the opposite of what a lot of people would actually want "existence" to mean. From a classical point of view what is wrong is your notion of existence. But it is perfectly reasonable to instead conclude that it is classical mathematics which has gone off the rails and they are now using words like "existence" in a nonsensical way. Both points of view are perfectly defensible. In fact it was proven by Goedel that any inconsistency in one leads to an inconsistency in the other. Therefore neither is actually able to claim to have a better grounding in logical consistency than the other. Historically the debate was that classical mathematics is more convenient to work with, while constructivism actually means something more reasonable. But once the set paradoxes faded, and with no difference in consistency, the simplicity of classical mathematics won.
  - darkmighty 12y ago
    So what's constructivism useful for anyway? Why change the basis of logic instead of proving non-constructability within the reasonable existing logics? (E.g. prove a real number isn't constructable instead of foregoing it's existence) There are also cases of interest beyond constructivism: what if a number is non-constructible but can be approximated? Saying it doesn't exist doesn't sound particularly useful.

Rapzid 12y ago

What if Anne is a dog and can't be married? It was never established that three PEOPLE were looking at each other.

dmitrig01 12y ago
In that case, Anne is unmarried
- reader_1000 12y ago
  However, it is not a person.
phaemon 12y ago
You posted this same comment twice, and four hours after I originally suggested Anne might be a dog. Could you not at least have gone for a cat?
- Rapzid 12y ago
  I accidentally replied under the OP when I meant to reply under this thread, so I stripped out the part most relevant and put it here. Dog was the first thing that came to my head that would have a proper noun(Name) that wasn't a person. Didn't see a reason to change it? Interestingly though, I do prefer cats.
sukilot 12y ago
That's mincing words, considering the whole prpblem a trick because maybe no one is a person. That resoning also shows that the "next item in a finite sequence" questions can have any equally correct answer. It doesn't hold up to Occam's Razor.

raverbashing 12y ago

Yes, it all depends on the dichotomy of Married/Not Married. If other states are allowed, then it's not possible to determine