命题逻辑的公理系统

重言式定理

同一律

\phi\leftrightarrow\phi

排中律

\phi\vee\neg\phi

矛盾律

\neg(\phi\wedge\neg\phi)

分离律

\phi\wedge(\phi\rightarrow\psi)\rightarrow\psi

双重否定律

\neg\neg\phi\rightarrow\phi

幂等律

(\phi\vee\phi)\leftrightarrow\phi

(\phi\wedge\phi)\rightarrow\phi

交换律

(\phi\wedge\psi)\rightarrow(\psi\wedge\phi)

(\phi\vee\psi)\rightarrow(\psi\vee\phi)

德摩根律

\neg(\phi\wedge\psi)\rightarrow(\neg\psi\vee\neg\phi)

\neg(\phi\vee\psi)\rightarrow(\neg\psi\wedge\neg\phi)

结合律

\phi\wedge(\psi\wedge\theta)\leftrightarrow(\phi\wedge\psi)\wedge\theta

\phi\vee(\psi\vee\theta)\leftrightarrow(\phi\vee\psi)\vee\theta

分配律

\phi\wedge(\psi\vee\theta)\leftrightarrow(\phi\wedge\psi)\vee(\phi\wedge\theta)

\phi\vee(\psi\wedge\theta)\leftrightarrow(\phi\vee\psi)\wedge(\phi\vee\theta)

公理系统

命题演算三组公理：

(P_1)\ \ \phi\rightarrow(\psi\rightarrow\phi)

(P_2)\ \ (\phi\rightarrow\psi\rightarrow\theta)\rightarrow(\phi\rightarrow\psi)\rightarrow(\phi\rightarrow\theta)

(P_3)\ \ (\neg\phi\rightarrow\psi)\rightarrow(\neg\phi\rightarrow\neg\psi)\rightarrow\phi

设定一个初始推理规则：

分离规则（MP） 如果有 \phi 和 \phi\rightarrow\psi ，那么有 \psi 。

以上三条公理和一条推理规则是这个演算系统的全部初始设定。从这些初始设定出发演绎出系统的内定理，需要给出「 形式证明」 的严格定义。

形式证明的定义

（证明）. \phi_1,\cdot\cdot\cdot,\phi_n 是一个有限公式序列，如果每个公式 \phi_i(1,\cdot\cdot\cdot,n) 满足以下条件之一，则称这个公式序列为一个序列，简称证明。

（1） \phi_i 是公理。

（2） \phi_i 是由序列中较前的两个公式应用分离规则得到的（即存在 j,k\leqslant i 使得 \phi_k=\phi_j\rightarrow\phi_i ）。

证明的直观意义就是从公理出发，通过分离规则得到一个又一个公式。

定义：（ \phi 的证明）. 如果一个证明的最后一项是 \phi ，则称这个证明的序列为 \phi 的证明。

定义：（内定理）. 如果 \phi 有一个证明，则称 \phi 是一个内定理，记作 \vdash\phi 。

结论：

（1）每条公理都是内定理。

（2）如果 \phi_1,\cdot\cdot\cdot,\phi_n 是一个证明，则任给 1\leqslant k\leqslant n,\phi_1,\cdot\cdot\cdot,\phi_k 也是一个证明，进而 \phi_k 也是一个内定理。

演绎规则

（演绎）. \Gamma 是公式集， \phi_1,\cdot\cdot\cdot,\phi_n 是有穷公式序列。如果每个 \phi_i(1,\cdot\cdot\cdot,n) 满足以下条件之一，则称这个公式序列是以 \Gamma 为假设的一个演绎。

（1） \phi_i 是公理。

（2） \phi_i 是 \Gamma 中的公式，即 \phi_i\in\Gamma 。

（3） \phi_i 是由序列中较前的两个公式应用分离规则得到的（即存在 j,k\leqslant i 使得 \phi_k=\phi_j\rightarrow\phi_i ）。

定义：（从 \Gamma 到 \phi 的演绎）. 如果以 \Gamma 为假设的演绎的最后一项是 \phi ，则称这个演绎是从 \Gamma 到 \phi 的一个演绎。

如果 \Gamma=\{\phi\} ，则可将 \Gamma\vdash\psi 简记为 \phi\vdash\psi 。
如果 \phi\vdash\psi 且 \psi\vdash\phi ，记为 \phi\vdash\dashv\psi 。
如果存在从 \Gamma 到 \phi 的演绎，则称 \Gamma 推出 \phi ，或 \phi 是 \Gamma 的推论，记为 \Gamma\vdash\phi 。
已知 \Gamma 和 \Sigma 都是公式集，如果任给 \phi\in\Sigma ，都有 \Gamma\vdash\phi ，则记为 \Gamma\vdash\Sigma 。

演绎规则：如果有 \Gamma\vdash\Sigma 且 \Sigma\vdash\Gamma ，则可得 \Gamma\vdash\psi 。所以，如果已经证明了 \{\psi_1,\psi_2\cdot\cdot\cdot,\psi_k\}\vdash\psi ，而再以 \Gamma 为假设的演绎中出现了 \phi_1,\phi_2,\cdot\cdot\cdot,\psi_k ，则可以直接得出 \psi 。这意味着一个已经被证明的演绎 \{\psi_1,\psi_2\cdot\cdot\cdot,\psi_k\}\vdash\psi 可以被看作一个演绎规则：从 \psi_1,\psi_2\cdot\cdot\cdot,\psi_k 可得到 \psi 。

应用已证明的演绎规则，可以简化证明。

设 \phi,\psi,\theta,\xi 是公式。则如下演绎规则成立：

（1）双重否定引入

\phi\vdash\neg\neg\phi

双重否定消去

\neg\neg\phi\vdash\phi

（2）蕴含引入或后件引入

\phi\vdash\psi\rightarrow\phi

蕴含消去或分离规则

\{\phi,\phi\rightarrow\psi\}\vdash\psi

（3）合取引入

\{\phi,\psi\}\vdash\phi\wedge\psi

合取消去

\phi\wedge\psi\vdash\phi

（4）析取引入

\phi\vdash\phi\vee\psi

析取消去

\{\phi\vee\psi,\phi\rightarrow\theta,\psi\rightarrow\theta\}\vdash\theta

（5）等值引入

\{\phi\rightarrow\psi,\psi\rightarrow\phi\}\vdash\phi\leftrightarrow\psi

等值消去

\phi\leftrightarrow\psi\vdash\phi\rightarrow\psi

（6）反证法

\{\neg\phi\rightarrow\psi,\neg\phi\rightarrow\neg\psi\}\vdash\phi

归谬法

\{\phi\rightarrow\psi,\phi\rightarrow\neg\psi\}\vdash\neg\phi

（7）假言三段论

\{\phi\rightarrow\psi,\psi\rightarrow\theta\}\vdash\phi\rightarrow\theta

析取三段论

\{\phi\vee\psi,\neg\phi\}\vdash\psi

（8）前件强化

\phi\rightarrow\theta\vdash\phi\wedge\psi\rightarrow\theta

后件强化

\{\phi\rightarrow\psi,\phi\rightarrow\theta\}\vdash\phi\rightarrow\psi\wedge\theta

（9）前件弱化

\{\phi\rightarrow\theta,\psi\rightarrow\theta\}\vdash\phi\vee\psi\rightarrow\theta

后件弱化

\phi\rightarrow\theta\vdash\phi\rightarrow\psi\vee\theta

（10）建设性二难推理

\{\phi\rightarrow\theta,\psi\rightarrow\xi,\phi\vee\psi\}\vdash\theta\vee\xi

破坏性二难推理

\{\phi\rightarrow\theta,\psi\rightarrow\xi,\neg\theta\vee\neg\xi\}\vdash\neg\phi\vee\neg\psi

（11）幂等律

\phi\wedge\phi\vdash\dashv\phi

\phi\vee\phi\vdash\dashv\phi

（12）交换律

\phi\wedge\psi\vdash\dashv\psi\wedge\phi

\phi\vee\psi\vdash\dashv\psi\vee\phi

（13）德摩根律

\neg(\phi\wedge\psi)\vdash\dashv\neg\phi\wedge\neg\psi

\neg(\phi\vee\psi)\vdash\dashv\neg\phi\vee\neg\psi

（14）结合律

\phi\wedge(\psi\wedge\theta)\vdash\dashv(\phi\wedge\psi)\wedge\theta

\phi\vee(\psi\vee\theta)\vdash\dashv(\phi\vee\psi)\vee\theta

（15）分配律

\phi\wedge(\psi\vee\theta)\vdash\dashv(\phi\wedge\psi)\vee(\phi\wedge\theta)

\phi\vee(\psi\wedge\theta)\vdash\dashv(\phi\vee\psi)\wedge(\phi\vee\theta)

（16）吸收律

\phi\rightarrow\psi\vdash\dashv\phi\rightarrow\phi\wedge\psi

输出律

\phi\rightarrow\psi\rightarrow\theta\vdash\dashv\phi\wedge\psi\rightarrow\theta

（17）假言易位

\phi\rightarrow\psi\vdash\dashv\neg\psi\rightarrow\neg\phi

\neg\phi\rightarrow\psi\vdash\dashv\neg\psi\rightarrow\phi

\phi\rightarrow\neg\psi\vdash\dashv\psi\rightarrow\neg\phi

\neg\phi\rightarrow\neg\psi\vdash\dashv\psi\rightarrow\phi

（18）等值否定交换

\phi\leftrightarrow\psi\vdash\dashv\neg\phi\leftrightarrow\neg\psi

\neg\phi\leftrightarrow\psi\vdash\dashv\phi\leftrightarrow\neg\psi

\phi\leftrightarrow\neg\psi\vdash\dashv\neg\phi\leftrightarrow\psi

\neg\phi\leftrightarrow\neg\psi\vdash\dashv\phi\leftrightarrow\psi

演绎的引入，得出了一些演绎规则，这些演绎规则能够进一步简化证明。但如果想证明内定理，则演绎规则中的假设必须是之前已经得到的，在内定理的证明过程中不能应用假设。

因此还需要考虑一些能够消去假设的原则，应用这些原则，可以从有假设的演绎得到内定理。其中最重要的就是演绎定理。

演绎定理

定义：（演绎定理）. 如果 \Gamma\cup\{\phi\}\vdash\psi ，则 \Gamma\vdash\phi\rightarrow\psi 。

定义：（演绎规则的逆）. 如果 \Gamma\vdash\phi\rightarrow\psi ，则 \Gamma\cup\{\phi\}\vdash\psi 。

演绎定理及其逆定理揭示了内定理和有前提（假设）的演绎之间的关系，能够帮助理解系统内定理和推理之间的关联。
当 \Gamma=\phi 时，作为演绎定理和演绎定理你定理的特例，可以得到： \phi\vdash\psi 当且仅当 \vdash\phi\rightarrow\psi 。

演绎定理还可以得到反证法和归谬法的其他形式：

引理：（反证法的第二形式）. 如果 \Gamma\cup\{\neg\phi\}\vdash\psi 且 \Gamma\cup\{\neg\phi\}\vdash\neg\psi ，则 \Gamma\vdash\phi 。

引理：（归谬法的第二形式）. 如果 \Gamma\cup\{\phi\}\vdash\psi 且 \Gamma\cup\{\phi\}\vdash\neg\psi ，则 \Gamma\vdash\neg\phi 。

引理：（反证法的第三形式）. 如果 \Gamma\cup\{\psi\}\vdash\phi 且 \Gamma\cup\{\neg\psi\}\vdash\phi ，则 \Gamma\vdash\phi 。

反证法、归谬法的几种形式也可以用于消去假设。

这个命题逻辑的公理系统是否是命题逻辑的形式化需要从两个方面考虑这一问题：一是可靠性，二是完全性。

可靠性

定理：（可靠性）. 如果 \vdash\phi ，那么 \models\phi 。即命题演算的所有内定理都是重言式。

定理：（广义可靠性）. 如果 \Gamma\vdash\phi ，则 \Gamma\models\phi 。

完全性

定理：（完全性）. 如果 \models\phi ，那么 \vdash\phi 。即命题逻辑语言下的所有重言式都是命题演算的内定理。

定理：（广义完全性）. 如果 \Gamma\models\phi ，则 \Gamma\vdash\phi 。

最早的完全性证明是由哥德尔给出的，而斤亨金的证明方法为人民所普遍采用。亨金最初用于证明一阶演算的完全性。也可以用于命题逻辑完全性证明。亨金证明是利用极大一致集及其性质证明的。

完全性定理亨金版本描述：设 \phi 是任意命题逻辑公式，若 \phi 不是内定理，则存在赋值 v ，使得 v(\phi)=0 。

紧致性

公式集 \Gamma 是可满足的当且仅当 \Gamma 的每个有穷子集都是可满足的。

紧致性定理有很多重要的应用，在「一阶逻辑」中将会有充分的体现。

可判定性

如果一个算法告诉我们一个公式 \phi 是否是一个逻辑的内定理，则称这个逻辑是可判定的。对于命题逻辑而言，应用真值表就可以判定 \phi 是否重言式。因此，命题逻辑是可判定的。

一阶逻辑不具有可判定性，这是命题逻辑和一阶逻辑的重要区别之一。

此文是命题逻辑的一个公理系统，事实上命题逻辑还有自然演绎系统（自然推理系统）。自然演绎系统最初是由德国数学家 Gentzen 引进的。公理系统和自然演绎系统各有特点。