Coq中命题外延性是否存在不一致性？相关共识问询

目前Coq社区已形成明确共识：命题外延性在Coq的基础理论框架下是一致的。

关于早期邮件列表示例的说明 #

• 你提到的2013年邮件列表中声称能证明命题外延性不一致的示例，其问题根源并非命题外延性本身，而是当时Coq递归函数的定义机制存在缺陷。
• 后续Coq官方对递归函数的定义规则（尤其是涉及命题域递归的部分）进行了修正，这一修改直接消除了该示例中的矛盾场景，因此现在无法复现该问题。

当前的实践与结论 #

• 将命题外延性作为公理引入Coq是安全的，不会引发系统不一致。
• 在实际Coq开发中，命题外延性是常用的辅助公理，常用于简化高阶逻辑推理、证明等价命题的可互换性等场景，被广泛认可为可靠的扩展。

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