4 ms·

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 w

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". :-)
    - bubblyworld 2y ago
      Ah, thanks! My blocker was that I thought contraposition wasn't valid at all in intuitionistic logic, but actually the one direction still holds, i.e "(P -> Q) -> (not Q -> not P)" is a tautology. In the other direction you get "(not Q -> not P) -> (P -> not not Q)" instead which is basically what you said in the first place =)
      - schoen 2y ago
        Yes, it's interesting how careful you have to be with what you can and can't do with negations. For example, some forms of De Morgan's Law work but some don't! These are valid intuitionistically: (P /\ Q) -> ~(~P \/ ~Q) (~P /\ ~Q) -> ~(P \/ Q) (P \/ Q) -> ~(~P /\ ~Q) ~(P \/ Q) -> (~P /\ ~Q) (~P \/ ~Q) -> ~(P /\ Q) These are not: ~(~P /\ ~Q) -> (P \/ Q) ~(P /\ Q) -> (~P \/ ~Q) ~(~P \/ ~Q) -> (P /\ Q) And with quantifiers, these are valid intuitionistically: (forall x, P x) -> (~exists x, ~P x) (exists x, P x) -> (~forall x, ~P x) ~(exists x, P x) -> (forall x, ~P x) But this isn't: ~(forall x, P x) -> (exists x, ~P x) (Assuming the existence of some x does not help here.)

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". :-)
  - bubblyworld 2y ago
    Ah, thanks! My blocker was that I thought contraposition wasn't valid at all in intuitionistic logic, but actually the one direction still holds, i.e "(P -> Q) -> (not Q -> not P)" is a tautology. In the other direction you get "(not Q -> not P) -> (P -> not not Q)" instead which is basically what you said in the first place =)
    - schoen 2y ago
      Yes, it's interesting how careful you have to be with what you can and can't do with negations. For example, some forms of De Morgan's Law work but some don't! These are valid intuitionistically: (P /\ Q) -> ~(~P \/ ~Q) (~P /\ ~Q) -> ~(P \/ Q) (P \/ Q) -> ~(~P /\ ~Q) ~(P \/ Q) -> (~P /\ ~Q) (~P \/ ~Q) -> ~(P /\ Q) These are not: ~(~P /\ ~Q) -> (P \/ Q) ~(P /\ Q) -> (~P \/ ~Q) ~(~P \/ ~Q) -> (P /\ Q) And with quantifiers, these are valid intuitionistically: (forall x, P x) -> (~exists x, ~P x) (exists x, P x) -> (~forall x, ~P x) ~(exists x, P x) -> (forall x, ~P x) But this isn't: ~(forall x, P x) -> (exists x, ~P x) (Assuming the existence of some x does not help here.)