一階理論及其元邏輯
正文
數理邏輯所研究的一個重要內容。一階理論是一種用一階語言陳述的、並用一階邏輯的規律作為證明工具的形式系統。一階邏輯是不包括非邏輯符號和非邏輯公理的一階理論。其他的一階理論，在其一階語言中包括非邏輯符號，並在公理中包括非邏輯公理。元邏輯是關於形式系統的語法和語義的邏輯研究。形式算術系統N 形式系統、一階理論這些抽象概念，可以從形式算術系統N中得到說明。系統N是自然數算術理論的形式化，建立系統 N所用的一階邏輯是帶等詞(=)的系統。系統N的初始符號有：聯結詞和量詞符號塡，→，凬；等詞符號=；個體變元符號x,y,z,…；個體常元符號 0,1；函式符號+，·；括弧(,)。在初始符號中沒有用到謂詞變元和函式變元，其中個體常元和函式符號是非邏輯符號，其餘的是邏輯符號。
系統 N的形成規則有項形成規則和公式的形成規則兩類。項形成規則：①一個體常元是一項，一個體變元是一項；②如果a,b是項，則a+b和a·b是項；③只有適合①和②兩條的是項。公式的形成規則：①如 a,b是項，則a=b是公式，稱為原子公式；②如果A,B是公式,α是一個體變元，則塡A,A→B,(凬α)A(α)是公式；③只有適合①、②兩條的是公式。在這些形成規則中出現的符號a,b,A,B和α，不是系統N中的符號，而是描述或陳述系統N時所使用的另一個稱為元語言中的符號。a，b表示任一項，α表示任一個體變元，A,B表示任一公式。這些符號稱為語法變元。A(α)表示α在A中出現（也可以不出現）。
一個量詞的轄域指這量詞後的最短公式，表示量詞在一個公式中的作用範圍。一個體變元α在一公式A中的某次出現是約束出現，如果α的這次出現是在(凬α)中或(凬α)的轄域中,一個體變元α在一公式A中某次出現是自由出現，如果α在A中的這次出現不是約束的，例如，在公式(凬y)((凬x)F(x)→F(y))中，量詞(凬y)的轄域是(凬x)F(x)→F(y)，(凬x)的轄域是F(x)，x和y在(凬y)((凬x)F(x)→F(y))中的兩次出現都是約束的。在公式(凬x)F(x)→F(y)中,x兩次出現是約束的,y的唯一一次出現則是自由的。個體變元α在A中可以既有約束出現又有自由出現，例如(凬x)F(x)→F(x)。個體變元α在A中是自由(約束)的,如果它在A中有自由（約束）出現。不含有自由 (個體)變元的公式稱為閉公式。
系統 N的公理：
A1,A→(B→A)；
A2,(A→(B→C))→((A→B)→(A→C))；
A3,(塡A→塡B)→((塡A→B)→A)；
A4,(凬α)(A→B)→(A→(凬α)B),
其中α在A中沒有自由出現；
A5,(凬α)→A(a),
其中A(α)是公式，a是項,並且a對於在A(α)中的α是自由的，即：如果β 是項a中的一個體變元，那末α在A(α)中的自由出現都不在(凬β)的轄域之中；
A6,α=α；
A7,α1=β1→(α2=β2→…(αn=βn(→(A(α1,α2,…αn
→A(β1,β2,…,βn)))…)；
N1,塡(α+1=0)；
N2,α+1=β+1→α=β；
N3,α+0=α；
N4,α+(β+1)=(α+β)+1；
N5,α·0=0；
N6,α·(β+1)=α·β+α。
A1～A7是一般的邏輯公理，其中A6～A7是關於等詞的公理；N1～N6是非邏輯公理，或者說是系統 N的特有的公理。這些公理都是用語法變元陳述的，是一些公理模式，而不是單個公理。每一公理模式都代表無窮條公理，如根據A6,x=x,y=y,z=z等等都是公理。用公理模式陳述公理，是為了在推理規則中可以不用代入規則。
系統N的推理規則或稱變形規則為：
R1，分離規則，從A和A→B可以推出B；
R2，概括規則，從A(α)可以推出(凬α)A(α)；
R3，數學歸納原則,從A(0)和(凬α)(A(α)→A(α+1))可以推出(凬α)A(α)，
其中R1、R2是一階邏輯的規則，R3是 N中特有的規則。
所謂定理是指從公理套用推理規則推演出來的公式，或者說，是有證明的公式。一個證明是公式的有窮序列，其中每一公式或者是公理或者是從序列中前面的公式套用推理規則得出的。一個證明也說是它的最後公式的證明。
系統 N滿足關於形式系統的下述要求：任給一符號，能夠機械地檢查它是不是 N中的符號；任給一符號的組合，能夠機械地檢查它是不是 N的一公式；任給一公式可以機械地檢查它是不是 N的一個公理；給定一有窮的公式序列，能夠機械地檢查它是不是 N中的一個正確的證明。
一階理論的語法研究 元邏輯對形式系統的研究包括語法的和語義的兩個方面。形式系統包括形式語言(符號、形成規則)、公理和推理規則三部分。如果只涉及符號、符號組合、公式序列的形狀,公式的變形,就是語法方面的研究，叫做語法學。語法研究的一個重要概念是可證明性，即一個公式是不是在系統中可證明的，是不是系統中的定理。語法學研究形式系統的以下幾個重要性質：①研究形式系統的一致性。其結果為：如果不是每一公式都是可證明的,或者不存在一個公式A，A和塡A都是可證明的,就說系統是一致的;否則，系統是不一致的。②研究形式系統的完全性。對於一階邏輯，完全性是指每一普遍有效的公式都是定理；對於其他的一階理論，如果任一閉公式A,或者A是定理,或者塡A是定理,就說系統是完全的;否則,系統是不完全的。③研究判定問題，即確定是否有一種機械方法對系統中的任意一個公式，用它都能機械地在有窮步內確定它是不是定理。通過語法研究所得到的定理叫做語法元定理。元定理不是系統自身之中的定理，而是關於系統的（性質的）定理。
一階理論的語義研究 在形式系統的語法研究過程中，是可以不涉及符號和公式的意義的。但是一個形式系統（形式理論）是一個有內容的理論的形式化。在構造一個形式系統,從而把一個有內容的理論形式化時,選取符號是要讓它們反映被形式化的理論的概念或指稱某種對象的。形成規則關於公式的規定，是要使公式成為被形式化的理論的語句的反映；公理的選擇是要使得它們經解釋後成為被形式化的理論的真語句。即一個形式系統的符號、公式等等是有預想的解釋的，或是從具體理論抽象得來的。一個形式系統可以有不同的解釋，預想的解釋是它的主要的或標準的解釋。關於形式系統的解釋以及關於它的公式的意義的研究是語義研究的基本內容。
對於一階理論T的形式語言L的解釋，由一個非空的論域D和一賦值系υ組成。賦值系包括以下規定：①對每一個體變元x，υ都賦與一個D中的元為值,記為xυ。對每一個體常元，在賦值υ下的值是D中的一特定的元。對每一項a，在賦值υ下的值記為aυ。
② 如 R是一個n元謂詞符號（常元），則Rυ是D中一特定的n元謂詞。
③ 如果ƒ是一個n元函式符號（運算）,則ƒυ是D中一特定的n元運算。如果ƒ是n元函式符號，且a1,a2,…,an是項，則(ƒ(a1,a2,…,an))υ=ƒυ(a
,a
…,a
)。 ④ 對於每一公式A,在賦值υ下的值或者為1（真）或者為0(假), 即Aυ的值是1或0；如果A為原子公式R(a1,…,an), (a1,…,an) 所賦之值〈a
,…,a〉屬於R所賦之值 Rυ，則(R(a1,…,an))之值為1，否則為0。(塡A)υ之值為1，若且唯若Aυ之值為0；(A凮B)υ之值為1；若且唯若Aυ之值為0或B之值為1；((凬)Ax)υ之值為 1, 若且唯若設A的賦值已經給定，用D中的每一個體替代A中的x時，A的值均為1 。在一階理論T中，由於被斷定的開公式如 x+y=y+x
和其閉公式(凬x)(凬y)(x+y =y +x)
可以互相推導，其真假亦相同。因之在探究其值時，可以只考慮閉公式。設 A是理論T的一個閉公式，I是在論域M中對T的一個解釋。在此解釋下，A成為關於M的一個或真或假的語句 AI。如 AI在 M中為真，則稱〈M,I〉為A 的一個模型。設∑為理論 T的一個閉公式集，〈M,I〉是∑的模型,若且唯若〈M,I〉是∑中每一公式的模型。如〈M,I〉是理論T的公理集的模型,則稱〈M,I〉為理論T的模型。一組有模型的公式又稱為可滿足的。形式系統 N的標準解釋，是取自然數域為論域，個體常元 0和1分別解釋為自然數域中的 0和1，函式符號+與·解釋為通常的加和乘。
真、假、賦值、可滿足性、模型等等都是語義概念。從語義學考慮，一個形式系統如果至少有一個模型，那末它就是一致的，如果每一真的公式都是可證明的，該形式系統就是完全的。對於判定問題，就是研究是否有一種機械的方法，能判定任意公式是不是真的。
元邏輯也研究語法和語義之間的關係。例如語法概念可證性和語義概念真理性，在20世紀30年代以前的數學中一般都是相混同的，K.哥德爾和A.塔爾斯基在元邏輯方面的工作證明，真理性是不能等同於可證性的。
元邏輯的一些重要結果 元邏輯在命題演算、一階邏輯以及一階數學理論等方面已有若干重要的結果。命題演算的元邏輯結果有：①可靠性定理。根據這條定理，命題演算的定理都是重言式即常真的。
② 一致性定理。命題演算是一致的，對任一公式A及其否定塡A,若其一是重言式,則另一必是常假的。根據可靠性定理，A和塡A不可能都是可證的。
③ 完全性定理。凡重言式都是定理，命題演算的每一公式都可變換成一個與之等值的合取範式，每一個重言的合取範式,都可以從可證公式p∨塡p,p→p∨q,p→(q→p∧q),套用分離規則推演出來，即是可證明的。因此，變換成合取範式的原來那個公式是可證明的，即是定理。
④ 命題演算是可判定的。對於任一公式 A是否為重言式，是不是定理，都是可判定的。用真值表方法或求合取範式的方法，都能機械地在有窮步內判定一公式是否為重言式，因而是不是定理。
命題演算的重要元邏輯問題，可以說都已得到肯定的解決，留下的一個新的有興趣的問題是尋找判定一公式是否為重言式的快速判定方法。
關於一階邏輯的重要的元邏輯結果有：①可靠性定理，即凡定理都是普遍有效的。
② 一致性定理。一階邏輯是一致的。若取只有一個個體a的集為論域，凬αA(α)即為A(a)，而所有量詞全部消去。於是，所有的公式都可看作是命題演算的公式。因此，對任一公式A，不可能A和塡A都可證。
③ 完全性定理。一階邏輯在語義意義下是完全的，即凡普遍有效的公式都是定理。完全性定理還有一個更強的形式，即每一一致的公式集都有模型，都是可滿足的。這一更強形式的完全性定理也稱強完全性。根據完全性定理，如果塡A不是定理，則塡A不普遍有效，因此，A是可滿足的。說一公式A是一致的,即從A不可能推出兩個矛盾的公式， 不外是意謂塡A不是定理。所以，如果A是一致的，那末A是可滿足的。這樣，對於一階邏輯來說，語義概念的普遍有效性、可滿足性，與語法概念的可證性和一致性，是相互符合的。
④ 緊緻性定理。一個公式集г是有模型的,若且唯若它的每一有窮子集是有模型的。根據一個比較容易證明的定理，公式集г是一致的,若且唯若它的每一有窮子集是一致的。緊緻性定理能直接從完全性定理推出。
⑤ 勒文海姆-司寇倫定理,簡稱LS定理。該定理表明,如一公式或一公式集有模型,則它有一可數模型。LS定理是L.勒文海姆、T.司寇倫證明的。從哥德爾對完全性定理的原來證明能直接推出LS定理。LS定理還有由塔爾斯基改進了的形式。LS定理的直接證明方法，為模型論以及集合論中相對一致性和獨立性的證明，提供了一個非常有用的工具。緊緻性定理和LS定理是模型論的基礎性定理。
⑥ 判定問題的結果。A.圖林和A.丘奇在1936年分別證明了一階邏輯是不可判定的，即不存在判定一個一階邏輯的公式是否普遍有效（可滿足）或是否可證的機械方法。圖林證明，圖林機的停機問題，即任一圖林機從空白帶開始計算是否最後停機是不解的（見圖林機器理論）。他又證明對於一台圖林機T是否停機的問題,可用一階邏輯的一個公式 A表達，使得T停機若且唯若A不可滿足，即停機問題可以歸約到一階邏輯的判定問題。因此，如果一階邏輯公式的普遍有效性（可滿足性）是可判定的，則停機問題是可解的。但這與停機問題不可解的結果相矛盾，因之一階邏輯公式的判定問題也是不可解的。除了這個一般性的結果，還有一階邏輯公式集的子集的判定問題。這通常是用前束範式對公式分類。關於這種分類的判定問題，在下述意義下已幾乎完全解決了，即每個前束類或者是可判定的或者是歸約類（不可判定的）。這方面的一個重要結果是,具有形式凬xヨu凬yA(x,u,y)的公式,其中僅包含若干二元謂詞或一個二元謂詞加上若干一元謂詞構成了一個關於可滿足性的歸約類。另外，只包含一元謂詞的公式類是可判定的。
關於形式數學系統，有如下幾個結果：①最早證明並且也是最重要的結果是哥德爾在1931年證明的兩個不完全性定理。第一個不完全性定理為：一個滿足條件①一致的，②適當豐富，即足以展開一個適量的自然數算術理論的形式系統S，是不完全的。例如，系統N是不完全的。在這樣的系統 S中，存在不可判定的語句，即不包含自由個體變元的閉公式 A，A和塡A都是不可證明的。經解釋後，根據排中律A與塡A二者之中必有一真，因此，在 S中有一真的但不可證明的語句。並且這樣的形式系統 S是不可能完全的，即如果把一個原來不可證的公式作為公理加到 S中，則在新的系統中總又可以構造出另一個閉公式，而且這個閉公式及其否定在這新的系統中都是不可證的。從這個定理還能推得，系統 S的真語句集是不能在 S中定義的，第一個不完全性定理顯示了形式系統的固有局限性，表明一個內容豐富的理論是不能完全形式化的。第二個不完全性定理表明，滿足上述條件①、②的形式系統S的一致性，是不能在系統S自身中證明的。它同時還表明，D.希爾伯特所提出的證明古典數學一致性的方案是不能實現的。
② 關於一致性的結果。W.阿克曼於1924年證明對數學歸納原則加以限制的經典數論的形式系統是一致的。在這方面，最著名的結果是G.根岑於1936年證明經典數論系統 N是一致的。根岑在證明中，放寬了希爾伯特對元邏輯研究所用方法的限制,使用了超窮歸納,超窮歸納是不能在系統 N中形式化的。一致性問題研究的另一個方向，是研究經典數論與直覺主義數論之間的關係。哥德爾在1933年找到了經典數論在直覺主義數論中的一個解釋。因此，如果直覺主義數論是一致的，則經典數論也是一致的。哥德爾還在1958年發表了另一個結果，即套用原始遞歸泛函得到了經典數論語句的一個構造性解釋。
③ 關於判定問題的結果。這類結果包括可判定性的和不可判定性兩個方面。關於可判定性的結果有：M.普拉斯伯格證明只有一個加法運算的自然數算術理論是可判定的；塔爾斯基證明初等代數和初等幾何是可判定的。不可判定性的結果有：象 N這樣的系統的真語句集是不可判定的，沒有判定一個語句是否真的機械方法。在象N 這樣的系統中，一切遞歸的或可判定的函式和謂詞都是可表示的，而系統的語言中的謂詞“真”卻不是在系統中可表示的或可定義的，因此，它也不是遞歸的或可判定的。一個著名的結果是,Ю.В.馬季亞謝維奇在1970年證明，希爾伯特第10個問題是不可解的，即丟番圖方程p(x1,…,xn)=0是否有整數解是不可判定的。
