Loading AI tools
来自维基百科,自由的百科全书
在數學與邏輯中,高階邏輯(縮寫HOL)是謂詞邏輯的一種形式,與一階邏輯的主要區別在於增加了量詞的作用元,命題變元和謂詞變元也能作約束變元(受量詞約束)且作謂詞變元的主目,有時語義也更強。例如,可量化謂詞的系統就是二階邏輯。 高階邏輯區別於一階邏輯的其他方式是在構造中允許下層的類型論。高階謂詞是接受其他謂詞作為參數的謂詞。一般的,階為n的高階謂詞接受一個或多個(n − 1)階的謂詞作為參數,這裡的n > 1。對高階函數類似的評述也成立。
高階邏輯更有表達力,但它們的性質,特別是有關模型論的,則不如一階邏輯完善,使它們對很多應用不能表現良好。
「高階邏輯」一般指高階簡單謂詞邏輯,「簡單」表示基礎類型論是簡單類型論。雷奧·屈斯克特和弗蘭克·普倫普頓·拉姆齊提出的簡單類型論是對阿爾弗雷德·諾思·懷特海和伯特蘭·羅素的《數學原理》的簡化。簡單類型有時也指不考慮多態類型和依賴類型。[1] 高階邏輯的一個實例是構造演算。
一階邏輯只量化個體;二階邏輯也量化集合;三階邏輯可以量化集合的集合,以此類推。
高階邏輯是一階、二階、三階……n階邏輯的結合,也就是說允許對任意嵌套的集合進行量化。
高階邏輯有兩種可能的語義。
在標準語義或完整語義中,對高階對象的量化包含其中所有可能的對象。例如,對個體集合的量化範圍是個體集合的整個冪集。因此,在標準語義中,一旦指定了個體集合,就足以指定所有量詞。高階邏輯的標準語義也因此比一階邏輯更有表達力,例如其允許對自然數與實數進行範疇公理化,這在一階邏輯中是不可能的。但根據哥德爾的結論,高階邏輯的標準語義不容許(遞歸的公理化的)可靠、完備的證明演算[2]。高階邏輯標準語義的模型論性質也比一階邏輯複雜,例如二階邏輯的勒文海姆數甚至大於一階邏輯的可測基數(若存在這樣的基數)。[3]一階邏輯的勒文海姆數則有ℵ0個,是最小的無窮基數。
在Henkin語義中,每種高階類型的解釋都包含單獨的域。所以,對個體集合的量化可能只涉及個體集合冪集的一個子集,配備此種語義的高階邏輯等同於一階多類邏輯,而非強於一階邏輯。特別地,高階邏輯的Henkin語義具有一階邏輯的所有模型論性質,且從一階邏輯繼承了可靠、完備的證明系統。
高階邏輯包括阿隆佐·邱奇的簡單類型論的分支[4]和直覺類型論的各種形式。Gérard Huet已經證明,三階邏輯的類型論中,合一是不可判定問題[5][6][7][8],也就是說不會有算法可以決定二階(遑論高階)的任意方程是否有解。
在同構意義下,冪集運算在二階邏輯在可以定義。利用這一觀察結果,亞科·欣蒂卡在1955年確定,二階邏輯可以模擬高價邏輯,即對高階邏輯的所有公式,都可在二階邏輯中找到其等可滿足公式。[9]
「高階邏輯」一詞在某些情況下被認為是指經典高階邏輯,但模態高階邏輯也有研究。根據一些邏輯學家的說法,哥德爾本體論證明最好(在技術上)在這樣的語境中研究。[10]
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.