一階理論是一種用一階語言陳述的、並用一階邏輯的規律作為證明工具的形式系統。一階邏輯是不包括非邏輯符號和非邏輯公理的一階理論。
基本介紹
- 中文名：一階理論及其元邏輯
- 領域：數學
定義,形成規則,一階理論的語法研究,一階理論的語義研究,
定義
數理邏輯所研究的一個重要內容。一階理論是一種用一階語言陳述的、並用一階邏輯的規律作為證明工具的形式系統。一階邏輯是不包括非邏輯符號和非邏輯公理的一階理論。其他的一階理論，在其一階語言中包括非邏輯符號，並在公理中包括非邏輯公理。元邏輯是關於形式系統的語法和語義的邏輯研究。
形式算術系統N形式系統、一階理論這些抽象概念，可以從形式算術系統N中得到說明。系統N是自然數算術理論的形式化，建立系統 N所用的一階邏輯是帶等詞(=)的系統。系統N的初始符號有：聯結詞和量詞符號塡，→，凬；等詞符號=；個體變元符號,,,…；個體常元符號 0,1；函式符號+，·；括弧(,)。在初始符號中沒有用到謂詞變元和函式變元，其中個體常元和函式符號是非邏輯符號，其餘的是邏輯符號。
形式算術系統N形式系統、一階理論這些抽象概念，可以從形式算術系統N中得到說明。系統N是自然數算術理論的形式化，建立系統 N所用的一階邏輯是帶等詞(=)的系統。系統N的初始符號有：聯結詞和量詞符號塡，→，凬；等詞符號=；個體變元符號,,,…；個體常元符號 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都是可證明的,就說系統是一致的;否則，系統是不一致的。②研究形式系統的完全性。對於一階邏輯，完全性是指每一普遍有效的公式都是定理；對於其他的一階理論，如果任一閉公式A,或者A是定理,或者塡A是定理,就說系統是完全的;否則,系統是不完全的。③研究判定問題，即確定是否有一種機械方法對系統中的任意一個公式，用它都能機械地在有窮步內確定它是不是定理。通過語法研究所得到的定理叫做語法元定理。元定理不是系統自身之中的定理，而是關於系統的（性質的）定理。
一階理論的語義研究
在形式系統的語法研究過程中，是可以不涉及符號和公式的意義的。但是一個形式系統（形式理論）是一個有內容的理論的形式化。在構造一個形式系統,從而把一個有內容的理論形式化時,選取符號是要讓它們反映被形式化的理論的概念或指稱某種對象的。形成規則關於公式的規定，是要使公式成為被形式化的理論的語句的反映；公理的選擇是要使得它們經解釋後成為被形式化的理論的真語句。即一個形式系統的符號、公式等等是有預想的解釋的，或是從具體理論抽象得來的。一個形式系統可以有不同的解釋，預想的解釋是它的主要的或標準的解釋。關於形式系統的解釋以及關於它的公式的意義的研究是語義研究的基本內容。
對於一階理論T的形式語言L的解釋，由一個非空的論域D和一賦值系υ組成。賦值系包括以下規定：①對每一個體變元，υ都賦與一個D中的元為值,記為。對每一個體常元，在賦值υ下的值是D中的一特定的元。對每一項a，在賦值υ下的值記為a。
② 如 R是一個n元謂詞符號（常元），則R是D中一特定的n元謂詞。
③ 如果ƒ是一個n元函式符號（運算）,則ƒ是D中一特定的n元運算。如果ƒ是n元函式符號，且a,a,…,a是項，則(ƒ(a,a,…,a))=ƒ(a,a…,a)。
④ 對於每一公式A,在賦值υ下的值或者為1（真）或者為0(假), 即A的值是1或0；如果A為原子公式R(a,…,a), (a,…,a) 所賦之值〈a,…,a〉屬於R所賦之值 R，則(R(a,…,a))之值為1，否則為0。(塡A)之值為1，若且唯若A之值為0；(A凮B)之值為1；若且唯若A之值為0或B之值為1；((凬)A)之值為 1, 若且唯若設A的賦值已經給定，用D中的每一個體替代A中的時，A的值均為1 。在一階理論T中，由於被斷定的開公式如
一階理論及其元邏輯
一階理論及其元邏輯
一階理論及其元邏輯一階理論及其元邏輯 一階理論及其元邏輯
對於一階理論T的形式語言L的解釋，由一個非空的論域D和一賦值系υ組成。賦值系包括以下規定：①對每一個體變元，υ都賦與一個D中的元為值,記為。對每一個體常元，在賦值υ下的值是D中的一特定的元。對每一項a，在賦值υ下的值記為a。
② 如 R是一個n元謂詞符號（常元），則R是D中一特定的n元謂詞。
③ 如果ƒ是一個n元函式符號（運算）,則ƒ是D中一特定的n元運算。如果ƒ是n元函式符號，且a,a,…,a是項，則(ƒ(a,a,…,a))=ƒ(a,a…,a)。
④ 對於每一公式A,在賦值υ下的值或者為1（真）或者為0(假), 即A的值是1或0；如果A為原子公式R(a,…,a), (a,…,a) 所賦之值〈a,…,a〉屬於R所賦之值 R，則(R(a,…,a))之值為1，否則為0。(塡A)之值為1，若且唯若A之值為0；(A凮B)之值為1；若且唯若A之值為0或B之值為1；((凬)A)之值為 1, 若且唯若設A的賦值已經給定，用D中的每一個體替代A中的時，A的值均為1 。在一階理論T中，由於被斷定的開公式如
一階理論及其元邏輯一階理論及其元邏輯一階理論及其元邏輯一階理論及其元邏輯一階理論及其元邏輯x+y=y+x
和其閉公式
(凬x)(凬y)(x+y =y +x)
可以互相推導，其真假亦相同。因之在探究其值時，可以只考慮閉公式。設 A是理論T的一個閉公式，I是在論域M中對T的一個解釋。在此解釋下，A成為關於M的一個或真或假的語句 A。如 A在 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不可能都是可證的。
③ 完全性定理。凡重言式都是定理，命題演算的每一公式都可變換成一個與之等值的合取範式，每一個重言的合取範式,都可以從可證公式∨塡,→∨,→(→∧),套用分離規則推演出來，即是可證明的。因此，變換成合取範式的原來那個公式是可證明的，即是定理。
④ 命題演算是可判定的。對於任一公式 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不可滿足，即停機問題可以歸約到一階邏輯的判定問題。因此，如果一階邏輯公式的普遍有效性（可滿足性）是可判定的，則停機問題是可解的。但這與停機問題不可解的結果相矛盾，因之一階邏輯公式的判定問題也是不可解的。除了這個一般性的結果，還有一階邏輯公式集的子集的判定問題。這通常是用前束範式對公式分類。關於這種分類的判定問題，在下述意義下已幾乎完全解決了，即每個前束類或者是可判定的或者是歸約類（不可判定的）。這方面的一個重要結果是,具有形式凬ヨ凬A(,,)的公式,其中僅包含若干二元謂詞或一個二元謂詞加上若干一元謂詞構成了一個關於可滿足性的歸約類。另外，只包含一元謂詞的公式類是可判定的。
形式系統 N的標準解釋，是取自然數域為論域，個體常元 0和1分別解釋為自然數域中的 0和1，函式符號+與·解釋為通常的加和乘。
真、假、賦值、可滿足性、模型等等都是語義概念。從語義學考慮，一個形式系統如果至少有一個模型，那末它就是一致的，如果每一真的公式都是可證明的，該形式系統就是完全的。對於判定問題，就是研究是否有一種機械的方法，能判定任意公式是不是真的。
元邏輯也研究語法和語義之間的關係。例如語法概念可證性和語義概念真理性，在20世紀30年代以前的數學中一般都是相混同的，K.哥德爾和A.塔爾斯基在元邏輯方面的工作證明，真理性是不能等同於可證性的。
元邏輯的一些重要結果 元邏輯在命題演算、一階邏輯以及一階數學理論等方面已有若干重要的結果。命題演算的元邏輯結果有：①可靠性定理。根據這條定理，命題演算的定理都是重言式即常真的。
② 一致性定理。命題演算是一致的，對任一公式A及其否定塡A,若其一是重言式,則另一必是常假的。根據可靠性定理，A和塡A不可能都是可證的。
③ 完全性定理。凡重言式都是定理，命題演算的每一公式都可變換成一個與之等值的合取範式，每一個重言的合取範式,都可以從可證公式∨塡,→∨,→(→∧),套用分離規則推演出來，即是可證明的。因此，變換成合取範式的原來那個公式是可證明的，即是定理。
④ 命題演算是可判定的。對於任一公式 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不可滿足，即停機問題可以歸約到一階邏輯的判定問題。因此，如果一階邏輯公式的普遍有效性（可滿足性）是可判定的，則停機問題是可解的。但這與停機問題不可解的結果相矛盾，因之一階邏輯公式的判定問題也是不可解的。除了這個一般性的結果，還有一階邏輯公式集的子集的判定問題。這通常是用前束範式對公式分類。關於這種分類的判定問題，在下述意義下已幾乎完全解決了，即每個前束類或者是可判定的或者是歸約類（不可判定的）。這方面的一個重要結果是,具有形式凬ヨ凬A(,,)的公式,其中僅包含若干二元謂詞或一個二元謂詞加上若干一元謂詞構成了一個關於可滿足性的歸約類。另外，只包含一元謂詞的公式類是可判定的。
