複製鏈接
請複製以下鏈接發送給好友
https://baike.baidu.hk/item/高階邏輯/1508133
複製
複製成功

高階邏輯

鎖定
高階邏輯亦稱“廣義謂詞邏輯”、“高階謂詞邏輯”。一階邏輯的推廣系統，謂詞邏輯的重要組成部分。謂詞邏輯有一階邏輯和高階邏輯之分。在一階邏輯中，量詞只能用於個體變元，取消這一限制條件，允許量詞也可用於命題變元和謂詞變元，由此構造起來的謂詞邏輯就是高階邏輯。公理化的高階邏輯系統或高階邏輯的自然推理系統又稱為廣義謂詞演算或高階謂詞演算。 [1] 
中文名
高階邏輯
外文名
Logik höherer Stufe
釋    義
接受其他謂詞作為參數的謂詞
應    用
數學
實    例
構造演算

目錄

  1. 1 簡介
  2. 2 應用
  3. 3 性質
  4. 4 演算

高階邏輯簡介

在數學中，高階邏輯在很多方面有別於一階邏輯。其一是變量類型出現在量化中；粗略的説，一階邏輯中禁止量化謂詞。允許這麼做的系統請參見二階邏輯。
高階邏輯區別於一階邏輯的其他方式是在構造中允許下層的類型論。高階謂詞是接受其他謂詞作為參數的謂詞。一般的，階為n的高階謂詞接受一個或多個（n− 1）階的謂詞作為參數，這裏的n> 1。對高階函數類似的評述也成立。
高階邏輯更加富有表達力，但是它們的性質，特別是有關模型論的，使它們對很多應用不能表現良好。作為哥德爾的結論，經典高階邏輯不容許（遞歸的公理化的）可靠的和完備的證明演算；這個缺陷可以通過使用Henkin模型來修補。
高階邏輯的一個實例是構造演算。

高階邏輯應用

高階邏輯在數學中，高階邏輯在很多方面有別於一階邏輯。其一是變量類型出現在量化中；粗略的説，一階邏輯中禁止量化謂詞。允許這麼做的系統請參見二階邏輯。
高階邏輯區別於一階邏輯的其他方式是在構造中允許下層的類型論。

高階邏輯性質

高階邏輯更加富有表達力，但是它們的性質，特別是有關模型論的，使它們對很多應用不能表現良好。作為哥德爾的結論，經典高階邏輯不容許(遞歸的公理化的)可靠的和完備的證明演算；這個缺陷可以通過使用 Henkin 模型來修補。
高階邏輯的一個實例是構造演算。
高階函數在數學和計算機科學中，高階函數是至少滿足下列一個條件的函數:
接受一個或多個函數作為輸入輸出一個函數在數學中它們也叫做算子(運算符)或泛函。微積分中的導數就是常見的例子，因為它映射一個函數到另一個函數。 [2] 

高階邏輯演算

在無類型 lambda 演算，所有函數都是高階的；在有類型 lambda 演算（大多數函數式編程語言都從中演化而來）中，高階函數一般是那些函數型別包含多於一個箭頭的函數。在函數式編程中，返回另一個函數的高階函數被稱為Curry化的函數。
在很多函數式編程語言中能找到的 map 函數是高階函數的一個例子。它接受一個函數 f 作為參數，並返回接受一個列表並應用 f 到它的每個元素的一個函數。
高階函數的其他例子包括函數複合、積分和常量函數 λx.λy.x。 [2] 
參考資料
  • 1.    彭漪漣．邏輯學大辭典：上海辭書出版社，2004年12月
  • 2.    Peter B. Andrews: An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Academic Press, 1986.