高階邏輯

在數學與邏輯中，高階邏輯（縮寫HOL）是謂詞邏輯的一種形式，與一階邏輯的主要區別在於增加了量詞的作用元，命題變元和謂詞變元也能作約束變元（受量詞約束）且作謂詞變元的主目，有時語義也更強。例如，可量化謂詞的系統就是二階邏輯。 高階邏輯區別於一階邏輯的其他方式是在構造中允許下層的類型論。高階謂詞是接受其他謂詞作為參數的謂詞。一般的，階為n的高階謂詞接受一個或多個（n − 1）階的謂詞作為參數，這裏的n > 1。對高階函數類似的評述也成立。

高階邏輯更有表達力，但它們的性質，特別是有關模型論的，則不如一階邏輯完善，使它們對很多應用不能表現良好。

「高階邏輯」一般指高階簡單謂詞邏輯，「簡單」表示基礎類型論是簡單類型論。雷奧·屈斯克特和弗蘭克·普倫普頓·拉姆齊提出的簡單類型論是對阿爾弗雷德·諾思·懷特海和伯特蘭·羅素的《數學原理》的簡化。簡單類型有時也指不考慮多態類型和依賴類型。^[1] 高階邏輯的一個實例是構造演算。

量化範圍

一階邏輯只量化個體；二階邏輯也量化集合；三階邏輯可以量化集合的集合，以此類推。

高階邏輯是一階、二階、三階……n階邏輯的結合，也就是說允許對任意嵌套的集合進行量化。

語義

高階邏輯有兩種可能的語義。

在標準語義或完整語義中，對高階對象的量化包含其中所有可能的對象。例如，對個體集合的量化範圍是個體集合的整個冪集。因此，在標準語義中，一旦指定了個體集合，就足以指定所有量詞。高階邏輯的標準語義也因此比一階邏輯更有表達力，例如其允許對自然數與實數進行範疇公理化，這在一階邏輯中是不可能的。但根據哥德爾的結論，高階邏輯的標準語義不容許（遞歸的公理化的）可靠、完備的證明演算^[2]。高階邏輯標準語義的模型論性質也比一階邏輯複雜，例如二階邏輯的勒文海姆數甚至大於一階邏輯的可測基數（若存在這樣的基數）。^[3]一階邏輯的勒文海姆數則有ℵ₀個，是最小的無窮基數。

在Henkin語義中，每種高階類型的解釋都包含單獨的域。所以，對個體集合的量化可能只涉及個體集合冪集的一個子集，配備此種語義的高階邏輯等同於一階多類邏輯，而非強於一階邏輯。特別地，高階邏輯的Henkin語義具有一階邏輯的所有模型論性質，且從一階邏輯繼承了可靠、完備的證明系統。

性質

高階邏輯包括阿隆佐·邱奇的簡單類型論的分支^[4]和直覺類型論的各種形式。Gérard Huet已經證明，三階邏輯的類型論中，合一是不可判定問題^[5][6][7][8]，也就是說不會有算法可以決定二階（遑論高階）的任意方程是否有解。

在同構意義下，冪集運算在二階邏輯在可以定義。利用這一觀察結果，亞科·欣蒂卡在1955年確定，二階邏輯可以模擬高價邏輯，即對高階邏輯的所有公式，都可在二階邏輯中找到其等可滿足公式。^[9]

「高階邏輯」一詞在某些情況下被認為是指經典高階邏輯，但模態高階邏輯也有研究。根據一些邏輯學家的說法，哥德爾本體論證明最好（在技術上）在這樣的語境中研究。^[10]

參見

• 高階文法
• 有類型lambda演算
• 直覺類型論

延伸閱讀

• Alonzo Church: A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, Vol. 5, 1940, 56-68.
• Leon Henkin: Completeness in the theory of types. Journal of Symbolic Logic, Vol. 15, 1950, 81-91.
• Peter B. Andrews: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. 2nd edition, Academic Press 2002.
• J. Lambek, P. J. Scott: Introduction to Higher Order Categorical Logic. Cambridge University Press 1986.

外部連結

• A short article from the Encyclopedia of Artificial Intelligence

1. Jacobs, 1999, chapter 5
2. Shapiro 1991, p. 87.
3. Menachem Magidor and Jouko Väänänen. "On Löwenheim-Skolem-Tarski numbers for extensions of first order logic （頁面存檔備份，存於互聯網檔案館）", Report No. 15 (2009/2010) of the Mittag-Leffler Institute.
4. Alonzo Church, A formulation of the simple theory of types （頁面存檔備份，存於互聯網檔案館）, The Journal of Symbolic Logic 5(2):56–68 (1940)
5. Huet, Gérard P. The Undecidability of Unification in Third Order Logic. Information and Control. 1973, 22 (3): 257–267. doi:10.1016/s0019-9958(73)90301-x.
6. Huet, Gérard. Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (學位論文). Universite de Paris VII. Sep 1976 [2023-10-25]. （原始內容存檔於2023-06-13） （French）. 引文格式1維護：未識別語文類型 (link)
7. Warren D. Goldfarb. The Undecidability of the Second-Order Unification Problem (PDF). Theoretical Computer Science. 1981, 13: 225–230 [2023-10-04]. （原始內容存檔 (PDF)於2023-06-20）.
8. Huet, Gérard. Higher Order Unification 30 years later (PDF). Carreño, V.; Muñoz, C.; Tahar, S. (編). Proceedings, 15th International Conference TPHOL. LNCS 2410. Springer. 2002: 3–12 [2023-10-04]. （原始內容存檔 (PDF)於2016-03-04）.
9. entry on HOL. [2023-10-04]. （原始內容存檔於2016-06-17）.
10. Fitting, Melvin. Types, Tableaus, and Gödel's God. Springer Science & Business Media. 2002: 139. ISBN 978-1-4020-0604-3. 哥德爾的論證是模態的，且至少是二階，因為他在對上帝的定義中，有對性質的明確量化。[...] [AG96] 表明，可以不把論證的一部分看做二階，而看做三階。