高阶逻辑

在数学与逻辑中，高阶逻辑（缩写HOL）是谓词逻辑的一种形式，与一阶逻辑的主要区别在于增加了量词的作用元，命题变元和谓词变元也能作约束变元（受量词约束）且作谓词变元的主目，有时语义也更强。例如，可量化谓词的系统就是二阶逻辑。 高阶逻辑区别于一阶逻辑的其他方式是在构造中允许下层的类型论。高阶谓词是接受其他谓词作为参数的谓词。一般的，阶为n的高阶谓词接受一个或多个（n − 1）阶的谓词作为参数，这里的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.

外部链接

1. Jacobs, 1999, chapter 5
2. Shapiro 1991, p. 87.
3. Menachem Magidor and Jouko Väänänen. "On Löwenheim-Skolem-Tarski numbers for extensions of first order logic （页面存档备份，存于互联网档案馆）", Report No. 15 (2009/2010) of the Mittag-Leffler Institute.
4. Alonzo Church, A formulation of the simple theory of types （页面存档备份，存于互联网档案馆）, The Journal of Symbolic Logic 5(2):56–68 (1940)
5. Huet, Gérard P. The Undecidability of Unification in Third Order Logic. Information and Control. 1973, 22 (3): 257–267. doi:10.1016/s0019-9958(73)90301-x. 
6. Huet, Gérard. Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (学位论文). Universite de Paris VII. Sep 1976 [2023-10-25]. （原始内容于2023-06-13） （French）.  引文格式1维护：未识别语文类型 (link)
7. Warren D. Goldfarb. The Undecidability of the Second-Order Unification Problem (PDF). Theoretical Computer Science. 1981, 13: 225–230 [2023-10-04]. （原始内容 (PDF)于2023-06-20）. 
8. Huet, Gérard. Higher Order Unification 30 years later (PDF). Carreño, V.; Muñoz, C.; Tahar, S. (编). Proceedings, 15th International Conference TPHOL. LNCS 2410. Springer. 2002: 3–12 [2023-10-04]. （原始内容 (PDF)于2016-03-04）. 
9. entry on HOL. [2023-10-04]. （原始内容于2016-06-17）. 
10. Fitting, Melvin. Types, Tableaus, and Gödel's God. Springer Science & Business Media. 2002: 139. ISBN 978-1-4020-0604-3. 哥德尔的论证是模态的，且至少是二阶，因为他在对上帝的定义中，有对性质的明确量化。[...] [AG96] 表明，可以不把论证的一部分看做二阶，而看做三阶。