Coq中析取与互斥命题sumbool的转换证明问题

核心结论 #

在未引入额外公理的标准Coq系统中，以下命题无法证明：

Conjecture or_to_sumbool : forall P : Prop, P \/ ~P -> { P } + { ~P }.

原因解释 #

标准Coq基于直觉主义构造逻辑，其类型系统对Prop（命题层）和Set（数据/计算层）有严格区分：

• Prop层面的命题被设计为“证明无关”的，即不同的证明不携带可计算的信息；
• Set层面的类型要求具备可计算的实例，{P} + {~P}本质是要求给出一个可判定的结果——要么构造出P的证明，要么构造出~P的证明。

即使假设P \/ ~P（命题层的排中律），Coq的规则也禁止直接从Prop的析取中提取出Set层面的可判定结果，这会破坏Prop的证明无关性设计，因此无法通过常规推导完成证明。

与HoTT情况的差异 #

在同伦类型论（HoTT）中，对于任意mere proposition P，存在函数：

|| P + ~P || -> P + ~P

这是因为HoTT的命题截断||_||有特殊的消去规则：当目标类型本身是mere proposition时，可以从截断后的类型中提取内容。而对于mere prop P，P + ~P也满足mere prop的性质（若存在两个不同的元素会导致逻辑矛盾），因此可以应用截断消去规则完成构造。但这套规则是HoTT特有的，标准Coq中没有对应的机制，无法直接复用这个思路。

可证明的前提 #

如果给Coq添加额外公理，比如：

• 可数选择公理（Countable Choice）
• 描述公理（Description Axiom）
• 直接引入classic公理（即命题层排中律）结合允许从Prop到Set提取信息的规则

就可以证明该命题。例如，classic公理直接给出forall P, P \/ ~P，再配合选择类公理，就能将命题层的析取转化为Set层的可判定结果。

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