可靠性与完备性

上级：logic

现代逻辑学的奠基性操作，是把一个逻辑系统拆分成两个先验上互不相关的侧面——然后证明它们重合。可靠性与完备性，就是这样的重合定理。

• syntax-and-semantics — 这个拆分本身：语法（⊢，证明 = 有限的、无意义的符号操作）对语义（⊨，模型中的真 = 意义）。这整个学科都建立在把两者拆开、再重新建立联系这件事上。
• soundness — ⊢ φ ⟹ ⊨ φ：一切可证的都为真（演算系统不撒谎）。容易的方向。
• completeness — ⊨ φ ⟹ ⊢ φ：一切为真的都可证（没有遗漏）。困难的方向（哥德尔，1929）。
• propositional-example — 在 P → (Q → P) 上同时看到两个方向（真值表 + 证明）。
• hilbert-godel-tarski — 这场拆分是如何诞生的：那场危机、希尔伯特纲领、塔斯基的真理论、哥德尔的完备性与不完备性。
• canonical-model — 典范模型/项模型：完备性究竟是如何被证明的（林登鲍姆 + 亨金 + 真值引理——语法变成模型），以三段论为例展开。

合起来：⊢ φ ⟺ ⊨ φ——可证性 = 真。同时满足这两者的证明系统，就是意义的一面忠实的镜子。

为什么它是基础性的

逻辑学想要两样看起来互不相容的东西：证明必须是机械的（可核查，不诉诸意义——希尔伯特的形式主义），但又必须能担保真（意义——塔斯基的语义学）。可靠性+完备性恰好就是这座桥梁：

• 通过证明来计算真——这是自动推理与证明助理的根基（一个可靠的内核，意味着一条被检查过的项确实为真）；
• 把可证性与真当作两个独立的对象来研究——这催生了证明论（语法）与模型论（语义）这两个独立的领域；
• 并且它们为哥德尔不完备性铺平了舞台：对于算术而言，语法与语义会分道扬镳——一个理论无法证明 ℕ 中的每一条真命题（见下面的告诫）。

这段历史的完整故事 → hilbert-godel-tarski。一个具体的命题逻辑演示 → propositional-example。

完备性 ≠ "不是不完备的"

证明系统的完备性（能证明所有有效的公式——一阶逻辑、命题逻辑）与哥德尔不完备性（一个理论无法证明其目标模型 ℕ 中为真的所有语句）是两回事。不要把它们混为一谈。