命题逻辑是最简单, 最基本的逻辑形式系统, 它可以用于刻画简单的逻辑推理过程。将逻辑推理过程形式化, 使得我们可以借助计算机自动化地完成逻辑推导, 在命题逻辑中所有的命题都是可判定的, 即对于任意一个命题都存在相应的算法可以在有限的时间内判定命题本身的真假, 后面我们会看到在谓词逻辑中这样的结论是不成立的, 我们将基于此展开讨论哥德尔不完备性定理

建立并研究形式系统, 首先应确定形式系统中用到的符号, 即需要确定字母表 (或称符号表), 然后定义形式系统的演变规则 (形式系统的语法), 而后赋予其相应的语义(对于纯粹的形式系统语义是不必要的, 但我们研究形式系统往往就是为了解决实际问题, 因而都需要赋予形式系统相应的语义), 对于命题逻辑来说, 其语义便是命题的真假, 如果一个命题为真, 则我们约定其真值为 1, 否则为 0, 我们统一使用小写字母如 p, q 来表示命题

命题联结词

命题可以通过联结词构成新的命题, 命题联结词有五种, 分别为否定词, 合取词, 析取词, 蕴涵词, 等价词

1. 否定词. 顾名思义, 是对命题的否定, 对于命题 $p$, $\neg p$ 为命题 $p$ 的否定, 它们的真值关系是相反的, 即若命题 $p$ 的真值为 1, 则 $\neg p$ 的真值为 0;
2. 合取词. 合取词可以理解为"且", 对于命题 $p$ 与 $q$, 命题 $p \wedge q$ 称为命题 $p$ 和命题 $q$ 的合取命题, 当 $p$ 和 $q$ 至少有一个命题的真值为 0 时, 命题 $p \wedge q$ 的真值便为 0
3. 析取词. 析取词可以理解为"或", 对于命题 $p$ 与 $q$, 命题 $p \lor q$ 称为命题 $p$ 和命题 $q$ 的析取命题, 当 $p$ 和 $q$ 至少有一个命题的真值为 1 时, 命题 $p \lor q$ 的真值便为 1
4. 蕴涵词. 蕴涵词类似于"若..则..", 对于命题 $p$ 与 $q$, 命题 $p \rightarrow q$ 称为命题 $p$ 和命题 $q$ 的析取命题, 命题 $p \rightarrow q$ 为假当且仅当命题 $p$ 为真且命题 $q$ 为假, 在蕴涵词中, 命题 $p$ 被称作前件, 命题 $q$ 被称作后件, 当前件为假时, 无论后件是否为真, 命题 $p \rightarrow q$ 都为真
5. 等价词. 等价词可以理解为"当且仅当", 对于命题 $p$ 与 $q$, 命题 $p \leftrightarrow q$ 为真当且仅当命题 $p$ 和 $q$ 同为真或同为假

命题联结词之间存在着一定的关系, 其中某些联结词可以通过其他联结词组合得到, 例如命题 $p \rightarrow q$ 实际上与命题 $\neg p \lor q$ 具有完全相同的真值表, 即 $\rightarrow$ 可以使用 $\neg$ 和 $\lor$ 的组合来替代, 再例如 $p \wedge q$ 实际上与命题 $\neg (p \rightarrow (\neg q))$ 具有完全相同的真值表, 即 $\wedge$ 也可以用 $\neg$ 和 $\rightarrow$ 的组合来替代, 实际上 $\{\neg, \lor\}$ 构成了一个联结词完备集, 其它的联结词都可以使用完备集的联结词组合得到

命题逻辑的符号表和公式集

建立形式系统, 首先需要确定系统的符号表, 由于前面我们提到命题逻辑联结词之间存在一定的联系, 其它的命题联结词都可以通过 $\neg$ 和 $\rightarrow$ 来导出, 所以在我们建立的形式系统中只引入这两个逻辑联结词, 另外, 无论是基本命题, 如 $p$, $q$, 还是复合命题 (如 $p \rightarrow q$, $p \lor q$ 等) 我们都统一称之为 "命题变元", 记为 $x_1$, $x_2$, ... , $x_n$, ..., 至此, 命题逻辑形式系统的符号表便已经确定了, 它由命题联结词和命题变元符号构成:

1. 命题联结词 $\neg$, $\rightarrow$
2. 命题变元的可数集合 $x_1$, $x_2$, ... $x_n$, ...

在这个符号集合上, 我们可以按照下面的方式递归定义系统的 "公式":

1. 所有的命题变元 $x_1$, $x_2$, ... 都是公式
2. 若 $p$ 是公式, 则 $\neg p$ 是公式, 若 $p$, $q$ 是公式, 则 $p \rightarrow q$ 也是公式
3. 经过有限次地使用 1 和 2 得到的都是公式

在这个定义下, 我们可以继续考察"公式"的性质, 我们记命题变元的集合为 X, X = $\{x_1, x_2, ... x_n, ...\}$, 使用如上的 1, 2, 3 规则可以生成公式集合, 我们将这个集合记为 L, 可以看到 L 如下的分层性

1. $L_1 = (x_1, x_2, ..., x_n, ...)$
2. $L_2 = (\neg x_1, \neg x_2, ... , \neg x_n, ... , x_1 \rightarrow x_2, x_1 \rightarrow x_3, ...)$
3. $L_3 = (\neg x_1 \rightarrow x_2, x_1 \rightarrow \neg x_2, ..., \neg(\neg x_1), ...)$
4. ...

而 $L(X) = L_1 \cup L_2 \cup L_3 ... \cup L_n ...$, 对于 $L_n$ 其实际是由基本的命题变元应用 $n$ 次逻辑联结词派生出的公式, 不难发现, 各层公式之间的交都是空集, $\neg$ 和 $\rightarrow$ 是作为公式集合 $L$ 上的一元和二元运算, 从而 $L(X)$ 构成了 $\{\neg, \rightarrow\}$ 型代数, 我们将其称为 "命题代数"

命题逻辑的形式系统

基于上面所定义的公式集 $L(X)$, 我们可以构建命题逻辑的形式系统, 对于命题变元集 $X = \{x_1, x_2, ... , x_n, ...\}$, 我们将带有 "公理" 和 "证明" 的命题代数 $L$ 称为命题变元集上的命题演算:

1. "公理". 注意这里所说的公理是我们所构建的这套形式系统的概念, 截止目前, 我们仅仅在讨论形式系统的定义和演变规则, 不涉及语义, 我们定义如下 3 种形式的公式作为我们所构建的形式系统的 "公理"

   1. $p \rightarrow (q \rightarrow p)$
   2. $p \rightarrow (q \rightarrow r) \rightarrow (p \rightarrow q) \rightarrow (p \rightarrow r)$
   3. $(\neg p \rightarrow \neg q) \rightarrow (q \rightarrow p)$

   实际上, 1, 2, 3 中的 $p, q, r$ 可以是公式集 $L(X)$ 中的任意公式, 所以公理实际上有无数多条, 1, 2, 3 是描述了所有的公理的上层形式

2. "证明". 所谓 "证明" 在形式上是一个公式序列, 设 $\Gamma \subseteq L(X)$, $p \in L(X)$, 若存在 $L(X)$ 中公式的有限序列 $p_1, p_2, ... p_n$, 其中 $p_n = p$, 对于所有的 $k \in [1, n]$, 都有

   1. $p_k \in \Gamma$ 或
   2. $p_k$ 是公理 或
   3. 存在 $i, j < k$, 使得 $p_j = p_i \rightarrow p_k$

则我们称序列 $p_1$, $p_2$, ... $p_n$ 是对 $p$ 的一个证明, 此时 $p$ 在公式集 $\Gamma$ 中可证

我们这里对 "公理", "证明" 的定义是形式化的, 实际上为了便于理解, 我们可以代入自然语言中的公理和证明加以理解, 所谓公理即是我们首先就承认的结论, 不需要证明, 它是逻辑推导的起点, 而证明便是从已知的前提出发, 根据推导规则进行演变, 得到最终的结论, 在整个证明的过程中, 实际上便产生了一个从前提到中间结论到最终结论的序列, 我们将这个序列称为"证明", 对于命题演算来说, 公理是不需要证明的, 也并非一定需要指定为上面所述的 3 种, 不同的 "公理" 将导致形成不同的命题演算

如果公式 $p$ 在公式集 $\Gamma$ 中可证, 则我们记 $\Gamma \vdash p$, $p$ 称作 $\Gamma$ 的语法推论, 特别地, 如果 $\emptyset \vdash p$, 则我们称 $p$ 为命题演算 $L$ 的"定理", 这里的定理尽管也是形式系统中的定义, 但很自然地可以按数学中的定理来理解, 即它不需要有特定的假定前提 (不需要像 $\Gamma \vdash p$ 那样需要有假定集 $\Gamma$ (即"前提")), 在 $L$ 中是自然成立的

在一个证明中, 若有 $p_j = p_i \rightarrow p_k$, 其中 $i, j < k$, 则我们称 $p_k$ 是 $p_i$ 和 $p_j$ 使用假言推理 (MP) 得到的, 这里自然的, $p_i$ 可以理解为前提, $p_j = p_i \rightarrow p_k$ 指示了 $p_i$ 到 $p_k$ 的演变规则, 即当前提 $p_i$ 成立时, 便可以得到结论 $p_k$, 当然作为形式系统, 其本身只是纯粹的符号, 不含有特定的语义, 这里这样表述只是为了方便理解

基于如上的对 "公理", "证明", "定理" 的定义, 我们可以得到如下的结论: