Hilbert 系统

命题逻辑及谓词逻辑的形式化公理系统中，有多种方案，差别基本在于推理规则与公理的权衡。 希尔伯特风格的公理系统尽可能追求使用更少的推理规则，因此引入更多公理模式。

其中一类典型的系统被称为希尔伯特系统(the Hilbert system)/希尔伯特表示(the Hilbert representation)/希尔伯特推理系统(Hilbert-style system)，如下。

希尔伯特系统（命题逻辑）

使用形式语言 [math]\displaystyle{ \mathcal{L}_{\lnot,\rightarrow} }[/math] 。

公理：

• [math]\displaystyle{ \phi \rightarrow (\psi \rightarrow \phi) }[/math]
• [math]\displaystyle{ (\phi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \chi)) }[/math]
• [math]\displaystyle{ (\lnot\phi \rightarrow \lnot\psi) \rightarrow (\psi \rightarrow \phi) }[/math]

推理规则：

• mp: [math]\displaystyle{ \phi, \phi \rightarrow \psi \vdash \psi }[/math]

其他希尔伯特风格系统（命题逻辑）的变体

第三条也可以换成：

• [math]\displaystyle{ (\lnot\phi \rightarrow \psi) \rightarrow ((\lnot\phi \rightarrow \lnot\psi) \rightarrow \phi) }[/math]
• [math]\displaystyle{ (\lnot\phi \rightarrow \lnot\psi) \rightarrow ((\lnot\phi \rightarrow \psi) \rightarrow \phi) }[/math]
• [math]\displaystyle{ ((\phi \rightarrow \psi) \rightarrow \phi) \rightarrow \phi }[/math]、[math]\displaystyle{ \lnot\phi \rightarrow (\phi \rightarrow \psi) }[/math]、[math]\displaystyle{ (\phi \rightarrow \lnot\phi) \rightarrow \lnot\phi }[/math]
• [math]\displaystyle{ \lnot\phi \rightarrow (\phi \rightarrow \psi) }[/math]、[math]\displaystyle{ (\lnot\phi \rightarrow \phi) \rightarrow \phi }[/math]

希尔伯特系统（谓词逻辑）

使用形式语言 [math]\displaystyle{ \mathcal{L}_{\lnot,\rightarrow,\forall} }[/math] 。

在命题逻辑公理上增加以下量词公理：

• [math]\displaystyle{ \forall x (\phi \rightarrow \psi) \rightarrow (\forall x \phi \rightarrow \forall x \psi) }[/math]
• [math]\displaystyle{ \forall x \phi \rightarrow \phi(t/x) }[/math] ， [math]\displaystyle{ t }[/math] 对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中可自由代入
• [math]\displaystyle{ \phi \rightarrow \forall x \phi }[/math] ， [math]\displaystyle{ x }[/math] 不在 [math]\displaystyle{ \phi }[/math] 中自由出现

涉及等词时还有以下等词公理。

• [math]\displaystyle{ t=t }[/math]
• [math]\displaystyle{ s=t \rightarrow (\phi(s/x) \rightarrow \phi(t/x)) }[/math] ， [math]\displaystyle{ s,t }[/math] 对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中可自由代入

其他希尔伯特风格系统（命题逻辑）的变体

命题公理和原来同样可进行替换。

量词公理：

• [math]\displaystyle{ \forall x (\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \forall x \psi) }[/math] ， [math]\displaystyle{ x }[/math] 不在 [math]\displaystyle{ \phi }[/math] 中自由出现：这一条可由第1、3条量词公理得出，且结合 [math]\displaystyle{ \forall x (\phi \rightarrow \phi) }[/math] 可推出第三条量词公理。

量词推演规则可能使用：

• 概括规则： [math]\displaystyle{ \phi }[/math] 得到 [math]\displaystyle{ \forall x \phi }[/math]
• 后件概括： [math]\displaystyle{ \phi \rightarrow \psi }[/math] 得到 [math]\displaystyle{ \phi \rightarrow \forall x \psi }[/math] ， [math]\displaystyle{ x }[/math] 不在 [math]\displaystyle{ \phi }[/math] 中自由出现

等词公理第二项可替换为：

• [math]\displaystyle{ s_1=t_1 \rightarrow ( \dots \rightarrow ( s_n = t_n \rightarrow f(s_1, \dots, s_n) = f(t_1, \dots, t_n) \dots) }[/math]，[math]\displaystyle{ s_1=t_1 \rightarrow ( \dots \rightarrow ( s_n = t_n \rightarrow (P(s_1, \dots, s_n) \rightarrow P(t_1, \dots, t_n)) \dots) }[/math]
• [math]\displaystyle{ s=s' \rightarrow ( f(t_1, \dots, t_{k-1}, s, t_{k+1}, \dots, t_n) = f(t_1, \dots, t_{k-1}, s', t_{k+1}, \dots, t_n)) }[/math]，[math]\displaystyle{ s=s' \rightarrow (P(t_1, \dots, t_{k-1}, s, t_{k+1}, \dots, t_n) \rightarrow P(t_1, \dots, t_{k-1}, s', t_{k+1}, \dots, t_n)) }[/math]

可以用存在量词作为初始符号，此时定义 [math]\displaystyle{ \forall x \phi = \lnot \exists x \lnot \phi }[/math] 。此时公理为：

• [math]\displaystyle{ \forall x (\phi \rightarrow \psi) \rightarrow (\exists x \phi \rightarrow \exists x \psi) }[/math]
• [math]\displaystyle{ \phi(t/x) \rightarrow \exists x \phi }[/math] ， [math]\displaystyle{ t }[/math] 对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中可自由代入
• [math]\displaystyle{ \exists x \phi \rightarrow \phi }[/math] ， [math]\displaystyle{ x }[/math] 不在 [math]\displaystyle{ \phi }[/math] 中自由出现

参考资料

证明论学习笔记2：希尔伯特系统 - Arjuna的文章 - 知乎