高阶逻辑
维基百科,自由的 encyclopedia
在数学与逻辑中,高阶逻辑(缩写HOL)是谓词逻辑的一种形式,与一阶逻辑的主要区别在于增加了量词的作用元,命题变元和谓词变元也能作约束变元(受量词约束)且作谓词变元的主目,有时语义也更强。例如,可量化谓词的系统就是二阶逻辑。 高阶逻辑区别于一阶逻辑的其他方式是在构造中允许下层的类型论。高阶谓词是接受其他谓词作为参数的谓词。一般的,阶为n的高阶谓词接受一个或多个(n − 1)阶的谓词作为参数,这里的n > 1。对高阶函数类似的评述也成立。
高阶逻辑更有表达力,但它们的性质,特别是有关模型论的,则不如一阶逻辑完善,使它们对很多应用不能表现良好。
“高阶逻辑”一般指高阶简单谓词逻辑,“简单”表示基础类型论是简单类型论。雷奥·屈斯克特和弗兰克·普伦普顿·拉姆齐提出的简单类型论是对阿尔弗雷德·诺思·怀特海和伯特兰·罗素的《数学原理》的简化。简单类型有时也指不考虑多态类型和依赖类型。[1] 高阶逻辑的一个实例是构造演算。