是否有`(A -> B \/ C) -> (A -> B) \/ (A -> C)`的直觉证明？

Question

以下是经典命题逻辑中的一个有用的引理。

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

向后的方向很容易证明。但我找不到前进方向的直观证明。我可以使用经典逻辑（排除中律）来证明上述命题。

您可以确认前进方向在经典逻辑中是可证明的。想想哥德尔完备定理吧。

现在我在想，也许

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

相当于

forall P: Prop, P \/ ~ P

。

我的问题如下：

(1)。是否有

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

的直观证明（不使用 LEM 或双重否定律）？

（2）。如果（1）的答案是否定的，那么我们可以证明

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

这是使用我上面提到的 LEM

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

的证明。

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.

我怀疑 (2) 也可以在 Coq 中证明。

Answer 1

没有(A -> B \/ C) -> (A -> B) \/ (A -> C)的

直觉

证明。请注意，

\/

的语法优先级高于

->

。

确实，人们可以找到一个 Kripke 计数器模型，这里使用我们团队多年前编写的

STRIP solver

进行计算。

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 }