研究數學中由個體、函數及關係構成的命題以及由這些命題經使用量詞和命題連接詞構成的更複雜的命題和這類命題之間的推理關係。在為數學的語言和推理建立形式系統的過程中,一階邏輯處於核心地位,多數常見的數學公理系統都可在一階邏輯中表述。(F.L.)G.弗雷格首先建立瞭一階邏輯的形式系統(1897)。人們也稱之為謂詞演算。其後,A.N.懷特海和B.A.W.羅素使其進一步精確化(1910)。

  在一階邏輯中描述一個數學理論,首先會涉及這這個理論所討論的對象、定義在這些對象上的函數、以及這些對象之間的關系或性質。數學理論所討論的對象稱為個體,由個體組成的非空集合稱為論域或個體域。按通常數學中的定義,一個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是否表示同一個數。

  可以將關系或命題用命題連接詞來構成更復雜的關系或命題。當描述一些個數為無窮的對象的性質時,就需要引進量詞。例如說“對任何一個自然數,都有一個比它大的素數”時,就引進瞭量詞“所有個體”及“存在個體”,並且將關系或命題經量詞構成瞭更復雜的關系或命題。“論域中的所有個體”稱為全稱量詞,由它所構成的命題“論域中所有的個體有某性質”,當論域中所有個體都有此性質時,此命題是真的,否則為假。“論域中存在個體”稱為存在量詞,由它所構成的命題“論域中存在個體有某性質”,當論域中某些個體有此性質時為真,否則為假。

  “所有個體”、“存在個體”中,量詞加在論域的個體上,稱為一階量詞。在一階邏輯中使用的量詞僅限於一階量詞。“所有函數”、“存在函數”、“所有關系”和“存在關系”是二階量詞。此外還有更高階的量詞。相應地也有二階邏輯、高階邏輯等。

  按照建立形式系統的一般原則(見邏輯演算),一階邏輯的形式系統應包括它的語言,即一階語言,以及邏輯公理和推理規則。

  一階語言的符號包括以下幾類。

  ① 個體變元xyz,…。

  ② 函數符號(表示函數)fgh,…;個體符號(表示論域中的個體)αb,с,…;及謂詞(表示關系)pQR,…。其中有一個二元謂詞=,稱為等詞(表示恒同關系)。

  ③ 命題聯結詞¬,∧,∨,→,↔以及量詞

(存在量詞),∀(全稱量詞)。

  ①,③及等詞稱為邏輯符號,其他符號,即等詞外的②稱為非邏輯符號。

  歸納地定義一階語言的項和公式,也稱之為形成規則。項的定義:

  ① 變元和個體符號是項。

  ② 若t1t2,…,tn是項,f是一個n元函數符號,則f(t1t2,…,tn)是項。

  公式可定義為:

  ① 若t1t2,…,tn是項,pn元謂詞符號,則p(t1t2,…,tn)是公式,也稱為原子公式。

  ② 若A是公式,則¬A是公式;若AB是公式,則ABABABAB是公式。

  ③ 若A是公式,則

x A,∀ x A是公式。

  如果變元x出現在公式A中形如

x B或∀ x B的部分,稱這個出現為 xA中的約束出現;否則,稱為 xA中的自由出現。例如在公式 x=0∨ x( x>0)中,第一個 x是自由出現,第二、三個 x是約束出現。沒有變元自由出現的公式稱為閉公式。

  謂詞演算作為一個形式系統,可以規定它的解釋。給定一個論域,對於謂詞演算中出現的個體符號、函數符號及謂詞依次解釋為論域中的個體及定義在此論域上的函數及關系。此論域及其對於謂詞演算中形式符號的解釋稱為該演算的一個結構或模型。由對於個體符號和函數符號的解釋可知,項可解釋為復合函數,它指稱個體。原子公式p(t1t2,…,tn)解釋為t1t2,…,tn所指稱的個體滿足n元關系p。若公式A(x)表示關系,則∀xA(x)解釋為論域中所有個體滿足關系A

x A( x)解釋為論域中存在某個體滿足關系 A

  謂詞演算的推理規則可規定如下:

  

  謂詞演算的邏輯公理陳述邏輯符號的性質,分為三類:

  ① 命題公理 將重言式(見命題邏輯)中出現的命題變元代之以謂詞演算中的任意公式後得到的公式;

  ② 恒同公理x=x及相等性公理

  

  ③ 替換公理Ax[α]→

x A及∀ x AA x[ α],其中 A x[ α]表示將公式 A中所有 x的自由出現代之以項 α

  謂詞演算的公理,即邏輯公理並不界定具體的函數或關系,而僅僅處理邏輯詞項的一般性質。換言之,對它的個體符號、函數符號、及謂詞的解釋可以是任意論域中的任意個體、函數及關系。謂詞演算的這個抽象性質對於近年來模型論的發展是本質的。

  在謂詞演算的框架中,用形式語言表述數學的公理(並不一定能完全表述),就得到不同數學理論的形式系統。這類形式公理刻畫瞭某些具體的非邏輯符號的性質,稱為非邏輯公理。例如:

  全序理論的形式系統中僅有一個非邏輯符號二元謂詞≤。除邏輯公理外,它還有非邏輯公理:①xyyzxz;②xyyxx=y;③xx;④xyyx。自然數集合及其上的順序關系就是全序理論的一個模型。

  群論的形式系統中隻有兩個非邏輯符號:個體符號1及二元函數符號·。它的非邏輯公理為:①x·(y·z)=(x·yz;②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為系統內的公式,x0A中自由出現,則對每個這樣的公式A,有公理

自然數的算術就是它的一個模型。

  陳述在一階語言中,由邏輯公理、非邏輯公理及推理規則推出的全部形式定理(見邏輯演算)稱為一階理論,記為T。為區別不同的一階理論T,隻要指出T的語言中的非邏輯符號及非邏輯公理就夠瞭。任何一階理論都包含瞭謂詞演算作為它的子系統。

  在謂詞演算的任意模型中均為真的公式稱為永真的或有效的公式。例如,公式A(xy)∨¬A(xy)就是有效的公式,而xyyx就不是有效的。因為在全序結構中,對xy在個體域中的任意取值,該公式的解釋均為真。而在半序結構中,例如該結構的論域為一個集合的全體子集的集合,≤解釋為集合的包含關系,那麼上式的解釋當xy取任意的兩個子集時就不都是真的瞭。

  直觀上看,邏輯的定理應當是在一切可能的世界中均為真的定理。在一定意義下,謂詞演算滿足這個性質。可以驗證,謂詞演算的公理均為有效的,它的推理規則的假設有效則結論也必有效。因此,謂詞演算的所有定理都是有效的。這個性質稱為謂詞演算的有效性或可靠性。反之,任意有效的公式必為謂詞演算的定理。這就是著名的哥德爾完備性定理。由K.哥德爾於1930年證明。

  用├A表示A是謂詞演算的形式定理,即A是系統內的定理。而可靠性與完備性刻畫瞭整個形式系統的性質,是關於系統的定理,也稱為元定理。形式系統的性質是數理邏輯主要的研究對象之一。

  由謂詞演算的有效性及完備性容易推知一階理論的可靠性與完備性。使一階理論T的所有公理為真的結構稱為T的一個模型。若T的一個公式AT的任意模型中均有效,稱AT中有效,記為TAAT的定理記為TA。那麼T的可靠性與完備性就可以陳述為TA的充分必要條件為TA

  若不存在A使得TA且├¬A,則稱T是協調的。

  若T是協調的,則T必有模型(廣義完備性定理)。

  形如

x 1 x 2,…, x n B的公式稱為前束型公式,其中 x i表示 x j或∀ x jB是一個不含量詞的公式。任何一個一階理論 T(當 T的非邏輯公理集為空集時就是一個謂詞演算)的公式 A,都有一個公式 A′,使得 TAA′,其中 A′為前束型公式 x 1 x 2,…, x η B,且 B中的非邏輯符號均在 A中出現。 A′也稱為 A的前束范式。此性質可用於對謂詞演算或一階理論的公式進行分類上。此時隻需考慮前束范式中的量詞,將它作為公式復雜性的一種測度。

  

參考書目

 王浩著:《數理邏輯通俗講話》,科學出版社,北京,1981。

 J.R.Schoenfield,MatheMatical Logic,Addison-Wesley,Reading Mass.,1967.