firstorderformula
一階邏輯的合式公式，在形式化的一階語言中遞歸地定義的公式。設
是一階邏輯的一個形式語言，
含邏輯符號和非邏輯符號。
中的非邏輯符號有：關係符號P，Q，R等；函式符號F，G等；常量符號c,d,e等。每個關係符號，函式符號都指定是n元關係或n元函式。
中的邏輯符號有：個體變元符號
，…等；邏輯聯詞
、→等；量詞
；等號≡；括弧)，(。
的項t：t可以是單個個體變元，也可以是單個個體常量：如果t1…tm是項，F是L的m元函式符號，則F(t1…tm)是項。
的原子公式：如果t1、t2是
的項，則t1≡t2是原子公式；如果t1…tn是項，R是L的n元關係符號，則R(t1…tn)是原子公式。
的公式：
的原子公式是公式；設φ、ψ是L的公式，x是
的一個個體變元，則(
φ)，(φ→ψ)，(
xφ)都是
的公式。這樣定義的語言公式乃至公式的集合統稱一階語言
。只要指出
的非邏輯符號，一階語言
就被確定。
中其他的聯結符，量詞都不是原始符號，＾，ˇ，的定義見命題公式，存在量詞定義為xφ
x
φ。一階公式中的一個個體變元如果出現在量詞的轄域中就稱為約束變元，不受任何一個量詞約束的變元稱為自由變元。沒有自由變元的公式稱為句子。