Hilbert 系统

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

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

Hilbert 系统(Hilbert system)/Hilbert 表示(Hilbert representation)是命题逻辑及谓词逻辑的形式化公理系统中的一种，属于 Hilbert 式系统（不允许进行假设）。其中每一步出现的都是在前提下的永真式。

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]

推理规则：

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

[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] 中自由出现

证明论
形式化公理系统（形式化、公理化）
推理系统	Hilbert 风格/公理系统：Hilbert 表示
	Gentzen 风格-自然演绎系统： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎
	Gentzen 风格-相继式演算： Gentzen 式相继式演算
证明、演绎	演绎、可演绎、证明、可证明
命题、定理	公理/公理模式、定理、元定理、变形规则
推理规则性质	保存真实性、保存重言性
公理系统性质	可靠性、完备性/完全性、一致性、独立性