行而上的博客

命题逻辑是最基本的逻辑系统。本文首先定义命题逻辑的字母表、语法、语义，然后给出永真式、矛盾式、可满足性、语义后承、语义等价的定义，然后证明一系列语义的性质，最后讨论命题逻辑符号的功能完全性。

一阶逻辑是形式化描述数学定理与证明的一套形式语言，原则上可以表达当今世界上的所有数学定理。本文定义一阶逻辑要满足的语法规则，定义如何为一阶逻辑语言赋予实际语义，并列举了一些由语法和语义的定义所引发的重要概念和事实。

上一节我们已经知道如何通过一阶逻辑语言形式化“数学命题”。现在我们想要形式化“数学证明”的概念。我们首先给出相继式演算的定义，说明如何用相继式演算书写形式化证明。然后我们验证相继式演算的可靠性，说明形式化证明一定是数学事实上可靠的。

本文证明基于一阶逻辑语言的相继式演算的完备性。首先定义一致性，证明完备性等价于一致性能推出可满足性。接下来，引入term interpretation，证明一致的公式集在满足contain witness与negation complete的前提下是可满足的(Henkin's Theorem)。然后我们移除这两条限制，证明符号集可数时完备性成立。最后证明符号集不可数时完备性也成立，从而完成整个完备性的证明。

一阶逻辑的表达能力

在偏序集$P$中，如果$P$的每一条链都有一个$P$中元素作为上界，那么$P$中存在极大元。Zorn's Lemma是集合论的ZF公理体系中选择公理的等价表述。

通过一阶逻辑语言我们能够形式化数学定理，现在我们想要形式化“证明”的概念。对证明的形式化同样是对现实中的数学证明的抽象，并且我们需要验证我们定义的形式上的证明概念的确等价于语义上的证明概念，这一性质称为完备性。哥德尔完备性定理指出一阶逻辑的确是具有完备性的。