數學分支之十九:數理邏輯論的體系
數理邏輯的主要分支包括:邏輯演算(包括命題演算和謂詞演算)、模型論、證明論、遞歸論和公理化集合論。數理邏輯和計算機科學有許多重合之處,兩者都屬于模擬人類認知機理的科學。許多計算機科學的先驅者既是數學家、又是邏輯學家,如阿蘭·圖靈、邱奇等。
程序語言學、語義學的研究從模型論衍生而來,而程序驗證則從模型論的模型檢測衍生而來。
柯里——霍華德同構給出了“證明”和“程序”的等價性,這一結果與證明論有關,直覺邏輯和線性邏輯在此起了很大作用。λ演算和組合子邏輯這樣的演算現在屬于理想程序語言。
計算機科學在自動驗證和自動尋找證明等技巧方面的成果對邏輯研究做出了貢獻,比如說自動定理證明和邏輯編程。