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

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 将不被接受]，但你可以安全地假设它；但是，它对您没有多大用处。