一階謂詞演算

一階謂詞演算亦稱“狹謂詞演算”。形式化的一階邏輯系統。一般有公理系統和自然推理系統兩種。

邏輯史上第一個完備的公理化的一階謂詞演算是19世紀末由德國邏輯學家弗雷格建立的，最早的一階謂詞邏輯自然推理系統則由甘岑於20世紀30年代建立。