通过Coq的Axiom关键字添加额外公理能否让Coq具备图灵完备性？

不存在可通过Coq Gallina的Axiom关键字定义、能让Coq变为图灵完备的公理，核心原因如下：

• Gallina中公理的本质是向类型系统宣告「存在对应类型的一个项」，不会引入任何新的归约/求值规则，本身没有任何计算行为。Coq的求值器遇到公理项时会直接停止处理，不会做额外的展开或计算。
• Coq的强规范化属性是由类型系统核心规则保障的：所有合法的Gallina项必然会在有限步内归约到范式，该规则不会因为新增公理声明发生改变。
• 哪怕引入会导致逻辑不一致的公理（比如Axiom cheat : False），最多只会让Coq的逻辑系统失去可靠性（可推导出任意命题为真），但不会破坏强规范化属性：哪怕你用False_rect从矛盾公理导出任意类型的项，这些项的求值过程依然是有限的，不会出现无限循环，自然无法满足图灵完备要求的「可构造不终止计算」的条件。
• 能让Coq变为图灵完备的操作（比如关闭守卫检查Unset Guard Checking、通过命令行参数修改类型系统核心规则等），都不属于Axiom关键字可以实现的范畴，和你限定的公理定义不符。

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