关于ZFC系统中可证性谓词χ(n)满足ZFC⊢χ(n)⇒ZFC⊢φ的条件的技术问询

咱们先从可证性谓词的基础概念聊起：假设$n$是公式$\phi$的哥德尔数，那么存在一个公式$\chi(n)$，它的含义是“ZFC证明了$\phi$”。直觉上你可能会觉得，如果ZFC能证明$\chi(n)$，那ZFC肯定也能证明对应的$\phi$——但实际上这个推论并不一定成立。

举个例子：如果$\phi$是矛盾式$1=0$，那对应的$\chi(n)$就是$\neg\text{Con(ZFC)}$（也就是“ZFC是不一致的”这个命题）。ZFC本身没法证明$\neg\text{Con(ZFC)}$，但这个命题和ZFC是一致的——也就是说，在ZFC+$\neg\text{Con(ZFC)}$这个扩充系统里，它会“声称自己能证明$1=0$”，但实际上它根本做不到这一点。

问题 #

什么时候会满足「若ZFC$\vdash\chi(n)$，则ZFC$\vdash\phi$」这个推论？

更新（2024年1月1日） #

我后来意识到，“ZFC$\vdash\chi(n)$蕴含ZFC$\vdash\phi$”这个说法可能存在矛盾，这和塔尔斯基定理有关：

塔尔斯基定理指出：如果理论$\Phi$是一致的，并且具备表示能力，那么$\Phi$的可证公式集合$\Phi^\vdash$无法在$\Phi$内部被表示。换句话说，不存在所谓的“真关系”$g(x)$，使得对于任意哥德尔数为$n$的公式$\phi$，$\Phi\vdash g(n)$当且仅当$\Phi\vdash\phi$。

而咱们这里的$\chi(n)$作为表达“ZFC证明$\phi$”的谓词，它的核心性质是：只要$n'$是公式$\phi'$的哥德尔数，$\chi(n')$就对应“ZFC证明$\phi'$”这个陈述。那如果对于所有的$n$，“ZFC$\vdash\chi(n)$就意味着ZFC$\vdash\phi$”都成立的话，$\chi(x)$不就正好是塔尔斯基定理里说不存在的那种表示吗？这就产生了明显的矛盾。

配图：来自Ebbinghaus所著《Logic》的塔尔斯基定理相关图示

备注：内容来源于stack exchange，提问作者Stephen Harrison