高階邏輯
維基百科,自由的 encyclopedia
在數學與邏輯中,高階邏輯(縮寫HOL)是謂詞邏輯的一種形式,與一階邏輯的主要區別在於增加了量詞的作用元,命題變元和謂詞變元也能作約束變元(受量詞約束)且作謂詞變元的主目,有時語義也更強。例如,可量化謂詞的系統就是二階邏輯。 高階邏輯區別於一階邏輯的其他方式是在構造中允許下層的類型論。高階謂詞是接受其他謂詞作為參數的謂詞。一般的,階為n的高階謂詞接受一個或多個(n − 1)階的謂詞作為參數,這裏的n > 1。對高階函數類似的評述也成立。
高階邏輯更有表達力,但它們的性質,特別是有關模型論的,則不如一階邏輯完善,使它們對很多應用不能表現良好。
「高階邏輯」一般指高階簡單謂詞邏輯,「簡單」表示基礎類型論是簡單類型論。雷奧·屈斯克特和弗蘭克·普倫普頓·拉姆齊提出的簡單類型論是對阿爾弗雷德·諾思·懷特海和伯特蘭·羅素的《數學原理》的簡化。簡單類型有時也指不考慮多態類型和依賴類型。[1] 高階邏輯的一個實例是構造演算。