Hilbert 系统

希尔伯特推理系统
术语名称	希尔伯特推理系统
英语名称	Hilbert-style system
别名	希尔伯特证明系统, Hilbert-style deductive system, Hilbert-style proof system

希尔伯特表示
术语名称	希尔伯特表示
英语名称	Hilbert representation
别名	希尔伯特系统, Hilbert system, 希尔伯特演算, Hilbert calculus

命题逻辑及谓词逻辑的形式化公理系统有多种方案，尽管都基于推理规则和公理，在推理规则与公理的权衡上有所差异。 Hilbert 风格的推理系统，或称 Hilbert 推理系统(Hilbert-style system)，尽可能追求使用更少的推理规则，作为权衡，引入更多公理模式。

其中，作为命题逻辑和谓词逻辑的典型的 Hilbert 推理系统被称为 Hilbert 系统(Hilbert system)/Hilbert 表示(Hilbert representation)。

Hilbert 系统（命题逻辑）

使用形式语言 [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]

其他 Hilbert 风格系统（命题逻辑）的变体

可以将第三条公理替换成：

• [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]

Hilbert 系统（谓词逻辑）

使用形式语言 [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] 中可自由代入

推理规则：

• mp 。

其他 Hilbert 风格系统（命题逻辑）的变体

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

量词公理可替换为：

• 第三项替换为 [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的文章 - 知乎