Coq构造性逻辑下缺失的德摩根律相关技术问询

Coq默认采用构造性逻辑，完整德摩根律中有2条无法构造性证明：

Theorem deMorgan_nand P Q (andPQ : ~(P /\ Q)) : P \/ Q.
Abort.

Theorem deMorgan_nall {A} (P : A -> Prop) (allPa : ~forall a, P a) : exists a, ~P a.
Abort.

这一特性是构造性逻辑的固有属性：构造性证明要求显式给出或命题、存在命题的成立实例，而该场景下无法通用地构造出对应实例。

常用的弱命题扩展定义如下：

Definition orW P Q := ~(~P /\ ~Q).
Definition exW {A} (P : A -> Prop) := ~forall a, ~P a.

基于上述定义可以证明合取非的替代德摩根律：

Theorem deMorgan_nand P Q (andPQ : ~(P /\ Q)) : orW (~P) (~Q).
  hnf; intros nnPQ; destruct nnPQ as [ nnP nnQ ].
  apply nnP; clear nnP; hnf; intros p.
  apply nnQ; clear nnQ; hnf; intros q.
  apply (andPQ (conj p q)).  
Qed.

但全称量词否定的对应形式以及另一条变体仍然无法证明：

Theorem deMorgan_nall {A} (P : A -> Prop) (allPa : ~forall a, P a) : exW (fun a => ~P a).
Abort.

Theorem deMorgan_nexn {A} (P : A -> Prop) (exPa : ~exists a, ~P a) : ~~forall a, P a.
Abort.

推导过程分别卡在~~P a到P a的转换、以及获取参数a后结论非False无法触发双重否定消去两个节点。

问题解答 #

1. 若deMorgan_nall不可证明，是否存在与之近似的等价定理？ #

纯构造性逻辑下有两类通用的近似方案：

• 保留构造性的弱结论形式：~forall a, P a -> ~~exists a, ~P a，该定理无需额外公理即可证明，仅将存在性结论弱化为双重否定形式，符合构造性逻辑要求。
• 添加前提增强证明能力：如果引入前提forall a, P a \/ ~P a（即谓词P的所有实例均可判定），则经典版本的deMorgan_nall可以直接证明；若论域A为有限类型，该可判定性前提可以自动推导，无需额外引入公理。

2. ~forall a, P a是否已是最简形式？ #

是的。在不含经典公理（排中律、选择公理等）的标准构造性逻辑体系中，~forall a, P a不存在等价的、不含全称量词否定的更简洁范式，是当前场景下的最简形式。仅在引入经典公理的前提下，才能将其等价转换为exists a, ~P a的存在形式。

3. 对于形如P : A -> Prop的带参数命题，是否存在类似结论为False时可用的排中律规则？ #

对应的通用规则为谓词可判定性公理，形式为forall (a : A), P a \/ ~P a，本质是排中律对谓词P的每一个实例都成立。除此之外还有两类构造性原生成立的规则可直接使用：

• 正向推导规则：(exists a, ~P a) -> ~forall a, P a，无前提限制，完全符合构造性要求。
• 否定场景双重否定消去规则：~~~(forall a, P a) -> ~(forall a, P a)，和单个命题的否定双重消去规则一致，结论为False时可直接调用。

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