高階述語論理（こうかいじゅつごろんり、英: Higher-order logic）は、一階述語論理と様々な意味で対比される用語である。
例えば、その違いは量化される変項の種類にも現われている。一階述語論理では、大まかに言えば述語に対する量化ができない。述語を量化できる論理体系については二階述語論理に詳しい。
その他の違いとして、基盤となる型理論で許されている型構築の違いがある。高階述語（higher-order predicate）とは、引数として1つ以上の別の述語をとることができる述語である。一般に n 階の高階述語の引数は1つ以上の (n − 1) 階の述語である（ここで n > 1）。同じことは高階関数（higher-order function）にも言える。
高階述語論理は表現能力が高いが、その特性、特にモデル理論に関わる部分では、多くの応用について性格が良いとは言えない。クルト・ゲーデルの業績により、古典的高階述語論理の任意の標準モデルで真となる命題のみ、そしてそれらの全てを証明できるような（帰納的に公理化された）健全で完全な証明計算は存在しない。一方、モデルの範囲を（非標準的モデルを含む）ヘンキンモデルに拡大すれば、任意のモデルで真となる命題のみ、そしてそれらの全てを証明できるような、健全で完全な証明計算は存在する。
高階述語論理の例として、アロンゾ・チャーチの Simple Theory of Types や Calculus of Constructions (CoC) がある。
関連項目
型付きラムダ計算
参考文献
Andrews, P.B., 2002. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed. Kluwer Academic Publishers, available from Springer.
Church, Alonzo, 1940, "A Formulation of the Simple Theory of Types," Journal of Symbolic Logic 5: 56-68.
Henkin, Leon, 1950, "Completeness in the Theory of Types," Journal of Symbolic Logic 15: 81-91.
Stewart Shapiro, 1991, "Foundations Without Foundationalism: A Case for Second-Order Logic". Oxford University Press.
Stewart Shapiro, 2001, "Classical Logic II: Higher Order Logic," in Lou Goble, ed., The Blackwell Guide to Philosophical Logic. Blackwell.
Lambek, J. and Scott, P. J., 1986. Introduction to Higher Order Categorical Logic, Cambridge University Press.
外部リンク
Miller, Dale, 1991, "Logic: Higher-order," Encyclopedia of Artificial Intelligence, 2nd ed.
表
話
関連項目
（英語版）
数理論理学
数学
メタ論理学
メタ数学
モデル理論
哲学的論理学
哲学
論理学の哲学
数学の哲学
証明論
集合論
論理学の歴史
基本概念
アブダクション
分析的と総合的の区別（英語版）
二律背反
アプリオリ
演繹
定義(内包と外延)
記述
帰納
推論
論理的帰結
論理形式（英語版）
論理的含意（英語版）
論理的真理
名前
必要十分条件
意味
パラドックス
可能世界論
前提
確率
理性
推理
参考
意味論
命題
サブスティトゥーション（英語版）
統語論（英語版）
真理
真理値
妥当性
数学記号の表
批判的思考と非形式論理学
分析
曖昧
信念
信用性（英語版）
根拠
説明
説明力（英語版）
事実
誤謬
探究
意見
節約
根拠
プロパガンダ