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