高階邏輯（縮寫HOL），亦稱“廣義謂詞邏輯”或“高階謂詞邏輯”，是一階邏輯的推廣系統，謂詞邏輯的重要組成部分。在一階邏輯中，量詞只能用于個體變元，而高階邏輯取消這一限制，允許量詞也可用于命題變元和謂詞變元。這樣構造起來的謂詞邏輯允許對任意嵌套的集合進行量化，包括一階、二階、三階……n階邏輯的結合。公理化的高階邏輯系統或高階邏輯的自然推理系統又稱為廣義謂詞演算或高階謂詞演算。
簡介
高階邏輯在數學中有別于一階邏輯，主要體現在變量類型出現在量化中。一階邏輯中禁止量化謂詞，而高階邏輯則允許。例如，二階邏輯也量化集合，三階邏輯可以量化集合的集合，以此類推。高階邏輯的構造中還允許下層的類型論，其中高階謂詞是接受其他謂詞作為參數的謂詞。一般的，階為n的高階謂詞接受一個或多個（n ? 1）階的謂詞作為參數，這里的n > 1。
性質
高階邏輯更加富有表達力，但是它們的性質，特別是有關模型論的，使它們對很多應用不能表現良好。庫爾特·卡塞雷斯的結論指出，經典高階邏輯不容許(遞歸的公理化的)可靠的和完備的證明演算；這個缺陷可以通過使用Henkin模型來修補。高階邏輯的標準語義比一階邏輯更有表達力，例如其允許對自然數與實數進行范疇公理化，這在一階邏輯中是不可能的。然而，高階邏輯的標準語義的模型論性質也比一階邏輯復雜。高階邏輯包括阿隆佐·邱奇的簡單類型論的分支和直覺類型論的各種形式。高階邏輯的一個實例是構造演算。
語義
高階邏輯有兩種可能的語義：標準語義和Henkin語義。在標準語義中，對高階對象的量化包含其中所有可能的對象，使得高階邏輯的標準語義不容許可靠、完備的證明演算。而在Henkin語義中，每種高階類型的解釋都包含單獨的域，使得配備此種語義的高階邏輯等同于一階多類邏輯，且具有一階邏輯的所有模型論性質。
演算
在無類型lambda演算中，所有函數都是高階的；在有類型lambda演算（大多數函數式編程語言都從中演化而來）中，高階函數一般是那些函數型別包含多于一個態射的函數。在函數式編程中，返回另一個函數的高階函數被稱為Curry化的函數。例如，map函數是高階函數的一個例子，它接受一個函數f作為參數，并返回一個應用f到列表每個元素的函數。其他例子包括函數復合、積分和常量函數λx.λy.x。高階函數在數學和計算機科學中是至少滿足下列一個條件的函數：接受一個或多個函數作為輸入或輸出一個函數。在數學中它們也叫做映射(運算符)或泛函。微積分中的導數就是常見的例子，因為它映射一個函數到另一個函數。
量化范圍與模型論性質
高階邏輯的量化范圍不僅包括個體，還擴展到集合、集合的集合等。在同構意義下，冪集運算在二階邏輯中可以定義，亞科欣蒂卡在1955年確定，二階邏輯可以模擬高階邏輯，即對高階邏輯的所有公式，都可在二階邏輯中找到其等可滿足公式。Gérard Huet已經證明，三階邏輯的類型論中，合一是不可判定問題，也就是說不會有算法可以決定二階（遑論高階）的任意方程是否有解。此外，高階邏輯的勒文海姆數甚至大于一階邏輯的可測基數（若存在這樣的基數），而一階邏輯的勒文海姆數則有?0個，是最小的無窮基數。
類型論
“高階邏輯”一般指高階簡單謂詞邏輯，其中“簡單”表示基礎類型論是簡單類型論。簡單類型論是雷奧·屈斯克特和弗蘭克·拉姆齊對阿爾弗雷德·懷特黑德和伯特蘭·阿瑟·威廉·羅素的《數學原理》的簡化。簡單類型有時也指不考慮多態類型和依賴類型。在某些情況下，“高階邏輯”被認為是指經典高階邏輯，但模態高階邏輯也有研究。根據一些邏輯學家的說法，庫爾特·卡塞雷斯本體論證明最好（在技術上）在這樣的語境中研究。
參考資料 >