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

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

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

量化範圍

編輯

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

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

語義

編輯

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

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

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

性質

編輯

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

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

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

參見

編輯

延伸閱讀

編輯
  • 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.

外部連結

編輯
  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). 
  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] 表明,可以不把論證的一部分看做二階,而看做三階。