高阶逻辑亦称“广义谓词逻辑”、“高阶谓词逻辑”。一阶逻辑的推广系统，谓词逻辑的重要组成部分。谓词逻辑有一阶逻辑和高阶逻辑之分。在一阶逻辑中，量词只能用于个体变元，取消这一限制条件，允许量词也可用于命题变元和谓词变元，由此构造起来的谓词逻辑就是高阶逻辑。公理化的高阶逻辑系统或高阶逻辑的自然推理系统又称为广义谓词演算或高阶谓词演算。
高阶逻辑区别于一阶逻辑的其他方式是在构造中允许下层的
类型论。高阶谓词是接受其他谓词作为参数的
谓词。一般的，阶为n的高阶谓词接受一个或多个（n− 1）阶的谓词作为参数，这里的n> 1。对
高阶函数类似的评述也成立。
高阶逻辑更加富有表达力，但是它们的性质，特别是有关
模型论的，使它们对很多应用不能表现良好。作为
哥德尔的结论，经典高阶逻辑不容许（
递归的
公理化的）可靠的和
完备的证明演算；这个缺陷可以通过使用Henkin模型来修补。
高阶逻辑区别于一阶逻辑的其他方式是在构造中允许下层的
类型论。
高阶逻辑更加富有表达力，但是它们的性质，特别是有关
模型论的，使它们对很多应用不能表现良好。作为
哥德尔的结论，经典高阶逻辑不容许(
递归的
公理化的)可靠的和
完备的证明演算；这个缺陷可以通过使用 Henkin 模型来修补。
高阶函数在数学和计算机科学中，高阶函数是至少满足下列一个条件的
函数:
接受一个或多个函数作为输入输出一个函数在数学中它们也叫做
算子(运算符)或
泛函。
微积分中的
导数就是常见的例子，因为它映射一个函数到另一个函数。
在无类型 lambda 演算，所有函数都是高阶的；在有类型 lambda 演算（大多数函数式编程语言都从中演化而来）中，高阶函数一般是那些函数型别包含多于一个箭头的函数。在函数式编程中，返回另一个函数的高阶函数被称为Curry化的函数。