高阶逻辑

维基百科,自由的百科全书
跳转至: 导航搜索

数学中,高阶逻辑在很多方面有别于一阶逻辑

其一是变量类型出现在量化中;粗略的说,一阶逻辑中禁止量化谓词。允许这么做的系统请参见二阶逻辑

高阶逻辑区别于一阶逻辑的其他方式是在构造中允许下层的类型论高阶谓词是接受其他谓词作为参数的谓词。一般的,阶为n的高阶谓词接受一个或多个(n − 1)阶的谓词作为参数,这里的n > 1。对高阶函数类似的评述也成立。

高阶逻辑更加富有表达力,但是它们的性质,特别是有关模型论的,使它们对很多应用不能表现良好。作为哥德尔的结论,经典高阶逻辑不容许(递归公理化的)可靠的和完备证明演算;这个缺陷可以通过使用Henkin模型来修补。

高阶逻辑的一个实例是构造演算

参见[编辑]

外部链接[编辑]

文献[编辑]

  • 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.