关于蕴含分配律的直觉主义可证性及与排中律等价性的求证

引理说明 #

经典命题逻辑中有如下实用引理：

(A -> B ∨ C) ↔ (A -> B) ∨ (A -> C)

该引理的反向推导易于证明，但正向推导无法找到直觉主义证明，不过可以借助*经典逻辑（排中律LEM）*完成证明。可通过哥德尔完备性定理验证正向推导在经典逻辑中的可证性，也可参考真值表验证。

我猜想命题∀ A B C: Prop, (A -> B ∨ C) -> (A -> B) ∨ (A -> C)与排中律∀ P: Prop, P ∨ ¬P等价，现提出以下问题：

问题(1) #

是否存在不使用排中律或双重否定律的直觉主义证明，来证明(A -> B ∨ C) -> (A -> B) ∨ (A -> C)？

问题(2) #

若问题(1)的答案为否，能否证明：

(∀ A B C: Prop, (A -> B ∨ C) -> (A -> B) ∨ (A -> C)) -> 
    ∀ P: Prop, P ∨ ¬P

经典逻辑下的Coq实现 #

以下是我使用排中律完成的(A -> B ∨ C) -> (A -> B) ∨ (A -> C)的Coq证明代码：

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中完成证明。

内容的提问来源于stack exchange，提问作者mindconnect.cc