可靠性
可靠性
Γ ⊢ φ ⟹ Γ ⊨ φ—— 任何你能证明的东西都是真的（在Γ的每一个模型中都真）。这套证明演算从不说谎。
证明——让真值沿着规则往下推（句法 → 语义）
这是容易的那个方向，走的是对推导做归纳——从 syntax to semantics 的这座桥是逐条规则、局部搭建起来的：
- 基础情形——公理： 检查每一条公理都是有效的（在所有模型中都为真）。（例如
P → (Q → P)——验证它的真值表，as in the example。） - 归纳情形——推理规则保真： 对每一条规则，只要前提为真，结论就为真。分离规则（Modus ponens）： 若
A在某个模型中为真，且A → B在该模型中也为真，那么B在该模型中也为真。 因此一条证明中的每一行，在前提的每一个模型中都为真；所以最后一行φ也为真。∎
整件事的内容就是：每一条规则都保真，所以真值沿着证明向下流动，从有效的公理一路流到结论。
不可退让——与完备性不同
这两个性质并不处在同等的地位上：
- 可靠性是强制性的。 一个证明系统哪怕只能证出一个假命题，就一文不值：一旦
⊢能推到一个不真的命题，它就能（借道这个不真的命题）推出任何东西，所以"⊢ φ"这句话对φ什么都说明不了。可靠性是一个证明系统配得上这个名字的最低要求——正是它让⊢有意义。 - Completeness只是锦上添花。 一个可靠但不完备的系统依然完全可用——它从不说谎，只是无法抵达每一个真命题。很多优秀的系统都是刻意做成可靠而不完备的（弱理论、可判定片段、大多数实用证明助手的自动化部分）。
这种不对称一句话概括：丢掉可靠性 → 变成垃圾；丢掉完备性 → 只是能力有限。 所以你永远不会拿可靠性去做交易；但你经常会拿完备性去换（换取可判定性、速度，或者一个更弱的基础）。
为什么它是你真正依赖的那个性质
可靠性正是让一份经过检查的证明值得信任的原因——这也是一个小型可信 proof kernel 存在的全部意义：它只能推导出为真的东西，所以一个通过类型检查的项确确实实就是一个证明。用 certificate 的语言来说，可靠性就是"验证者接受的凭证确实是有效的"。它的逆否命题是一件趁手的工具：⊭ φ ⟹ ⊬ φ——像 P → Q 这样一个非重言式是无法被证明的。