命题表达式
命题语言的字符集由和变量和命题运算符构成，由于 \(\land, \lor, \leftrightarrow\) 都能用 \(\lnot, \to\) 代替，故定义符号表：
其中 \(A_n\) 代表了可数个命题变量
命题逻辑的有限符号串定义为：
记 \(|s|\) 为 \(s\) 的长度，并写成 \(\langle s_1, s_2, \cdots, s_{|s|} \rangle\)，记 \(s * t\) 表示 \(s\) 与 \(t\) 的拼接
记 \(L \subseteq \Sigma ^ *\) 是一个准语言当且仅当 \(\forall A_n : \langle A_n \rangle \in L\) 且具有以下封闭性：
记 \(\mathcal L_0\) 是所有准语言的交，则可见，\(\mathcal L_0\) 自己也是一个准语言，并且除由封闭性定义的符号串外都不属于 \(\mathcal L_0\)
逻辑赋值
一个关于 \(\mathcal L_0\) 的真假赋值 \(\nu : A_n \mapsto \{ T, F \}\) 是一个命题变量到真值的映射，而显然其定义域可扩张到所有 \(\varphi \in \mathcal L_0\)
记 \(\varphi \in \mathcal L_0\) 是可满足的当且仅当存在 \(\nu\) 使得 \(\nu(\varphi) = T\)，同理对 \(\Gamma \subseteq \mathcal L_0\) 定义
记 \(\varphi \in \mathcal L_0\) 是重言式或恒真式当且仅当对每个 \(\nu\) 都有 \(\nu(\varphi) = T\)
记 \(\varphi \in \mathcal L_0\) 是谬论当且仅当对每个 \(\nu\) 都有 \(\nu(\varphi) = F\)
记 \(\varphi \in \mathcal L_0\) 是 \(\Gamma \subseteq \mathcal L_0\) 的逻辑结论，当且仅当对每个 \(\nu\) 都有 \(\nu(\Gamma) = \nu(\varphi)\)，记成 \(\Gamma \vDash \varphi\)
布尔代数可表示性
考虑 \(\varphi\) 中的变量 \(A_0, \cdots, A_{n - 1}\)，其对应了一个映射 \(f : \{ T, F \} ^ n \mapsto \{ T, F \}\)，称 \(\varphi\) 诱导出了 \(f\)
则对于每个 \(f : \{ T, F \} ^ n \mapsto \{ T, F \}\)，容易证得存在 \(\varphi\) 可以诱导出它
首先，构造 \(\varphi \land \psi := (\lnot(\varphi \to (\lnot \psi)))\)，\(\varphi \lor \psi := ((\lnot\varphi) \to \psi)\)
然后，记 \(\sigma \in \{ T, F \} ^ n\)，以下表达式即为所求：
令 \(\Sigma_1 := \{ (, ), \land, \lor, \lnot, \to, \leftrightarrow, A_n | n \in \mathbb N \}\)，同上定义 \(\Sigma_1 ^ *, \mathcal L_0 ^ *\)
证明系统
一个证明系统，除语言之外，还由逻辑公理与推理规则组成。
形式化的说，对于 \(r\) 属于推理规则集合 \(\mathcal R\)，有 \(r \subseteq \mathcal L ^ m * \mathcal L, \; m \geq 1\)
对于 \((A_1, \cdots, A_m, B) \in r\)，称 \(A_{1 \sim m}\) 为前提，\(B\) 为结论，写作：
从而，我们定义证明：
设 \(s = \langle \varphi_1, \varphi_2, \cdots, \varphi_n \rangle\)，则称 \(s\) 是一个来自 \(\Gamma \subseteq \mathcal L\) 的证明，当且仅当 \(\varphi_i\) 属于以下几种情况：
- \(\varphi_i \in \Gamma\)
- \(\varphi_i\) 是一条逻辑公理
- 存在 \(j_1, \cdots j_m\) 与推理规则 \(r\)，使得 \(\varphi_i = r(\varphi_{j_1}, \cdots, \varphi_{j_m})\)
而 \(\varphi\) 被称为是 \(\Gamma\) 的一个定理，当且仅当存在来自 \(\Gamma\) 的证明 \(s\) 使得 \(s_{|s|} = \varphi\)，写作 \(\Gamma \vdash \varphi\)
特别的，当 \(\Gamma = \varnothing\) 时，写作 \(\vdash \varphi\)
希尔伯特证明系统
我们先考虑没有 \(\lnot\) 的语言，我们定义以下公理与证明规则：
其中 \(MP\) 为肯定前件，\(A1\) 称为第一宽容律，\(A2\) 称为蕴含分配律
由以上的公理系统，我们可以证明以下结论：
自蕴含律：\(\vdash (\varphi \to \varphi)\)
\(s_1 = ((\varphi \to ((\psi \to \varphi) \to \varphi)) \to ((\varphi \to (\psi \to \varphi)) \to (\varphi \to \varphi)))\)，由 \(A2\)
\(s_2 = (\varphi \to ((\psi \to \varphi) \to \varphi))\)，由 \(A1\)
\(s_3 = ((\varphi \to (\psi \to \varphi)) \to (\varphi \to \varphi))\)，由 \(s_1, s_2\) 与 \(MP\)
\(s_4 = (\varphi \to (\psi \to \varphi))\)，由 \(A1\)
\(s_5 = (\varphi \to \varphi)\)，由 \(s_3, s_4\) 与 \(MP\)
第一传递律：\(\vdash ((\varphi \to \psi) \to ((\theta \to \varphi) \to (\theta \to \psi)))\)
\(s_1 = ((\varphi \to \psi) \to (\theta \to (\varphi \to \psi)))\)，由 \(A1\)
\(s_2 = ((\theta \to (\varphi \to \psi)) \to ((\theta \to \varphi) \to ((\theta \to \psi))))\)，由 \(A2\)
\(s_3 = (((\theta \to (\varphi \to \psi)) \to ((\theta \to \varphi) \to ((\theta \to \psi)))) \to ((\varphi \to \psi) \to ((\theta \to (\varphi \to \psi)) \to ((\theta \to \varphi) \to ((\theta \to \psi))))))\)，由 \(A1\)
\(s_4 = ((\varphi \to \psi) \to ((\theta \to (\varphi \to \psi)) \to ((\theta \to \varphi) \to ((\theta \to \psi)))))\)，由 \(s_2, s_3\) 与 \(MP\)
\(s_5 = (((\varphi \to \psi) \to ((\theta \to (\varphi \to \psi)) \to ((\theta \to \varphi) \to ((\theta \to \psi))))) \to (((\varphi \to \psi) \to (\theta \to (\varphi \to \psi))) \to ((\varphi \to \psi) \to ((\theta \to \varphi) \to ((\theta \to \psi))))))\)，由 \(A2\)
\(s_6 = (((\varphi \to \psi) \to (\theta \to (\varphi \to \psi))) \to ((\varphi \to \psi) \to ((\theta \to \varphi) \to ((\theta \to \psi)))))\)，由 \(s_4, s_5\) 与 \(MP\)
\(s_7 = ((\varphi \to \psi) \to ((\theta \to \varphi) \to ((\theta \to \psi))))\)，由 \(s_1, s_6\) 与 \(MP\)
容易发现，这样证明太麻烦了。为此，我们引入一些定理
导出引理
令 \(\Gamma \subseteq \mathcal L_0, \varphi \in \mathcal L_0, \psi \in \mathcal L_0\)，则有：
证明：记 \(\Gamma \vdash \varphi\) 证明为 \(s\)，\(\Gamma \vdash (\varphi \to \psi)\) 证明为 \(t\)，则 \(s * t * \langle \psi \rangle\) 即为 \(\Gamma \vdash \psi\) 的证明，最后一步使用 \(MP\)
演绎引理
令 \(\Gamma \subseteq \mathcal L_0, \varphi \in \mathcal L_0, \psi \in \mathcal L_0\)，则有：
证明：考虑 \(\Gamma \cup \{\varphi\} \vdash \psi\) 的证明 \(s\)，我们尝试归纳的证明对于所有 \(i\)，有 \(\Gamma \vdash (\varphi \to s_i)\)，从而得到 \(\Gamma \vdash (\varphi \to s_{|s|})\) 即 \(\Gamma \vdash (\varphi \to \psi)\)
对于 \(s_i\)，有三种可能：
若 \(s_i = \varphi\)，则自蕴含律保证了 \(\vdash (\varphi \to \varphi)\)
若 \(s_i \in \Gamma\) 或 \(s_i\) 是一条逻辑公理，则 \(\Gamma \vdash (\varphi \to s_i)\) 的证明即为序列 \(\langle s_i, (s_i \to (\varphi \to s_i)), (\varphi \to s_i) \rangle\)
否则，\(s_i\) 就由 \(s_j, s_k\) 与 \(MP\) 得到，其中 \(j, k < i\)，且 \(s_k = (s_j \to s_i)\)
由归纳假设，有 \(\Gamma \vdash (\varphi \to s_j)\) 由 \(\Gamma \vdash (\varphi \to (s_j \to s_i))\)，且由 \(A2\) 有 \(\Gamma \vdash ((\varphi \to (s_j \to s_i)) \to ((\varphi \to s_j) \to (\varphi \to s_i)))\)，连续应用两次导出引理即证
逆定理 \(\displaystyle\frac{\Gamma \vdash (\varphi \to \psi)}{\Gamma \cup \{\varphi\} \vdash \psi}\) 是容易证的，只需对 \(\Gamma \cup \{\varphi\} \vdash \varphi, \Gamma \cup \{\varphi\} \vdash (\varphi \to \psi)\) 应用导出引理即可
得到这两个强大的引理后，我们便可以继续证明一些结论
前提顺序无关律：\(\vdash (((\varphi \to \psi) \to \theta) \to (\varphi \to (\psi \to \theta)))\)
由演绎引理，只需证明 \(\{ ((\varphi \to \psi) \to \theta), \varphi, \psi \} \vdash \theta\)
由 \(A1\) 经过演绎引理，有 \(\{ \psi \} \vdash (\varphi \to \psi)\)，又有 \(\{ ((\varphi \to \psi) \to \theta), \varphi, \psi \} \vdash ((\varphi \to \psi) \to \theta)\) 由导出引理即证
第二传递律：\(\vdash ((\varphi \to \psi) \to ((\psi \to \theta) \to (\varphi \to \theta)))\)
由演绎引理，只需证明 \(\{ (\varphi \to \psi), (\psi \to \theta), \varphi \} \vdash \theta\)，这由导出引理是显然的
对于 \(\lnot\)，我们加入公理：第一逆否命题法则
显然，导出引理与演绎引理依然成立
第二与第三宽容律：\(\vdash (\varphi \to ((\lnot\varphi) \to \psi)),\ \vdash ((\lnot\varphi) \to (\varphi \to \psi))\)
应用演绎引理，两者都只需证明 \(\{ \varphi, (\lnot\varphi) \} \vdash \psi\) 即可
由 \(A1\) 经过演绎引理，有 \(\{ (\lnot\varphi) \} \vdash ((\lnot\psi) \to (\lnot\varphi))\)，由 \(A3\) 有 \(\vdash (((\lnot\psi) \to (\lnot\varphi)) \to (\varphi \to \psi))\)
故利用导出引理，有 \(\{ \varphi, (\lnot\varphi) \} \vdash (\varphi \to \psi)\)，故再利用导出引理得证
第一归谬律：\(\vdash (((\lnot\varphi) \to \varphi) \to \varphi)\)
由第三宽容律与 \(A2\) 加上导出引理，有 \(\vdash ((\lnot\varphi \to \varphi) \to (\lnot\varphi \to \lnot\psi))\)
由 \(A3\)，有 \(\vdash ((\lnot\varphi \to \lnot\psi) \to (\psi \to \varphi))\)，依第二传递律与导出引理可证 \(\vdash ((\lnot\varphi \to \varphi) \to (\psi \to \varphi))\)
再应用演绎引理可知 \(\{ (\lnot\varphi \to \varphi) \} \vdash (\psi \to \varphi)\)，取 \(\psi = (\lnot\varphi \to \varphi)\)，即 \(\{ (\lnot\varphi \to \varphi) \} \vdash \varphi\)，由演绎引理即证
第一否定之否定律：\(\vdash ((\lnot(\lnot\varphi)) \to \varphi)\)
由第三宽容律，\(\vdash ((\lnot(\lnot\varphi)) \to ((\lnot\varphi) \to \varphi))\)
再由第一归谬律与第二传递律加上导出引理即证
第二归谬律：\(\vdash ((\varphi \to (\lnot\varphi)) \to (\lnot\varphi))\)
由第一否定之否定律，\(\vdash ((\lnot(\lnot\varphi)) \to \varphi)\)
再由第二传递律与导出引理，\(\vdash ((\varphi \to (\lnot\varphi)) \to ((\lnot(\lnot\varphi)) \to (\lnot\varphi)))\)
由第一归谬律，\(\vdash (((\lnot(\lnot\varphi)) \to (\lnot\varphi)) \to (\lnot\varphi))\)，再由第二传递律与导出引理即证
第二否定之否定律：\(\vdash (\varphi \to (\lnot(\lnot\varphi)))\)
由第二宽容律，\(\vdash (\varphi \to ((\lnot\varphi) \to (\lnot(\lnot\varphi))))\)
由第二归谬律，\(\vdash (((\lnot\varphi) \to (\lnot(\lnot\varphi))) \to (\lnot(\lnot\varphi)))\)，再由第二传递律与导出引理即证
第二逆否命题法则：\(\vdash ((\varphi \to \psi) \to ((\lnot\psi) \to (\lnot\varphi)))\)
由第一否定之否定律与第二传递律加上导出引理，\(\vdash ((\varphi \to \psi) \to ((\lnot(\lnot\varphi)) \to \psi))\)
由第二否定之否定律与第一传递律加上导出引理，\(\vdash (((\lnot(\lnot\varphi)) \to \psi) \to ((\lnot(\lnot\varphi)) \to (\lnot(\lnot\psi))))\)
由 \(A3\)，\((((\lnot(\lnot\varphi)) \to (\lnot(\lnot\psi))) \to ((\lnot\psi) \to (\lnot\varphi)))\)
反复运用第二传递律与导出引理，即证得结论
完备性
一致性：令 \(\Gamma \subseteq \mathcal L_0\)，称 \(\Gamma\) 是一致的当且仅当不存在 \(\varphi\) 使得 \(\Gamma \vdash \varphi\) 且 \(\Gamma \vdash (\lnot\varphi)\)，否则称其为不一致的
由上可知，若 \(\Gamma\) 不一致，当且仅当对任意 \(\varphi\)，有 \(\Gamma \vdash \varphi\)
可靠性：设 \(\Gamma \subseteq \mathcal L_0\) 与 \(\varphi \in \mathcal L_0\)，如果 \(\Gamma \vdash \varphi\)，那么 \(\Gamma \vDash \varphi\)
考虑归纳，设 \(\Gamma \vdash \varphi\) 的证明 \(s\)，若 \(s_i \in \Gamma\) 或 \(s_i\) 是一条逻辑公理，那么无论怎样都有 \(\Gamma \vDash s_i\)，否则存在 \(s_j\) 与 \(s_k = (s_j \to s_i)\)，设真假赋值 \(\nu(\Gamma) = T\)，则 \(\nu(s_j) = \nu(s_j) \to \nu(s_i) = T\)，故 \(\nu(s_i) = T\)，得证
由可靠性定理与一致性得定义，即得 \(\Gamma \subseteq \mathcal L_0\) 如果是可满足的，那么一定是一致的
这带来了一个问题：如果 \(\Gamma\) 是一致的，那一定是可满足的吗？
我们即将证明这点，不过不妨先来看看这件事的推论
有效性：设 \(\Gamma \subseteq \mathcal L_0\)，则 \(\Gamma\) 如果是一致的，那么一定是可满足的
第一完备性：设 \(\Gamma \subseteq \mathcal L_0\)，则 \(\Gamma\) 是一致的当且仅当其是可满足的
冗余假设引理：设 \(\Gamma \subseteq \mathcal L_0\)，\(\varphi \in \mathcal L_0\)，若 \(\Gamma \cap \{ (\lnot\varphi) \} \vdash \varphi\)，那么 \(\Gamma \vdash \varphi\)
由演绎引理，\(\Gamma \vdash ((\lnot\varphi) \to \varphi)\)，又由第一归谬律，\(\vdash (((\lnot\varphi) \to \varphi) \to \varphi)\)，故依导出引理得到 \(\Gamma \vdash \varphi\)
第二完备性：设 \(\Gamma \subseteq \mathcal L_0\) 与 \(\varphi \in \mathcal L_0\)，那么 \(\Gamma \vDash \varphi\) 当且仅当 \(\Gamma \vdash \varphi\)
容易发现，\(\Gamma \cap \{ (\lnot\varphi) \}\) 不可能被满足，由第一完备性定理可知其不一致，故 \(\Gamma \cap \{ (\lnot\varphi) \} \vdash \varphi\)，由冗余假设引理即证
应用第二完备性定理，立即得到定理：
若 \(\varphi\) 是重言式，那么 \(\vdash \varphi\)
第一完备性的证明
todo