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

[[分类:推理理论]][[分类:以 Hilbert 命名]]{{DEFAULTSORT:hilbert xi4tong3}}
{{#seo:
|keywords=希尔伯特系统,希尔伯特风格,希尔伯特表示
|description=希尔伯特系统指一种推理系统，基于形式化公理、进行命题逻辑与谓词逻辑的推理。特征是在尽可能少的推理规则基础上，加入精简的公理、公理模式。其中推理规则一般只有分离规则。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2023-07-19
}}
{{InfoBox
|name=希尔伯特推理系统
|eng_name=Hilbert-style system
|aliases=希尔伯特证明系统,Hilbert-style deductive system,Hilbert-style proof system
}}
{{InfoBox
|name=希尔伯特表示
|eng_name=Hilbert representation
|aliases=希尔伯特系统,Hilbert system,希尔伯特演算,Hilbert calculus
}}
'''Hilbert 系统'''('''Hilbert system''')/'''Hilbert 表示'''('''Hilbert representation''')是[[:分类:命题逻辑|命题逻辑]]及[[:分类:谓词逻辑|谓词逻辑]]的[[形式化公理系统（逻辑）|形式化公理系统]]中的一种，属于 Hilbert 式系统（不允许进行假设）。其中每一步出现的都是在前提下的永真式。

== Hilbert 系统（命题逻辑） ==

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

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

可以将第三条公理替换成：
* <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>

== Hilbert 系统（谓词逻辑） ==

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

推理规则：
* mp 。

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

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

量词公理可替换为：
* 第三项替换为 <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的文章 - 知乎]