哥德尔不完备定理

哥德尔不完备定理讨论的是形式算术理论，而不是日常知识是否可靠。理论给出公理和有效推理规则，证明是能够机械核查的有限步骤。一致性指不能同时推出某个句子及其否定；这里的完备性则指每个句子都能被证明或被否证。两者不是一回事。

适用对象还须有效公理化，并能够表达足够的自然数算术。第一定理可用于扩展罗宾逊算术等弱算术的理论。若省略这些前提，断言任何形式系统都不完备就不成立；把全部自然数真句直接当成公理，也不是一个满足有效公理化要求的补救方案。

参考：[2]

第一不完备定理的常见现代形式说：一致、有效公理化且足够强的算术理论，总有一个句子，使它和它的否定都不能在该理论内证明。罗瑟的改进使这一结论只需通常的一致性；哥德尔原来对特定句子不可否证的论证用了更强条件，不能混写。

关键是给符号串、公式及有限证明分配自然数编码，从而把“这个数编码了那个句子的证明”写成算术关系。固定点引理随后产生与自身不可证明性相联系的句子。所谓自指是精确的编码构造，不是直接把“这句话是假的”塞进算术，也不是让系统同时证明互相矛盾的话。

参考：[1]

第二不完备定理进一步限制内部的一致性证明。以皮亚诺算术为例，采用标准证明编码，将“一切数字都不编码出0＝1的证明”表达为一致性句子。如果该理论确实一致，它就不能在自身内推出这个句子。

这里须满足对可证明性谓词的适当可推导性条件；随便写一个声称表示一致性的公式，并不能自动套用结论。第二定理也不禁止在更强理论中证明较弱理论的一致性，或讨论相对一致性。它限制的是指定系统用自身资源完成某类证明的能力。

参考：[1]

“不可证明”总是相对于某套公理和规则。对标准自然数结构而言，一个算术句子有其真假；系统能否证明它是另一层问题。把一个原来独立的句子加入公理，可以解决这一句的可证性，但只要扩充后的理论仍满足定理前提，就还会有新的独立句子。

哥德尔的一阶逻辑完备定理说，公理的所有模型中都成立的语义后果可以由逻辑规则推出；不完备定理说，特定算术公理不能决定语言中的每个句子。前者谈逻辑推理是否足以捕捉语义后果，后者谈理论能决定多少内容，两者并不矛盾，更不能推出所有数学结论都不可信。

参考：[2]