查看“︁Hilbert 系统”︁的源代码

[[分类:推理理论]]{{DEFAULTSORT:hilbert xi4tong3}}
{{#seo:
|keywords=希尔伯特系统,希尔伯特风格,希尔伯特表示
|description=希尔伯特系统指一种推理系统，基于形式化公理、进行命题逻辑与谓词逻辑的推理。特征是在尽可能少的推理规则基础上，加入精简的公理、公理模式。其中推理规则一般只有分离规则。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2023-07-19
}}
[[:分类:命题逻辑|命题逻辑]]及[[:分类:谓词逻辑|谓词逻辑]]的[[形式化公理系统（逻辑）|形式化公理系统]]中，有多种方案，差别基本在于推理规则与公理的权衡。
<ins>希尔伯特</ins>风格的公理系统尽可能追求使用更少的推理规则，因此引入更多公理模式。

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

== <ins>希尔伯特</ins>系统（命题逻辑） ==

使用形式语言 <math>\mathcal{L}_{\lnot,\rightarrow}</math> 。

公理：
* <math>\phi \rightarrow (\psi \rightarrow \phi)</math>
* <math>(\phi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \chi))</math>
* <math>(\lnot\phi \rightarrow \lnot\psi) \rightarrow (\psi \rightarrow \phi)</math>

推理规则：
* [[分离规则|mp]]: <math>\phi, \phi \rightarrow \psi \vdash \psi</math>

== 其他<ins>希尔伯特</ins>风格系统（命题逻辑）的变体 ==

第三条也可以换成：
* <math>(\lnot\phi \rightarrow \psi) \rightarrow ((\lnot\phi \rightarrow \lnot\psi) \rightarrow \phi)</math>
* <math>(\lnot\phi \rightarrow \lnot\psi) \rightarrow ((\lnot\phi \rightarrow \psi) \rightarrow \phi)</math>
* <math>((\phi \rightarrow \psi) \rightarrow \phi) \rightarrow \phi</math>、<math>\lnot\phi \rightarrow (\phi \rightarrow \psi)</math>、<math>(\phi \rightarrow \lnot\phi) \rightarrow \lnot\phi</math>
* <math>\lnot\phi \rightarrow (\phi \rightarrow \psi)</math>、<math>(\lnot\phi \rightarrow \phi) \rightarrow \phi</math>

== <ins>希尔伯特</ins>系统（谓词逻辑） ==

使用形式语言 <math>\mathcal{L}_{\lnot,\rightarrow,\forall}</math> 。

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

* <math>\forall x (\phi \rightarrow \psi) \rightarrow (\forall x \phi \rightarrow \forall x \psi)</math>
* <math>\forall x \phi \rightarrow \phi(t/x)</math> ， <math>t</math> 对 <math>x</math> 在 <math>\phi</math> 中可自由代入
* <math>\phi \rightarrow \forall x \phi</math> ， <math>x</math> 不在 <math>\phi</math> 中自由出现

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

* <math>t=t</math>
* <math>s=t \rightarrow (\phi(s/x) \rightarrow \phi(t/x))</math> ， <math>s,t</math> 对 <math>x</math> 在 <math>\phi</math> 中可自由代入

== 其他<ins>希尔伯特</ins>风格系统（命题逻辑）的变体 ==

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

量词公理：
* <math>\forall x (\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \forall x \psi)</math> ， <math>x</math> 不在 <math>\phi</math> 中自由出现：这一条可由第1、3条量词公理得出，且结合 <math>\forall x (\phi \rightarrow \phi)</math> 可推出第三条量词公理。
量词推演规则可能使用：
* 概括规则： <math>\phi</math> 得到 <math>\forall x \phi</math>
* 后件概括： <math>\phi \rightarrow \psi</math> 得到 <math>\phi \rightarrow \forall x \psi</math> ， <math>x</math> 不在 <math>\phi</math> 中自由出现

等词公理第二项可替换为：
* <math>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>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>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>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>\forall x \phi = \lnot \exists x \lnot \phi</math> 。此时公理为：
* <math>\forall x (\phi \rightarrow \psi) \rightarrow (\exists x \phi \rightarrow \exists x \psi)</math>
* <math>\phi(t/x) \rightarrow \exists x \phi</math> ， <math>t</math> 对 <math>x</math> 在 <math>\phi</math> 中可自由代入
* <math>\exists x \phi \rightarrow \phi</math> ， <math>x</math> 不在 <math>\phi</math> 中自由出现

== 参考资料 ==
[https://zhuanlan.zhihu.com/p/34918363 证明论学习笔记2：希尔伯特系统 - Arjuna的文章 - 知乎]