关于满足初等算术要求的形式系统中是否存在既不可证真、不可证伪也无法证明其独立性的语句的技术问询

嗨，这个问题问得特别好——其实在数理逻辑领域，这类“连独立性都无法被系统自身证明”的语句确实是存在的，咱们慢慢拆解清楚：

首先对齐咱们的基础共识：你提到的哥德尔第一不完备性定理、连续统假设（CH）独立于ZFC，这些都是理解的前提。咱们要找的是这样一个语句φ，对于满足初等算术要求的一致形式系统F：

• F既证不出φ为真，也证不出φ为假（也就是φ在F里不可判定）
• 同时，F也没办法证明“φ独立于F”——换句话说，F没法推导出“我既证不出φ也证不出¬φ”这个结论

怎么构造出这样的语句？ #

核心还是用哥德尔的自指技巧，类似构造哥德尔语句的思路，但要多绕一层：
我们可以利用形式系统能编码自身证明关系的特性，构造一个自指语句φ，它的“语义”等价于：

“我在F中是不可判定的，并且F不能证明我是不可判定的”

通过递归定理（数理逻辑里构造自指语句的核心工具），这样的语句是可以严格构造出来的。咱们来验证它的性质：

1. φ在F中不可判定：
   假设F是一致的。如果F能证明φ，那根据φ的自指内容，F就会同时证明“我不可判定”，但F已经证出φ了，这就矛盾了；同理，F也不能证明¬φ——因为如果F证出¬φ，那就意味着要么φ是可证的，要么F能证明φ不可判定，但前者和F的一致性矛盾，后者又会和¬φ的内容结合，推出F能证明φ不可判定，可这时候φ其实是不可判定的，F证出¬φ又会和这个事实矛盾。所以φ确实在F中既不可证真也不可证伪。
2. F无法证明φ的独立性：
   如果F能证明“φ独立于F”（也就是F能推导出“我既证不出φ也证不出¬φ”），那根据φ的自指内容，φ就等价于这个独立性语句加上“F不能证明这个独立性”，那F证出独立性的话，就会直接证出¬φ，这又回到了刚才的矛盾。所以F绝对没办法证明φ的独立性。

这样一来，φ就完美满足了你提出的三个条件。

关于扩展系统的问题 #

你问到如果把φ加到F里得到新系统F'=F+φ，F'能不能证明φ的独立性？其实在F'里，φ是作为公理加进去的，所以F'直接就能证出φ，自然φ在F'里是可证的，根本不独立，所以F'会明确证明“φ在F'中是可证的”，也就是不具备独立性。

如果是问F'能不能证明φ在原系统F中的独立性？那根据哥德尔第二不完备性定理，F'=F+φ是一致的（因为F不能证¬φ），但F'不能证明自身的一致性，而“φ在F中不可判定”等价于“F+φ是一致的，且F+¬φ也是一致的”。F'要证明“F+φ一致”其实就是证明自身一致，但它做不到；同时F'也没法证明“F+¬φ一致”，所以F'也没法证明φ在原系统F中的独立性。

最后聊聊“永远不知道”这件事 #

其实这正是数理逻辑里很迷人的一点：形式系统的边界是客观存在的，这种“多层不可知”的语句就是边界的直观体现，但这也不是什么值得沮丧的事——反而让我们更清晰地认识到形式化方法的能力范围，这也是逻辑研究最有价值的地方之一。

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