5 ms·
"Jack is looking at Anne, but Anne is looking at George. Jack is married, but George is not. Is a married person looking at an unmarried person?" On a side not
by yodsanklai 12y ago
"Jack is looking at Anne, but Anne is looking at George. Jack is married, but George is not. Is a married person looking at an unmarried person?"
On a side note, in constructive propositional logic, the answer is indeed C (http://en.wikipedia.org/wiki/Intuitionistic_logic http://en.wikipedia.org/wiki/Intuitionistic_logic). In this type of formalism, you have to provide a witness for every existential, or choice for every disjunction. In particular the law of excluded middle isn't an axiom. In order to prove the above proposition, you would need to be able to prove whether Anne is married, or unmarried.
- cscurmudgeon 12y agoYes. But "background logic" (which classical first-order logic strives to model) is needed to prove meta theorems about any of the constructive logics. While the object-level proofs in some constructive/intuitionistic logic might do away with the law of excluded middle, the meta-theoretics proofs (proofs of theorems about the formalism) usually use them quite freely. My point is that there is no formalism that can ignore LEM at all levels (informal --> meta-theoretical--> object). The constructive logics are quite useful for things like program generation but I am not sure if we should use them as a model for human reasoning.
- enord 12y agoWas going to point this out as well. For a moment I almost resigned myself to be among the 80%, luckily I found a way to smug myself out of self-perceived mediocrity.
- deleted 12y ago[deleted]
- darkmighty 12y agoI 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 agoI 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. :-)
- tunesmith 12y agoCan someone explain this further to me? For instance, I thought that constructive logic merely says that not-not-A is not necessarily equal to A. In other words, truth is more about whether A is "provable" while not-A means "not provable", while it's perfectly possible for it to be unknowable whether something is provable. However, in constructive logic isn't it still fine to restrict a value to one of only two values? For instance, it's still valid to say that (for the sake of argument) someone can only be married or unmarried, in constructive logic, right? So therefore, of someone isn't married, they are unmarried by definition - because we're not talking about values of truth/provability. Right? So in other words, if we agree that someone can only be married or unmarried (which I take as an assumed premise in this problem), wouldn't the answer still be A in constructive/intuitionist logic?
- htns 12y agoI'm no expert, but as I understand induction is also a form of this kind of "case reasoning", so to get anything much done you will have to introduce some extra axioms, even if you omit the excluded middle.
- sukilot 12y agoDeduction not induction, but yes.
- deleted 12y ago[deleted]
- sukilot 12y agoYes, if you assume (M1(p) or not M1(p)) for a specific M1.