希尔伯特系统

在数学物理学中，希尔伯特系统是一个不经常使用的术语，用于描述由C*代数描述的物理系统。在逻辑学，尤其是数理逻辑学中，希尔伯特系统，有时被称为希尔伯特微积分、希尔伯特式演绎系统或希尔伯特-阿克曼系统，是归于戈特洛布-弗雷格和大卫-希尔伯特的一种形式演绎系统。这些演绎系统最常被研究的是一阶逻辑，但对其他逻辑也有兴趣。希尔伯特系统的大多数变体在平衡逻辑公理和推理规则之间的权衡方面采取了一种特有的处理方式。希尔伯特系统的特点是选择了大量的逻辑公理方案和一小套推理规则。自然演绎系统则采取相反的做法，包括许多推理规则，但很少或没有公理方案。最常研究的希尔伯特系统要么只有一条推理规则--命题逻辑的模因，要么有两条推理规则--经过概括，也可以处理谓词逻辑--以及几个无限的公理方案。

用于命题模态逻辑的希尔伯特系统，有时被称为希尔伯特-刘易斯系统，通常用两个额外的规则进行公理化，即必要性规则和统一替换规则。希尔伯特系统的许多变体的一个特点是，在它们的任何推理规则中都不改变上下文，而自然演绎和顺序计算都包含一些改变上下文的规则。因此，如果人们只对同义反复的可推导性感兴趣，没有假设性的判断，那么就可以将希尔伯特系统形式化，使其推理规则只包含相当简单形式的判断。其他两个演绎系统也不能这样做：由于在它们的一些推理规则中上下文被改变了，它们不能被形式化，从而避免假设性判断--即使我们想用它们来证明同义反复的可推导性也不行。

在希尔伯特式的演绎系统中，形式化演绎是一个有限的公式序列，其中每个公式要么是公理，要么是通过推理规则从先前的公式中得到的。这些形式化演绎是为了反映自然语言的证明，尽管它们要详细得多。是一组公式，被视为假设。比如说{displaystyleGamma}是一组公式，被视为假设。可以是一组群论或集合论的公理。符号{displaystyleGamma}vdashphi}是指有一个推论，它是由一个人负责的。意味着有一个推论以希尔伯特式演绎系统的特点是使用众多的逻辑公理方案。公理方案是一个无限的公理集，通过将某种形式的所有公式替换成特定的模式而得到。逻辑公理集不仅包括从这个模式产生的那些公理，还包括这些公理之一的任何概括。一个公式的泛化是通过在该公式上添加零个或多个通用量词而得到的；例如

谓词逻辑有几种不同的公理化，因为对于任何逻辑来说，都有选择公理和规则的自由，这也是该逻辑的特征。我们在这里描述了一个有九个公理的希尔伯特系统，只有规则modusponens，我们称之为单规则公理化，它描述了经典的等价逻辑。