3 ms·

Aside to your aside: When A can be proven from B, and A can also be proven from !B, it is really tempting to conclude that A is proven. But many people will arg

by cvoss 2y ago

Aside to your aside: When A can be proven from B, and A can also be proven from !B, it is really tempting to conclude that A is proven. But many people will argue this is incorrect in general, that is, they deny the excluded middle axiom. What if B is independent of your system of logic? We know then that A is not disprovable (since a proof of !A would prove !B). But that doesn't prove A. Unless A can be proven without reference to B, A might be independent too.

BalinKing 2y ago
Not an expert, but I don't think that independence is particularly relevant—intuitionists deny LEM for more fundamental philosophical reasons AFAIK, even for statements that could theoretically be proven true or false within your system of logic.
- cvoss 2y ago
  I don't understand there to be anything deeper about it, though happy to be corrected. In a consistent system, there are three kinds of statements: the provable ones, the disprovable ones, and the independent ones. This is straight from Godel Incompleteness I. The sin of LEM is exactly that it overlooks the reality of incompleteness. But, if course, you also can't fix it with an axiom encoding the trichotomy I just stated, because the independence of a statement is itself a statement that lives in a higher ambient system.
  - whatshisface 2y ago
    LEM doesn't overlook completeness within the context of an axiom system. Independent results remain, by definition, without correspondence to any proof. Believe it or not, constructive math actually does have a LEM, but a derived one. Any computable value can be shown to either equal or not equal another. Only for uncomputable predicates does the absence of LEM result in our inability to conclude x from not not x.
bubblyworld 2y ago
Yeah, I believe it's invalid to conclude "B" from "A => B" and "not A => B" in constructive logic, for this reason. But most mathematicians reason classically without thinking twice about it!
- schoen 2y ago
  You can conclude "not not B", which is also called "B is irrefutable". Irrefutability is like a weaker version of "true" in constructive logic that means "could be assumed without introducing a new contradiction". https://en.wikipedia.org/wiki/Double-negation_translation https://en.wikipedia.org/wiki/Double-negation_translation
  - bubblyworld 2y ago
    How do you conclude that in this case? I've never spent much time reasoning intuitionistically, so I'm a bit slow! If I try to do it directly I keep using the law of excluded middle accidentally by assuming "A or not A" (or some consequence like contraposition if I try and apply your linked theorems).
    - schoen 2y ago
      Here is a quick and dirty Coq proof (which I'm sure could be simplified and cleaned up in various ways). Theorem foo: forall P Q: Prop, (P -> Q) /\ (~P -> Q) -> ~~Q. Proof. intros. destruct H. assert (~Q -> ~P). intros. intros contra. apply H in contra. contradiction. intros contra. apply contra. apply H1 in contra. apply H0 in contra. assumption. Qed. Sorry that may not go very far toward explaining why this is true or how to prove it outside of Coq. Let me think about what this is saying. First of all, contraposition (in the "adding a not" form, not in the "removing a not" form) is an intuitionistic theorem. And it is getting used here. So we are saying, use contraposition (here, prove contraposition) on P -> Q, to get ~Q -> ~P. Now, to show ~~Q, we want to show that ~Q would lead to a contradiction. (In Coq, ~X is literally defined as X -> False.) So, suppose ~Q. Then from that contraposition conclusion, we have ~P. But by hypothesis, ~P -> Q, so then Q. Then we have Q and ~Q, which is a contradiction. (To explicitly use the contradiction to deduce False, we can say "we have Q -> False and we have Q, therefore we can deduce False".) OK, I guess that wasn't so hard! Anyway, getting the contraposition consequence is actually very close to getting the desired result here. You just have to think in terms of "~~Q" meaning "~Q implies a contradiction". :-)

by cvoss 2y ago

BalinKing 2y ago

Not an expert, but I don't think that independence is particularly relevant—intuitionists deny LEM for more fundamental philosophical reasons AFAIK, even for statements that could theoretically be proven true or false within your system of logic.

cvoss 2y ago
I don't understand there to be anything deeper about it, though happy to be corrected. In a consistent system, there are three kinds of statements: the provable ones, the disprovable ones, and the independent ones. This is straight from Godel Incompleteness I. The sin of LEM is exactly that it overlooks the reality of incompleteness. But, if course, you also can't fix it with an axiom encoding the trichotomy I just stated, because the independence of a statement is itself a statement that lives in a higher ambient system.
- whatshisface 2y ago
  LEM doesn't overlook completeness within the context of an axiom system. Independent results remain, by definition, without correspondence to any proof. Believe it or not, constructive math actually does have a LEM, but a derived one. Any computable value can be shown to either equal or not equal another. Only for uncomputable predicates does the absence of LEM result in our inability to conclude x from not not x.

bubblyworld 2y ago

Yeah, I believe it's invalid to conclude "B" from "A => B" and "not A => B" in constructive logic, for this reason. But most mathematicians reason classically without thinking twice about it!

schoen 2y ago
You can conclude "not not B", which is also called "B is irrefutable". Irrefutability is like a weaker version of "true" in constructive logic that means "could be assumed without introducing a new contradiction". https://en.wikipedia.org/wiki/Double-negation_translation https://en.wikipedia.org/wiki/Double-negation_translation
- bubblyworld 2y ago
  How do you conclude that in this case? I've never spent much time reasoning intuitionistically, so I'm a bit slow! If I try to do it directly I keep using the law of excluded middle accidentally by assuming "A or not A" (or some consequence like contraposition if I try and apply your linked theorems).
  - schoen 2y ago
    Here is a quick and dirty Coq proof (which I'm sure could be simplified and cleaned up in various ways). Theorem foo: forall P Q: Prop, (P -> Q) /\ (~P -> Q) -> ~~Q. Proof. intros. destruct H. assert (~Q -> ~P). intros. intros contra. apply H in contra. contradiction. intros contra. apply contra. apply H1 in contra. apply H0 in contra. assumption. Qed. Sorry that may not go very far toward explaining why this is true or how to prove it outside of Coq. Let me think about what this is saying. First of all, contraposition (in the "adding a not" form, not in the "removing a not" form) is an intuitionistic theorem. And it is getting used here. So we are saying, use contraposition (here, prove contraposition) on P -> Q, to get ~Q -> ~P. Now, to show ~~Q, we want to show that ~Q would lead to a contradiction. (In Coq, ~X is literally defined as X -> False.) So, suppose ~Q. Then from that contraposition conclusion, we have ~P. But by hypothesis, ~P -> Q, so then Q. Then we have Q and ~Q, which is a contradiction. (To explicitly use the contradiction to deduce False, we can say "we have Q -> False and we have Q, therefore we can deduce False".) OK, I guess that wasn't so hard! Anyway, getting the contraposition consequence is actually very close to getting the desired result here. You just have to think in terms of "~~Q" meaning "~Q implies a contradiction". :-)