形式化方法已经有大量的应用，如计算机辅助证明、模型检查、系统规约化语言（如 TLA+），这些技术的基础都离不开数理逻辑。现代逻辑学已经发展得非常广泛：Propositional logic（命题逻辑），First-order logic（也称 Predicate logic），Second-order logic，Higher-order logic，Constructive logic（也称 Intuitionistic logic），Modal logic（模态逻辑），Temporal logic（时态逻辑是模态逻辑的一个分支），Free logic，Plural logic，Paraconsistent logic（次协调逻辑），Quantum logic（量子逻辑）。逻辑学与其它理论也有非常紧密的联系，如集合论、证明论、模型论、计算理论等。在计算机技术领域，学习一阶逻辑、时态逻辑等，可以帮助我们更好地运用形式化方法。

形式系统的一致性和完全性

背景：希尔伯特为了解决数学基础问题，希望将数学建立在可靠的逻辑系统之上。

一致性（consistent）

有些文献里面将一致性称作「协调性」。有三种一致性：

  • 古典一致性（）

    系统 中不存在公式 ，使得 和 都在该系统中 可证。

  • 语法一致性（）

    系统中不是任何公式都 可证 的，或者说至少有一个公式 是 不可证 的。如果系统中 每个 公式都是 可证 的（句句是真理），那么这个系统就没有什么用处了。

  • 语义一致性（）

    也称作可靠性（soundness），凡是 可证 的（或称作 valid，即 有效的）公式都真的。

古典一致性和语法一致性都在 句法 和 规则 范围内，弱于语义一致性。如果系统的语义一致性得到证明，那么古典一致性和语法一致性也是满足的。因此，一致性 通常指 语义一致性，也即 可靠性（soundness）。一致性 的证明比较简单，其主要思路是：所有公理（axioms）是真的，推理规则（rules）是保真的，通过对证明序列进行归纳，即可得证。

完全性

完全性也有三种：

  • 古典完全性（ 或者 ）

    系统 中任一个公式 ，要么 是可证的，要么 是可证的。

  • 语法完全性

    如果把系统中的任一不可证公式作为公理增加到已有的系统中，导致系统变得不一致，则称该系统是语法完全的（或绝对完备的）。

  • 语义完全性（）

    如果在一个形式系统的所有模型中都真的公式在该系统中都可以得到证明，则称该系统是语义完全的（相对完备的）。

语义完全性（completeness）是语义一致性的逆命题，我们一般讨论的 完全性 都指「语义完全性」。完全性 的证明比较复杂，Wiki 中有一些概括，证明过程需要理解演绎定理（Deduction Theorem）。证明思路为：

  1. 证明

    即如果 是 的语义后承，那么 是重言式（永真式）。

  2. 证明

    即证明重言式都存在一个证明序列。

  3. 证明

    将 当作前提，然后运用蕴含消除规则，最终即可得证 。

演绎定理

演绎定理 是重要的元定理。在命题逻辑中，可以如此表述：。如果 是空集，则 。

参考资料

https://en.m.wikipedia.org/wiki/Natural_deduction