正文
在一階邏輯中描述一個數學理論，首先會涉及這個理論所討論的對象、定義在這些對象上的函式、以及這些對象之間的關係或性質。數學理論所討論的對象稱為個體，由個體組成的非空集合稱為論域或個體域。按通常數學中的定義，一個n元函式就是從論域A的個體的所有n元組的集合至A中的一個映射。A中個體的n元組(α1,α2,…,αn)經映射F對應到A中的個體表示為F(α1,α2,…,αn)。函式增加了個體的表達形式。人們也考慮論域A中哪些n元組滿足關係R，即A中哪些n元組(α1,α2,…,αn)使得R(α1,α2,…,αn)為真。此時的R(α1,α2,…,αn)就是一個命題。在各種關係中，相等關係是經常要用的。因為常常需要知道不同個體的表達式是否指稱同一個對象。例如3+3與2×3是否表示同一個數。
可以將關係或命題用命題連線詞來構成更複雜的關係或命題。當描述一些個數為無窮的對象的性質時，就需要引進量詞。例如說“對任何一個自然數，都有一個比它大的素數”時，就引進了量詞“所有個體”及“存在個體”，並且將關係或命題經量詞構成了更複雜的關係或命題。“論域中的所有個體”稱為全稱量詞，由它所構成的命題“論域中所有的個體有某性質”，當論域中所有個體都有此性質時，此命題是真的，否則為假。“論域中存在個體”稱為存在量詞，由它所構成的命題“論域中存在個體有某性質”，當論域中某些個體有此性質時為真，否則為假。
“所有個體”、“存在個體”中，量詞加在論域的個體上，稱為一階量詞。在一階邏輯中使用的量詞僅限於一階量詞。“所有函式”、“存在函式”、“所有關係”和“存在關係”是二階量詞。此外還有更高階的量詞。相應地也有二階邏輯、高階邏輯等。
按照建立形式系統的一般原則（見邏輯演算），一階邏輯的形式系統應包括它的語言，即一階語言，以及邏輯公理和推理規則。
一階語言的符號包括以下幾類。
①個體變元x，y，z，…。
②函式符號（表示函式）ƒ，g，h，…；個體符號（表示論域中的個體）α，b，с，…；及謂詞（表示關係）p,Q，R，…。其中有一個二元謂詞=,稱為等詞（表示恆同關係）。
③命題聯結詞塡,∧，∨，→,凮以及量詞(存在量詞)，凬（全稱量詞）。
①，③及等詞稱為邏輯符號，其他符號，即等詞外的②稱為非邏輯符號。
歸納地定義一階語言的項和公式，也稱之為形成規則。項的定義：
①變元和個體符號是項。
②若t1,t2,…,tn是項，ƒ是一個n元函式符號,則ƒ(t1,t2,…,tn)是項。
公式可定義為：
①若t1,t2,…,tn是項，p是n元謂詞符號,則p(t1,t2,…,tn)是公式，也稱為原子公式。
②若A是公式，則塡A是公式；若A，B是公式，則A∧B，A∨B，A→B，A凮B是公式。
③若A是公式，則xA,凬xA是公式。
如果變元x出現在公式A中形如xB或凬xB的部分，稱這個出現為x在A中的約束出現；否則，稱為x在A中的自由出現。例如在公式x=0∨x(x>0)中，第一個x是自由出現,第二、三個x是約束出現。沒有變元自由出現的公式稱為閉公式。
謂詞演算作為一個形式系統，可以規定它的解釋。給定一個論域，對於謂詞演算中出現的個體符號、函式符號及謂詞依次解釋為論域中的個體及定義在此論域上的函式及關係。此論域及其對於謂詞演算中形式符號的解釋稱為該演算的一個結構或模型。由對於個體符號和函式符號的解釋可知,項可解釋為複合函式,它指稱個體。原子公式p(t1,t2,…,tn)解釋為t1,t2,…,tn所指稱的個體滿足n元關係p。若公式A(x)表示關係，則凬xA(x)解釋為論域中所有個體滿足關係A，xA(x)解釋為論域中存在某個體滿足關係A。
謂詞演算的推理規則可規定如下：
謂詞演算的邏輯公理陳述邏輯符號的性質，分為三類：
①命題公理將重言式（見命題邏輯）中出現的命題變元代之以謂詞演算中的任意公式後得到的公式；
②恆同公理x=x及相等性公理
③替換公理Ax【α】→xA及凬xA→Ax【α】,其中Ax【α】表示將公式A中所有x的自由出現代之以項α。
謂詞演算的公理，即邏輯公理並不界定具體的函式或關係，而僅僅處理邏輯詞項的一般性質。換言之，對它的個體符號、函式符號、及謂詞的解釋可以是任意論域中的任意個體、函式及關係。謂詞演算的這個抽象性質對於近年來模型論的發展是本質的。
在謂詞演算的框架中，用形式語言表述數學的公理（並不一定能完全表述），就得到不同數學理論的形式系統。這類形式公理刻畫了某些具體的非邏輯符號的性質，稱為非邏輯公理。例如：
全序理論的形式系統中僅有一個非邏輯符號二元謂詞≤。除邏輯公理外，它還有非邏輯公理:①x≤y∧y≤z→x≤z;②x≤y∧y≤x→x=y；③x≤x;④x≤y∨y≤x。自然數集合及其上的順序關係就是全序理論的一個模型。
群論的形式系統中只有兩個非邏輯符號：個體符號1及二元函式符號·。它的非邏輯公理為：①x·(y·z)=(x·y)·z；②x·1=x；1·x=x；③y(x·y=1∧y·x=1)。任何一個群都是它的模型。
數論的形式系統中的非邏輯符號有：個體符號0,一元函式符號s及兩個二元函式符號＋及·。數論（或皮亞諾算術）的公理為：①塡s(x)=0，②s(x)=s(y)→x=y，③x+0=x，④x+s(x)=s(x+y)，⑤x·0=0，⑥x·s(y)=（x·y）+x，⑦若A為系統內的公式，x0在A中自由出現,則對每個這樣的公式A，有公理自然數的算術就是它的一個模型。
陳述在一階語言中，由邏輯公理、非邏輯公理及推理規則推出的全部形式定理（見邏輯演算）稱為一階理論，記為T。為區別不同的一階理論T,只要指出T的語言中的非邏輯符號及非邏輯公理就夠了。任何一階理論都包含了謂詞演算作為它的子系統。
在謂詞演算的任意模型中均為真的公式稱為永真的或有效的公式。例如,公式A(x,y)∨塡A(x,y)就是有效的公式，而x≤y∨y≤x就不是有效的。因為在全序結構中，對x，y在個體域中的任意取值，該公式的解釋均為真。而在半序結構中，例如該結構的論域為一個集合的全體子集的集合，≤解釋為集合的包含關係，那么上式的解釋當x，y取任意的兩個子集時就不都是真的了。
直觀上看，邏輯的定理應當是在一切可能的世界中均為真的定理。在一定意義下，謂詞演算滿足這個性質。可以驗證，謂詞演算的公理均為有效的，它的推理規則的假設有效則結論也必有效。因此，謂詞演算的所有定理都是有效的。這個性質稱為謂詞演算的有效性或可靠性。反之，任意有效的公式必為謂詞演算的定理。這就是著名的哥德爾完備性定理。由K.哥德爾於1930年證明。
用├A表示A是謂詞演算的形式定理，即A是系統內的定理。而可靠性與完備性刻畫了整個形式系統的性質，是關於系統的定理，也稱為元定理。形式系統的性質是數理邏輯主要的研究對象之一。
由謂詞演算的有效性及完備性容易推知一階理論的可靠性與完備性。使一階理論T的所有公理為真的結構稱為T的一個模型。若T的一個公式A在T的任意模型中均有效，稱A在T中有效，記為T喺A。A是T的定理記為T├A。那么T的可靠性與完備性就可以陳述為T├A的充分必要條件為T喺A。
若不存在A使得T├A且├塡A，則稱T是協調的。
若T是協調的，則T必有模型（廣義完備性定理）。
形如x1，x2,…,xnB的公式稱為前束型公式，其中xi表示xj或凬xj，B是一個不含量詞的公式。任何一個一階理論T(當T的非邏輯公理集為空集時就是一個謂詞演算)的公式A，都有一個公式A′，使得T├A凮A┡,其中A┡為前束型公式x1,x2,…,xηB，且B中的非邏輯符號均在A中出現。A′也稱為A的前束範式。此性質可用於對謂詞演算或一階理論的公式進行分類上。此時只需考慮前束範式中的量詞，將它作為公式複雜性的一種測度。
