4 ms·

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

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.)

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.)