一階邏輯
概況
一階謂詞演算或一階邏輯(FOL)允許量化陳述的公式，比如"存在着 x，..." (x) 或 "對於任何 x，..." (砢)，這裡的 x 是論域(domain of discourse)的成員。一階(遞歸)公理化理論是通過增加一階句子/斷定的遞歸可枚舉集合作為公理，可以被公理化為一階邏輯擴展的理論。這裡的"..."叫做謂詞並表達某種性質。謂詞是適用於某些事物的表達。所以，表達"是黃色"或"喜歡椰菜"分別適用於是黃色或喜歡椰菜的那些事物。
一階邏輯是區別於高階邏輯的數理邏輯，它不允許量化性質。性質是一個物體的特性;所以一個紅色物體被表述為有紅色的特性。性質可以被當作物體只憑自身的一種構成(form)，它可以擁有其他性質。性質被認為有別於擁有它的物體。所以一階邏輯不能表達下列陳述，"對於所有的性質 P，..." 或"存在着性質 P，..."。
但是，一階邏輯足夠強大了，它可以形式化全部的集合論和幾乎所有的數學。把量化限制於個體(individual)使它難於用於拓撲學目的，但它是在數學底層經典的邏輯理論。它是比句子邏輯強比二階邏輯弱的理論。
一階邏輯的定義
謂詞演算構成如下
生成規則(就是形成合式公式的遞歸定義)。
變換規則(就是推導定理的推理規則)。
公理或公理模式的(可能的可數的無限)集合。
有兩種類型的公理: 邏輯公理，它是對於謂詞演算有效的，和非邏輯公理，它是在特殊情況下為真的，就是說，在它所在的理論的標準解釋中是真的。例如，非邏輯的皮亞諾公理在算術的符號主義標準解釋下是真的，但是對於謂詞演算它們不是有效的。
在公理的集合是無限的的時候，需要能判定給定的合式公式是否是一個公理的一個算法。進一步的，應當有可以判定一個推理規則的應用是否正確的算法。