如何在Coq的构造性逻辑中证明排中律不成立？

首先得指出你在定理定义上的小偏差：你写的Theorem em: forall P : Prop, ~P / P -> False其实是在试图证明“排中律蕴含矛盾”，但这和构造性逻辑中“排中律不成立”的意思并不一致。构造性逻辑只是不把排中律P \/ ~P当作默认公理，并不是说排中律本身是矛盾的——实际上在经典逻辑里排中律完全合法，只是构造性逻辑不接受它作为无需证明的规则。

回到你当前的证明状态：当你执行intros P H. unfold not in H. intuition.后得到的两个子目标：

1. P : Prop, H0 : P -> False ⊢ False
2. P : Prop ⊢ False

这两个子目标在构造性逻辑中都是无法证明的，原因很直接：

• 第一个子目标：你只有P->False（也就是~P），但要证False的话，需要一个P的证明来代入这个蕴含式，而你手里没有任何关于P的肯定性证据。
• 第二个子目标：直接要求证明False，这在一致的逻辑系统里是不可能的，除非系统本身存在矛盾。

那如果你想正确展示“排中律在构造性逻辑中不可证”，应该怎么做呢？

正确的方向：理解构造性逻辑中排中律的地位 #

在Coq的构造性逻辑中，我们无法证明全称的排中律：

Theorem em_unprovable : forall P : Prop, P \/ ~P.

如果你尝试去证明这个定理，比如执行intros P.之后，会发现没有任何构造性的方法生成P或者~P的证明——因为对于任意命题P，我们不一定能找到它的构造性证明，也不一定能找到它否定的构造性证明。

不过有趣的是，我们可以证明排中律的双重否定是成立的：

Theorem double_neg_em : forall P : Prop, ~~(P \/ ~P).
Proof.
  intros P H.
  unfold not in H.
  apply H.
  right.
  intros P0.
  apply H.
  left.
  exact P0.
Qed.

这说明排中律不是矛盾的，只是在构造性逻辑中无法被直接证明。

验证排中律不可证的另一种方式 #

Coq允许我们通过添加经典逻辑的公理来对比：导入Classical库后，你可以直接使用排中律：

Require Import Classical.

Theorem em_classical : forall P : Prop, P \/ ~P.
Proof.
  apply classic.
Qed.

这也侧面说明，排中律本身不是矛盾的，只是构造性逻辑不包含它作为公理。

总结一下：你之前的定理定义偏离了目标，当前的子目标无法证明是因为它们本身在构造性逻辑中就没有证明——这其实也从侧面反映了排中律不能被当作构造性逻辑的定理，因为如果它能被证明的话，你的原定理（排中律蕴含矛盾）就会导出系统矛盾，而Coq是一致的。

内容的提问来源于stack exchange，提问作者kengkeng