高阶逻辑

高阶逻辑
image
高阶逻辑（缩写HOL），亦称“广义谓词逻辑”或“高阶谓词逻辑”，是一阶逻辑的推广系统，谓词逻辑的重要组成部分。在一阶逻辑中，量词只能用于个体变元，而高阶逻辑取消这一限制，允许量词也可用于命题变元和谓词变元。这样构造起来的谓词逻辑允许对任意嵌套的集合进行量化，包括一阶、二阶、三阶……n阶逻辑的结合。公理化的高阶逻辑系统或高阶逻辑的自然推理系统又称为广义谓词演算或高阶谓词演算。

简介

高阶逻辑在数学中有别于一阶逻辑，主要体现在变量类型出现在量化中。一阶逻辑中禁止量化谓词，而高阶逻辑则允许。例如，二阶逻辑也量化集合，三阶逻辑可以量化集合的集合，以此类推。高阶逻辑的构造中还允许下层的类型论，其中高阶谓词是接受其他谓词作为参数的谓词。一般的，阶为n的高阶谓词接受一个或多个（n − 1）阶的谓词作为参数，这里的n > 1。

性质

高阶逻辑更加富有表达力，但是它们的性质，特别是有关模型论的，使它们对很多应用不能表现良好。哥德尔的结论指出，经典高阶逻辑不容许(递归的公理化的)可靠的和完备的证明演算；这个缺陷可以通过使用Henkin模型来修补。高阶逻辑的标准语义比一阶逻辑更有表达力，例如其允许对自然数与实数进行范畴公理化，这在一阶逻辑中是不可能的。然而，高阶逻辑的标准语义的模型论性质也比一阶逻辑复杂。高阶逻辑包括阿隆佐·邱奇的简单类型论的分支和直觉类型论的各种形式。高阶逻辑的一个实例是构造演算。