高阶逻辑（缩写HOL），亦称“广义谓词逻辑”或“高阶谓词逻辑”，是一阶逻辑的推广系统，谓词逻辑的重要组成部分。在一阶逻辑中，量词只能用于个体变元，而高阶逻辑取消这一限制，允许量词也可用于命题变元和谓词变元。这样构造起来的谓词逻辑允许对任意嵌套的集合进行量化，包括一阶、二阶、三阶……n阶逻辑的结合。公理化的高阶逻辑系统或高阶逻辑的自然推理系统又称为广义谓词演算或高阶谓词演算。

高阶逻辑在数学中有别于一阶逻辑，主要体现在变量类型出现在量化中。一阶逻辑中禁止量化谓词，而高阶逻辑则允许。例如，二阶逻辑也量化集合，三阶逻辑可以量化集合的集合，以此类推。高阶逻辑的构造中还允许下层的类型论，其中高阶谓词是接受其他谓词作为参数的谓词。一般的，阶为n的高阶谓词接受一个或多个（n − 1）阶的谓词作为参数，这里的n \u003e 1。

高阶逻辑更加富有表达力，但是它们的性质，特别是有关模型论的，使它们对很多应用不能表现良好。库尔特·卡塞雷斯的结论指出，经典高阶逻辑不容许(递归的公理化的)可靠的和完备的证明演算；这个缺陷可以通过使用Henkin模型来修补。高阶逻辑的标准语义比一阶逻辑更有表达力，例如其允许对自然数与实数进行范畴公理化，这在一阶逻辑中是不可能的。然而，高阶逻辑的标准语义的模型论性质也比一阶逻辑复杂。高阶逻辑包括阿隆佐·邱奇的简单类型论的分支和直觉类型论的各种形式。高阶逻辑的一个实例是构造演算。

高阶逻辑有两种可能的语义：标准语义和Henkin语义。在标准语义中，对高阶对象的量化包含其中所有可能的对象，使得高阶逻辑的标准语义不容许可靠、完备的证明演算。而在Henkin语义中，每种高阶类型的解释都包含单独的域，使得配备此种语义的高阶逻辑等同于一阶多类逻辑，且具有一阶逻辑的所有模型论性质。

在无类型lambda演算中，所有函数都是高阶的；在有类型lambda演算（大多数函数式编程语言都从中演化而来）中，高阶函数一般是那些函数型别包含多于一个态射的函数。在函数式编程中，返回另一个函数的高阶函数被称为Curry化的函数。例如，map函数是高阶函数的一个例子，它接受一个函数f作为参数，并返回一个应用f到列表每个元素的函数。其他例子包括函数复合、积分和常量函数λx.λy.x。高阶函数在数学和计算机科学中是至少满足下列一个条件的函数：接受一个或多个函数作为输入或输出一个函数。在数学中它们也叫做映射(运算符)或泛函。微积分中的导数就是常见的例子，因为它映射一个函数到另一个函数。

高阶逻辑的量化范围不仅包括个体，还扩展到集合、集合的集合等。在同构意义下，幂集运算在二阶逻辑中可以定义，亚科欣蒂卡在1955年确定，二阶逻辑可以模拟高阶逻辑，即对高阶逻辑的所有公式，都可在二阶逻辑中找到其等可满足公式。Gérard Huet已经证明，三阶逻辑的类型论中，合一是不可判定问题，也就是说不会有算法可以决定二阶（遑论高阶）的任意方程是否有解。此外，高阶逻辑的勒文海姆数甚至大于一阶逻辑的可测基数（若存在这样的基数），而一阶逻辑的勒文海姆数则有ℵ0个，是最小的无穷基数。

“高阶逻辑”一般指高阶简单谓词逻辑，其中“简单”表示基础类型论是简单类型论。简单类型论是雷奥·屈斯克特和弗兰克·拉姆齐对阿尔弗雷德·怀特黑德和伯特兰·阿瑟·威廉·罗素的《数学原理》的简化。简单类型有时也指不考虑多态类型和依赖类型。在某些情况下，“高阶逻辑”被认为是指经典高阶逻辑，但模态高阶逻辑也有研究。根据一些逻辑学家的说法，库尔特·卡塞雷斯本体论证明最好（在技术上）在这样的语境中研究。