逻辑 · 证明的边界
哥德尔第一不完备性定理
即使证明规则明确、系统不会自相矛盾，也仍有它无法证明的算术真命题。
先约定一个数学证明系统
它从公理出发，按规则一步步推导。公理可以由算法列举，每份证明都能机械核查；它还足以表达基本的自然数算术，包括加法、乘法，并能用数字编码自己的语句与证明。
可靠性 不证明错的
只证明在通常的自然数中为真的命题。
涵盖全部真理 不漏掉对的
希望所有算术真命题，都能在系统内证明。
可靠性蕴含自洽性。自洽只要求：不能既证明一个命题，又证明它的否定。下面先假定系统自洽，看看证明的边界在哪里。
一个谈论自身证明的算术命题
“命题 G 无法在这个系统中被证明。”
G 说的是“我没有证明”，不是“我是假的”。这句话是数学编码后含义的通俗转述。
那么，G 能在这个系统中被证明吗？
试试两种假设，沿着推理走下去。
选择一个假设，查看它会带来什么。
这条路会违背自洽性
- 假设系统证明了 G。
那么，确实存在一份 G 的有限证明，可以给它编上一个自然数号码。
- 系统也能核查这份证明。
因此，它能推出“G 有证明”。但它刚证明的 G，表达的恰恰是“G 没有证明”。
- “有证明”与“没有证明”同时出现。
系统推出了互相否定的两个命题，这与我们假定的自洽性矛盾。
所以：如果系统自洽，它就不能证明 G。
这条路留下了一个无法证明的真命题
- 假设系统不能证明 G。
也就是：没有任何自然数，编码了一份这个系统认可的 G 的证明。
- 再读一遍 G。
它说的正是“我在这个系统中没有证明”。于是，从系统外看，G 在通常的自然数中为真。
- 真，却无法在系统内证明。
“涵盖全部算术真理”的愿望落空了。这里没有产生逻辑矛盾，而是发现了证明能力的边界。
所以：系统内的可证明性，无法囊括全部算术真理。
两条路，一个边界
规则能机械执行，又足以表达基本算术：
这样的系统，如果自洽，就不完备。
准确地说，总有一个算术命题，系统既不能证明它，也不能证明它的否定。这是第一不完备性定理的现代形式（含罗瑟的加强）。
直观推演与完整定理，还有什么区别？
上面的演示说明：在自洽的前提下，标准哥德尔句 G 不可证明，并在通常的自然数中为真。我们在系统外，借助对系统自洽性的假设得出这一结论；这不是系统内部的一份 G 的证明。
逻辑学中的“完备”通常指：每个语句，系统都能证明它或它的否定。仅凭上面对 G 的推演，还没有排除系统证明 G 的否定。哥德尔原来的论证用更强的“ω-自洽性”排除这一情形；罗瑟后来改造了所构造的语句，使普通自洽性就足以保证两边都不可证明。
自然语言中的自我指涉本身不是证明。严格论证通过哥德尔编码与对角引理，构造一个真正的算术语句，使系统内可证明“G 等价于 G 没有系统内证明”。这里的“真”，始终指通常的自然数解释。
这为什么重要？
真理与证明，是两个层次
“是真的”与“能从这套公理推出”并不等同。无法在一个系统中证明，也不意味着永远无法证明：换用更强的公理，有时就能继续前进。
没有一套规则能包办全部算术真理
可以扩充公理，但只要新的系统仍然自洽、可有效公理化且足够强，不完备性就仍然适用。它揭示的是每一套这类固定规则的边界，而不是数学推理失去了价值。
算法也有原则性的边界
图灵证明，不存在一个总能给出正确答案的通用算法，判断任意程序在给定输入下是否会停止。这种与自我指涉有关的限制，与不完备性密切相连；它不只是“计算太慢”。