高階邏輯

在數學中，高階邏輯在很多方面有別於一階邏輯。

其一是變量類型出現在量化中；粗略的說，一階邏輯中禁止量化謂詞。允許這麼做的系統請參見二階邏輯。

高階邏輯區別於一階邏輯的其他方式是在構造中允許下層的類型論。高階謂詞是接受其他謂詞作為參數的謂詞。一般的，階為n的高階謂詞接受一個或多個（n − 1）階的謂詞作為參數，這裡的n > 1。對高階函數類似的評述也成立。

高階邏輯更加富有表達力，但是它們的性質，特別是有關模型論的，使它們對很多應用不能表現良好。作為哥德爾的結論，經典高階邏輯不容許（遞歸的公理化的）可靠的和完備的證明演算；這個缺陷可以通過使用Henkin模型來修補。

高階邏輯的一個實例是構造演算。

參見

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

外部連結

• A short article from the Encyclopedia of Artificial Intelligence

文獻

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