跳转到内容

高阶逻辑

维基百科,自由的百科全书

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

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

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

量化范围

[编辑]

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

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

语义

[编辑]

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

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

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

性质

[编辑]

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

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

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

参见

[编辑]

延伸阅读

[编辑]
  • 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). 
  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] 表明,可以不把论证的一部分看做二阶,而看做三阶。