高阶逻辑

在数学与逻辑中，高阶逻辑（缩写HOL）是谓词逻辑的一种形式，与一阶逻辑的主要区别在于增加了量词的作用元，命题变元和谓词变元也能作约束变元（受量词约束）且作谓词变元的主目，有时语义也更强。例如，可量化谓词的系统就是二阶逻辑。 高阶逻辑区别于一阶逻辑的其他方式是在构造中允许下层的类型论。高阶谓词是接受其他谓词作为参数的谓词。一般的，阶为 ${\displaystyle n}$ 的高阶谓词接受一个或多个 ${\displaystyle (n-1)}$ 阶的谓词作为参数，这里的 ${\displaystyle n>1}$。对高阶函数类似的评述也成立。

高阶逻辑更有表达力，但它们的性质，特别是有关模型论的，则不如一阶逻辑完善，使它们对很多应用不能表现良好。

“高阶逻辑”一般指高阶简单谓词逻辑，“简单”表示基础类型论是简单类型论。雷奥·屈斯克特和弗兰克·普伦普顿·拉姆齐提出的简单类型论是对阿尔弗雷德·诺思·怀特海和伯特兰·罗素的《数学原理》的简化。简单类型有时也指不考虑多态类型和依赖类型。^[1] 高阶逻辑的一个实例是构造演算。

量化范围

一阶逻辑只量化个体；二阶逻辑也量化集合；三阶逻辑可以量化集合的集合，以此类推。

高阶逻辑是一阶、二阶、三阶……n阶逻辑的结合，也就是说允许对任意嵌套的集合进行量化。

语义

高阶逻辑有两种可能的语义。

在标准语义或完整语义中，对高阶对象的量化包含其中所有可能的对象。例如，对个体集合的量化范围是个体集合的整个幂集。因此，在标准语义中，一旦指定了个体集合，就足以指定所有量词。高阶逻辑的标准语义也因此比一阶逻辑更有表达力，例如其允许对自然数与实数进行范畴公理化，这在一阶逻辑中是不可能的。但根据哥德尔的结论，高阶逻辑的标准语义不容许（递归的公理化的）可靠、完备的证明演算^[2]。高阶逻辑标准语义的模型论性质也比一阶逻辑复杂，例如二阶逻辑的勒文海姆数甚至大于一阶逻辑的可测基数（若存在这样的基数）。^[3]一阶逻辑的勒文海姆数则有ℵ₀个，是最小的无穷基数。

在Henkin语义中，每种高阶类型的解释都包含单独的域。所以，对个体集合的量化可能只涉及个体集合幂集的一个子集，配备此种语义的高阶逻辑等同于一阶多类逻辑，而非强于一阶逻辑。特别地，高阶逻辑的Henkin语义具有一阶逻辑的所有模型论性质，且从一阶逻辑继承了可靠、完备的证明系统。

性质

高阶逻辑包括阿隆佐·邱奇的简单类型论的分支^[4]和直觉类型论的各种形式。Gérard Huet已经证明，三阶逻辑的类型论中，合一是不可判定问题^[5][6][7][8]，也就是说不会有算法可以决定二阶（遑论高阶）的任意方程是否有解。

在同构意义下，幂集运算在二阶逻辑在可以定义。利用这一观察结果，亚科·欣蒂卡在1955年确定，二阶逻辑可以模拟高价逻辑，即对高阶逻辑的所有公式，都可在二阶逻辑中找到其等可满足公式。^[9]

“高阶逻辑”一词在某些情况下被认为是指经典高阶逻辑，但模态高阶逻辑也有研究。根据一些逻辑学家的说法，哥德尔本体论证明最好（在技术上）在这样的语境中研究。^[10]

参见

• 高阶文法
• 有类型lambda演算
• 直觉类型论

延伸阅读

• Alonzo Church: A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, Vol. 5, 1940, 56-68.
• Leon Henkin: Completeness in the theory of types. Journal of Symbolic Logic, Vol. 15, 1950, 81-91.
• Peter B. Andrews: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. 2nd edition, Academic Press 2002.
• J. Lambek, P. J. Scott: Introduction to Higher Order Categorical Logic. Cambridge University Press 1986.