如果我不导入经典逻辑，你能证明 Coq 中的 Excluded Middle 是错误的吗

Question

我知道排除中间在构造逻辑中是不可能的。然而，当我尝试在 Coq 中展示它时，我陷入了困境。

Theorem em: forall P : Prop, ~P \/ P -> False.

我的做法是：

intros P H.
unfold not in H.
intuition.

系统说如下：

2 subgoals
P : Prop
H0 : P -> False
______________________________________(1/2)
False
______________________________________(2/2)
False

我应该如何进行？谢谢

Answer 1

你试图构造的不是 LEM 的否定，它会说“存在一些 P 使得 EM 不成立”，而是声称没有命题是可判定的，这当然会导致一个微不足道的不一致：

Axiom not_lem : forall (P : Prop), ~ (P \/ ~ P).

Goal False.
now apply (not_lem True); left.

无需使用花哨的双重否定引理；因为这显然是不一致的[想象一下它会成立！]

LEM 的“经典”否定确实是：

Axiom not_lem : exists (P : Prop), ~ (P \/ ~ P).

它是不可证明的[否则 EM 不会被接受]，但你可以安全地假设它；但它对你来说没有多大用处。