逻辑中的可靠性定理怎样连接证明与模型

可靠性定理讨论形式逻辑中两种判断之间的关系：一种是依据推理规则写出证明，另一种是考察命题在模型中的真假。一个推理系统具有可靠性，意味着它的证明规则不会把语义上不成立的结论证明出来。

弱可靠性通常表示：如果某个命题在不依赖额外前提的情况下可被证明，那么它在所有相关模型中都成立。强可靠性则允许加入任意前提集合；只要能由这些前提推出一个命题，这个命题就应在所有满足前提的模型中成立。空前提的情形可以看作后者的特殊情况。

这里的“可靠性”也要与日常所说的可靠信息分开。对于一个具体论证，人们常把推理有效且前提真实称为健全或可靠；形式系统的可靠性则检验规则与语义之间是否匹配。即使推理规则没有问题，也不能仅凭形式证明保证现实世界中提供的前提确实为真。

资料依据：维基百科《可靠性定理》及该页贡献者（修订记录）。本文重组论述并改写表达；依Creative Commons Attribution-Share Alike 4.0提供。