Search code examples
coq

Is there an intuitionistic proof of `(A -> B \/ C) -> (A -> B) \/ (A -> C)`?

Following is a useful lemma in classical propositional logic.

(A -> B \/ C) <-> (A -> B) \/ (A -> C).

The backward direction is easily proved. But I could not find an intuitionistic proof of the forward direction. I could prove above proposition using classical logic(Law of Excluded Middle) though.

You can confirm that the forward direction is provable in classical logic. Just think about the Godel's Completeness Theorem.

Truth table for forward direction

Now I am thinking, perhaps forall A B C: Prop, (A -> B \/ C) -> (A -> B) \/ (A -> C) is equivalent to forall P: Prop, P \/ ~ P.

My question is as follows:

(1). Is there an intuitionistic proof (not using LEM or double negation law) of (A -> B \/ C) -> (A -> B) \/ (A -> C)?

(2). If the answer to (1) is negative, then can we prove

(forall A B C: Prop, (A -> B \/ C) -> (A -> B) \/ (A -> C)) -> 
    forall P: Prop, P \/ ~ P`

Here is the proof of (A -> B \/ C) -> (A -> B) \/ (A -> C) using LEM I mentioned above.

From Coq Require Import Classical_Prop.

Fact imp_dist_or: forall A B C: Prop,
  (A -> B \/ C) -> (A -> B) \/ (A -> C).
Proof.
  intros.
  destruct (classic (A -> B)) as [H1 | H2].
  - left. exact H1.
  - right.
    intros Ha.
    apply H in Ha.
    destruct Ha as [Hb | Hc].
    + unfold not in H2.
      assert (Hab: A -> B).
      { intros HA. exact Hb. }
      apply H2 in Hab. destruct Hab.
    +  exact Hc.
Qed.

I suspect that (2) is also provable in Coq.

Solution

  • There is no intuitionistic proof of (A -> B \/ C) -> (A -> B) \/ (A -> C). Notice that \/ has higher syntactic priority that ->.

    Indeed, one can find a Kripke counter model of that, here computed using the STRIP solver written by our team many years ago.

    STRIP> define => (a->b|c)->(a->b)|(a->c); refute; kripke;
unprovable: => ((a->(b|c))->((a->b)|(a->c)))
Counter-model for => ((a->(b|c))->((a->b)|(a->c)))

0 : {  }
  1 : { a,c }
  2 : { a,b }