如何用给定的假设证明排除中间（forall P Q : Prop, (P -> Q) -> (~P \/ Q)）？答案

【问题标题】：How can I prove excluded middle with the given hypothesis (forall P Q : Prop, (P -> Q) -> (~P \/ Q))?如何用给定的假设证明排除中间（forall P Q : Prop, (P -> Q) -> (~P \/ Q)）？
【发布时间】：2021-12-25 10:17:32
【问题描述】：

我目前对如何证明以下定理感到困惑：

Theorem excluded_middle2 : 
 (forall P Q : Prop, (P -> Q) -> (~P \/ Q)) -> (forall P, P \/ ~P).

我被困在这里：

Theorem excluded_middle2 : 
  (forall P Q : Prop, (P -> Q) -> (~P \/ Q)) -> (forall P, P \/ ~P).
Proof.
  intros.
  evar (Q : Prop).
  specialize H with (P : Prop) (Q : Prop).

我知道在 coq 中不可能简单地证明排中律，但我真的很想知道用这个给定的定理是否可以证明排中律？

【问题讨论】：

标签： coq logical-foundations

【解决方案1】：

是的，你可以。使用 ssreflect 的一种方法如下（可能有更短的方法）：

Lemma orC P Q : P \/ Q -> Q \/ P.
Proof. by case; [right | left]. Qed.

Theorem excluded_middle2 : 
 (forall P Q : Prop, (P -> Q) -> (~ P \/ Q)) -> (forall P, P \/ ~ P).
Proof.
move=> orasimply P.
have pp : P -> P by [].
move: (orasimply P P pp).
exact: orC.
Qed.

【讨论】：