fbpx
维基百科

一阶逻辑

一阶逻辑是使用於数学哲学语言学電腦科學中的一种形式系统,也可以稱為:一阶斷言演算低階斷言演算量化理論谓词逻辑。一階邏輯和命題邏輯的不同之處在於,一階邏輯包含量詞

高階邏輯和一階邏輯不同之處在於,高階邏輯的斷言符號可以有斷言符號或函數符號當做引數,且容許斷言量詞或函數量詞[1]。在一階邏輯的語義中,斷言被解釋為關係。而高階邏輯的語義裡,斷言則會被解釋為集合的集合。

在通常的語義下,一階邏輯是可靠(所有可證的敘述皆為真)且完備(所有為真的敘述皆可證)的。雖然一階邏輯的邏輯歸結只是半可判定性的,但還是有許多用於一階邏輯上的自動定理證明。一階邏輯也符合一些使其能通過證明論分析的元邏輯定理,如勒文海姆–斯科倫定理緊緻性定理

一階邏輯是數學基礎中很重要的一部份。許多常見的公理系統,如一階皮亞諾公理冯诺伊曼-博内斯-哥德尔集合论策梅洛-弗蘭克爾集合論都是一階理論。然而一階邏輯不能控制其無窮模型的基數大小,因根據勒文海姆–斯科倫定理和康托爾定理,可以構造出一種“病態”集合論模型,使整個模型可數,但模型內卻會覺得自己有「不可數集」。類似地,可以證明實數系的普通一階理論既有可數模型又有不可數模型。這類的悖論被稱為斯科倫悖論。但一階的直覺主義邏輯裡,勒文海姆–斯科倫定理不可證明[2],故不會有以上之現象。

簡介

在命題邏輯裡,「蘇格拉底是哲學家」、「柏拉圖是哲學家」只能簡單標記為   

而一階邏輯先设符號   意為 「 x 是哲學家」,然後以   代表蘇格拉底、   代表柏拉圖,則   對應    對應   。也就是賦予斷言符號 語意的解釋。這個解釋預設一個「所有人類的群體」(也就是語義解釋的論域),并將變數   解釋為自群體中取出來的某人。

斷言符號可以包含一個以上的變數。例如:设   意為「 x 與 y 是夫妻」,则   意为「蘇格拉底和 y 是夫妻」。

一階邏輯和命題邏輯相同,斷言符號和變數還能與邏輯符號組成更複雜的敘述。例如:设斷言符號   意為   是學者。則「若 x 為哲學家,則 x 為學者」可表示為:

 

而「對所有 x ,若 x 為哲學家,則 x 為學者」則記為:

 

也就是自左方開始閱讀,以   表示「对于所有 x 」,可以將之理解為「对于所有 x  右方的敘述為真。」其中,  這個符號被称为  全稱量詞

直觀上有「若所有x是哲學家,那x的長子也會是哲學家」這樣“合理”的敘述。若设   意為 「 x 的長子」,那么這段“合理”敘述可記為:

 

  表示“與   有唯一對應的那個對象”,被稱為函數符號。這段直觀為真的敘述,經過適當的擴展以後就是一階邏輯其中的一條公理

而對於「有 x 是哲學家」这一叙述,則引入另一種量詞表記為:

 

自左方開始閱讀,以   代表「存在 x 」,可以將之理解為「有 x 使   右方的敘述為真」。其中,  被稱為  存在量詞。全稱量詞和存在量詞一起被簡稱為量詞

直觀上,「並非所有 x 不是哲學家」,和「有 x 是哲學家」是等價的;且「不存在 x 不是學者」也与「所有的 x 是學者」等價。所以只要有「否定」這個邏輯概念,那么一階邏輯就能以全稱量詞為基礎,作以下的符號定義(   解釋為 「否定」, 而   代表一段"敘述"):

 

由此,存在量詞被定義為全稱量詞的衍伸。

形式理論

一階邏輯的形式理論可分成幾個部份:

  1. 語法英语Syntax (logic):決定哪些符號組合是合式公式。(直觀上的“文法無誤的敘述”)
  2. 推理規則:由合式公式符號組合出新合式公式的規則(直觀上的“推理”)
  3. 公理:一套合式公式(直觀上的基本假設)

基本符號

一套理論能容許多少符號,取決於人類根据物理定律能塑造多少符號。但以目前無法確知宇宙是不是有限,或是是否可無限制分割。雖然所有的公理化集合論都以量詞的形式隱晦的承認無窮的存在(如ZF集合論的無窮公理),甚至以這樣自然數意義上的無窮為基礎,去建構出不可數的實數。但將之對應到現實,還是會回到同樣的物理問題。

謹慎起見,以下各種類的符號沒有特別聲明,數量將會是有限個。

邏輯符號

詞彙表中存在若干個邏輯符號,通常包括:

  1. 量化符號   
    • 某些作者[3]會把   符號定義為  ,如此便只需要   做為基礎符號。
  2. 邏輯聯結詞:以下為可能的表示符號(关于波蘭表示法下的邏輯連接詞,請參見逻辑运算的波兰记法):
    • 否定  
    • 條件   
    •   
    •  ||
    • 雙條件  
    • 某些作者[4]會作如下的符號定義:
     
     
     
    如此一來只需要否定條件做為基礎符號。
  3. 標點符號:括號、逗號及其他,依作者的喜好有所不同。
    • 為了更有效的將括號做配對,通常還會採用大括號{ }中括號[ ]
  4. 至多跟自然數一樣多的變數,通常標記為英文字母末端的小寫字母xyz、…,也常會使用下標(或上標、上下標兼有)來區別不同的變數:x0x1x2、…(特別注意c有時候會被當成常數符號而引起混淆)。
  5. 等式符號: 
    • 有作者會因為語義上对“相等”的不同解释,而將等式符號視為雙元斷言符號、甚至是某種合式公式的簡寫。
  6. 符號相等: 
    • 為了將符號辨識上区别等同和等式符號,某些作者[5]會額外採用這個符號。

注意:並非所有的符號都是必需的。比如,在比較極端的情况中,因为謝費爾豎線(或異或)的布林代數完備性使得所有不含量詞的邏輯公理都可以用謝費爾豎線表述,而大幅減少基礎的邏輯聯結詞。

另外,一些作者並沒有將語義學形式理論劃分清楚,而會將真值常數納入符號的一環:用 T 、Vpq  來表示「真」,並用 F 、 Opq  來表示「假」。

斷言符號

「他們兩人是夫妻」,是一個關於兩個“對象”的斷言,而「他是人」、「三點共線」则表明斷言容許一個或者多個對象。所以對於自然數    約定:

 

為一階邏輯的合法詞彙。它在直觀上表示一個有   個“對象”的斷言,稱為   元斷言符號。下標的自然數   只是拿來和其他同為   元的斷言符號作區別。

實用上只要有申明,不至於和其他詞彙引起混淆的話,可以用任意的形式簡寫一個斷言符號。如:公理化集合論裡的雙元斷言符號   也可以表示为  

函數符號

「物體的顏色」、「夫妻的長子」这种断言說明了一组對象所唯一對應的對象。但不同的夫妻有不同的長子;不同的物體有不同的顏色。據此,形式上對於自然數    約定:

 

為一階邏輯的合法詞彙,直觀上表示   個“對象”所對應到的東西,稱它為   元函數符號需要特別注意,這種“唯一對應”的直觀想法,必須配上關於“等式”的性質(詳見下面的等式定理章节),才能在形式理論中被實現。

与斷言符號一样,只要不引起混淆,就可以用任何的形式簡寫函數符號。如:公理化集合論裡的   是依據聯集公理而定義的新函數符號(請參見下面函數符號與唯一性章節),也可以冗長的表記為  

常數符號

「刻度0」、「原點」、「蘇格拉底」是直觀上"唯一不變"的對象。據此,對自然數   約定

 

為一階邏輯的合法詞彙,直觀上表示一個“唯一不變”的對象,稱為常數符號。同樣的。“常數的不變性”需配上等式的性質(詳見下面等式定理)才能被實現。

為了不和變數的表記混淆,常數符號一樣可以用任何的形式簡寫,如公理化集合論裡的   是根據空集公理函數符號與唯一性,而定義的新常數符號。亦可冗長的表示為  

語法

和自然語言(如英語)不同,一階邏輯的語言以明確的遞迴定義判斷一個給定的詞彙是否合法。大致上來說,一階邏輯以「項」代表討論的對象,而對「項」的斷言組成了最基本的原子(合式)公式;而原子公式和邏輯符號組成了更複雜的合式公式(也就是“敘述”)。

「那對夫妻的長子的職業」、「 」、「 」代表變數可以與函數符號組成更一般的物件。據此形式,遞迴地規定一類合法詞彙——為:

  1. 變數常數是項。
  2.   全都是項,那么   也是項。
  3. 項只能通过以上兩點,於有限步驟內建構出來。

習慣上以大寫的西方字母(如英文字母、希伯來字母、希臘字母)代表項,如果變數不得不採用大寫字母,而可能跟項引起混淆的話,需額外規定分辨的辦法。

原子公式

為了比較簡潔地規定甚麼是合式公式,先規定原子公式為:(若   是項)

 

這樣的形式。

公式

一階邏輯的合式公式(簡稱公式或   )以下面的規則遞迴地定義:

  1. 原子公式為公式。(美觀起見,在原子公式外面包一層括弧也是公式)
  2.   為公式,則   為公式。
  3.    為公式,則   為公式。
  4.   為公式,   為任意變數,則   為公式。 (美觀起見  ,也就是裡面的量詞有無外包括弧都是公式)
  5. 合式公式只能通过以上四點,於有限步驟內建構出來。

另外成對的中括弧跟大括弧,符號辨識上視為成對的小括弧,而草書的大寫西方字母為公式的代號。

舉例來說,

 

是公式而

 

則不是公式。

而接下來只要對任意公式   與變數  ,做以下符號定義

 

 

 

  (同樣美觀起見  

這樣所有的邏輯連接詞與量詞就納入了合式公式的規範。

施用

所謂的施用/作用,是以下公式形式的口語說法:(其中    都是公式)

  •   稱為   施用於   上。
  •   稱為   施用於    上。
  •   稱為   施用於    上。
  •   稱為   施用於    上。
  •   稱為   施用於    上。
  •   稱為   施用於   上。
  •   稱為   施用於   上。

就类似于運算子作用在它們身上。

自由變數和約束變數

量詞所施用的公式被稱為量詞的範圍(scope)。同一個變數在公式一般來說不只出現一次,若變數   出現在   的範圍內,稱這樣出現的  不自由/被約束的   (not free/bounded);反過來說,不出現在   的範圍內的某個   被稱為自由的  

例如,對於公式:

 

  就是量詞   的範圍;而   裡的   就是不自由的;反之   裡的   就是自由的。

  於公式   完全自由,意為於   出現的   都是自由的;反之,說   於公式   完全不自由/完全被約束,意為   內根本沒有   ,或是   內沒有自由的   。若   內所有的變數都完全不自由,  特稱為封閉公式/句子(closed formula/sentence)。

括弧的簡寫

括弧是為了保證語意解釋符合預期,但太多的括弧書寫不易,為此規定以下的“重構法”(反過來就是“簡寫法”),從表面上不合法的一串符號找出作者原來想表達的公式:

  • 若整串符號的括弧不成對,直接視為無法重構
  •  (左至右)的施用順序重構括弧。
  • 相鄰的邏輯連接詞或量詞無法決定施用順序的話,以右邊為先。
  • 重構施用的順序,以被成對括弧包住的部分為優先施用,其次才是落單的斷言符號。

舉例來說

 

的重構過程如下

  1.   (優先施用  
  2.   (施用  
  3.   (最後施用  

可以被重構為公式的一串符號則寬鬆的認定為“合式公式”。(最明顯的例子就是合式公式最外層的括弧可以省略)

波蘭表示法

波蘭表示法將邏輯連接詞前置於被施用的公式而非傳統的中間。如果沿用以上的"施用順序",這個表示法允許捨棄所有括弧。如公式

 

轉成波蘭表示法的過程如下

  (轉成波蘭表示法的順序)
  (邏輯連結詞的符號轉換)

推理规则

MP律

對於公式   

   組合出  

直觀意義非常明顯,就是p=>qp可以推出q

公理

邏輯公理

如果   都是公式,則:

  • (A1)  
  • (A2)  
  • (A3)  

都是公理。

它们实际上是公理模式,代表著“跟自然數一樣多”條的公理。

量词公理

以下的   為任意變數,    為任意公式。

  • (A4)   是一個項,    中出現的任意變數;若   裡,所有   的的範圍裡都沒有自由的   (這個情況稱為   裡項    是自由的),則
 
為公理
其中   代表把   裡自由的   都取代為   所得到的新公式。
  • (A5)如果    裡完全被約束,則
 
為公理
  • (A6)   為公理
  • (A7) 若   是公理,   是任意變數,則
 
也是公理。

它们实际上是公理模式

等式和它的公理

根據不同作者的看法,甚至是理論本身的需求,「等式」在形式理論裡可能是斷言符號或是一段公式(如 a 等於 b 可定義為對所有的 xx 屬於 a 等價於 x 屬於 b )。而如何刻劃直觀上「等式的性質」,有一開始就將「等式的性質」視為公理(模式),但也有視為元定理的另一套處理方法,以下暫且以公理模式的方式處理。以元定理處理的方法會在等式定理詳述。

  是一段變數    完全自由,且型式完全被確定的公式   的簡寫。要求:

  • (E1) 對任意變數    為公理。
  • (E2) 對於任意變數   ,若在公式   中自由的   都不在   的範圍內。若以  代表   某些(而非全部)自由的   被取代成   而成的新公式,則
 
為公理。

事實上這兩個公理模式也確保了函數符號“唯一對應”和常數符號的“唯一性”,但證明這些性質需要一些元定理,簡便起見合併於下面的等式定理一節講述。

標準語義

一階邏輯的標準語義源於波蘭邏輯學家阿尔弗雷德·塔斯基所著《On the Concept of Truth in Formal Languages》。根據上面語法一節,公式是由原子公式遞迴地添加邏輯連結詞而來的,而原子公式是由斷言符號與項所構成的。所以要檢驗一條公式在特定的論域下正不正確,就要規定項的取值,然後檢驗這樣的取值會不會落在斷言符號所對應的關係裡。由此延伸出所有公式的“真假值“。

也就是一套一階邏輯的語義解釋,要包含

  1. 變數取值的論域
  2. 如何解釋函數符號(為論域中的某個函數)與常數符號(為論域中的某特定元素),以便從特定的變數取值得出項的取值。
  3. 如何將斷言符號與論域裡的某關係做對應。

通常一套解釋方法(簡稱為解釋)會以代號   表示。

項的取值

量詞的解釋需要指明變數取值範圍的論域——也就是一個集合   。而變數可能跟自然數一樣多,換句話說,所有變數在論域   取的值可以依序以自然數標下標——也就是一個在   取值的數列。如果以   的代號(不一定是變數本身的表示符號)來列舉變數,那麼從   的某套變數取值就以

 

或較直觀的符號

 

來表示。

一套解釋   會將   元函數符號   解釋成某個   函數;而常數符號   解釋成特定的   (亦稱為   的取值為  ),這樣就可以用上面語法一節定義項的方式,遞迴地規定項的取值

在解釋   下的某套變數取值下,一列項   的取值分別為  ,則這套變數取值下,項   的取值規定為

 

真假的賦值

直觀上要解釋關係最直接的方法,就是列舉所有符合關係的對象;例如如果想說明夫妻關係,可以列舉所有(老公, 老婆)的雙元有序對,但並非所有的人類有序對都會在這個關係中。

以此為基礎,若以   代表所有以    中的元素構成的   元有序對的集合(也就是  笛卡兒積) ,那一套解釋   會將   元斷言符號   解釋為一個

 

 有序對子集合。

這樣就可以依據語法的遞迴定義,以下面的規則對每條公式賦予真值。(這種賦值方式稱為T-模式,取名於邏輯學家阿尔弗雷德·塔斯基)

在一套解釋   下:

  • 在一套特定的變數取值下,一列項   的取值為   ,那   為真定義為
 
反之
 
則定義為假。
  • 在一套特定的變數取值下,「  為真」 等價於 「  為假」。
  • 在一套特定的變數取值下,  為真,意為「   為假或是   為真。」 (p=>q為假只有p為真且q為假的狀況)
  • 在變數取值   下,  為真,意為「對所有的    於變數取值   下為真」。(也就是把變數   的取值換為論域的任意元素仍然為真)

更進一步的來說

  1. 在一套解釋   下,不管怎麼樣的變數取值,公式   都為真,則稱為    為真,以符號   簡記。若沒有變數取值可以滿足   ,則稱    為假
  2. 若任意解釋下公式   都為真,稱  邏輯有效的(logically valid) (類似於命題邏輯恆真式
  3. 若一階邏輯理論   的公理都於   為真,稱解釋   模型(model)

代數化語義

另一種一階邏輯語義的方法可經由命題邏輯的林登鮑姆-塔斯基代數擴展而成。有如下幾種類型:

這些代數都是純粹擴展兩元素布林代數而成的

塔斯基和葛范德於1987年證明,沒有超過包在三個以上的量化內的原子句子的部份一階邏輯,其表示力和關係代數相同。上述部份一階邏輯令人十分地感到有興趣,因為它已足夠表示皮亞諾算術公理化集合論,包括典型的ZFC。他們亦證明了,具有簡單有序對的一階邏輯和具有兩個有序的投影函數的關係代數等價。

空論域

上述的語義解釋都要求論域為非空集合。但在如自由邏輯之中,設定空論域是被允許的。甚至代數結構的類包含一個空結構(如空偏序集),當允許空論域時,這個類只能是一階邏輯中的一個基本類,不然就要將空結構由類中移除。

不過,空論域存在著一些難點:

  • 許多常見的推理規則只在論域被要求是非空時才為有效的。一個例子為,當x不是 內的自由變數時, 會薀涵 。這個用來將公式寫成前束範式的規則在非空論域中是可靠的,但在允許空論域時則是不可靠的。
  • 在使用變數賦值函數的解釋中,真值的定義不能和空論域一起運作,因為不存在範圍為空的變數賦值函數。(相似地,也無法將解釋賦予上常數符號。)在甚至是原子公式的真值可被定義之前,都必須選定一個變數賦值函數。然後一個句子的真值即可在任一個變數賦值之下定義出其真值,且可證明其真值不依選定的賦值而變。這個做法在賦值函數不存在時不能運作;除非將其改成配上空論域。

因此,若空論域是被允許的,通常也必須被視成特例。不過,大多數的作家會簡單地將空論域由定義中排除。

常用的推理性質

定理與證明

以下介紹一些基本用語和符號

在一階邏輯理論   下,   代表有一列公式   滿足:

  1.   符號辨識上為  
  2. 所有的  有下列兩種可能情況
  •    的公理。
  • 存在  使得    (也就是由前面的公式以MP律組合出來)

口語上會稱公式   (或   ) 為   下的定理(theorem)。而這列  會稱為 證明

例如定理    的證明:

   (公理A2)
   (公理A1)
   (公理A1)
    加上MP律)
    加上MP律)

以上其實是蘊含了無限多定理的元定理的證明(因為沒有給出合式公式的明確形式)。方便起見,這種元定理還是會稱為定理並以同樣的形式來表達。

直觀上的證明,總是會有一些“前提假設”,對此,若以   代表一列有限數目的公式,那

  代表有一列公式   滿足:

  1.   符號辨識上為  
  2. 所有的   有下列三種可能情況
  •    的公理。
  •    中的其中一條公式。
  • 存在  使得    (也就是由前面的公式以MP律組合出來)

這樣稱   為在前提   下,  證明;或是說   推論結果

若要特別凸顯   裡的一條"前提條件"   對"證明過程"的重要性,可以用   的符號去特別凸顯。若   裡的公式列舉出來有   ,那亦可表示為

 

證明過程沒有被引用的公式盡可能不寫出來。另一方面從以上對於證明定義可以發現,依怎樣的順序列舉前提條件,對於證明本身是不會有任何影響的。

本節所介紹的符號,在引用哪個理論很顯然的情況下,  的下標  可以省略。

實際的證明常常會"引用"別的(元)定理,嚴格來說,就是照抄(元)定理的證明過程,然後作一些修改使符號一致。為了節省證明的篇幅,引用時只會單單列出配合引用(元)定理所得出的公式(形式),並在後面註明引用的(元)定理代號。

演繹元定理

從公理(A1)和(A2)會得出不但直觀且實用的演繹元定理

(D)Metatheorem of Deduction:

一階邏輯理論   下,若有   ,則有  

證明

(注意這是元邏輯英语Metalogic下的證明):

假設   為條件所說   的證明,如果    裡的公式或   的公理,那根據(A1)

 

所以由MP律有

 

  ,那因為

 

所以有

 

至此 的部分證明完畢。

接下來要用歸納法;假設對   都有   。 若  是公理、或從   來的、或是根本就是  ,仿造上面   的部分就有

 

剩下沒考慮的狀況是由MP律組合出   的狀況,也就是有   使  

由公理A2有

一阶逻辑, 此條目需要編修, 以確保文法, 用詞, 语气, 格式, 標點等使用恰当, 2022年6月15日, 請按照校對指引, 幫助编辑這個條目, 幫助, 討論, 此條目的语调或风格可能不適合百科全書的寫作方式, 2022年6月15日, 請根據指南協助改善这篇条目, 請在讨论页討論問題所在及加以改善, 是使用於数学, 哲学, 语言学及電腦科學中的一种形式系统, 也可以稱為, 一阶斷言演算, 低階斷言演算, 量化理論或谓词逻辑, 一階邏輯和命題邏輯的不同之處在於, 一階邏輯包含量詞, 高階邏輯和一階邏輯不同之處在於,. 此條目需要編修 以確保文法 用詞 语气 格式 標點等使用恰当 2022年6月15日 請按照校對指引 幫助编辑這個條目 幫助 討論 此條目的语调或风格可能不適合百科全書的寫作方式 2022年6月15日 請根據指南協助改善这篇条目 請在讨论页討論問題所在及加以改善 一阶逻辑是使用於数学 哲学 语言学及電腦科學中的一种形式系统 也可以稱為 一阶斷言演算 低階斷言演算 量化理論或谓词逻辑 一階邏輯和命題邏輯的不同之處在於 一階邏輯包含量詞 高階邏輯和一階邏輯不同之處在於 高階邏輯的斷言符號可以有斷言符號或函數符號當做引數 且容許斷言量詞或函數量詞 1 在一階邏輯的語義中 斷言被解釋為關係 而高階邏輯的語義裡 斷言則會被解釋為集合的集合 在通常的語義下 一階邏輯是可靠 所有可證的敘述皆為真 且完備 所有為真的敘述皆可證 的 雖然一階邏輯的邏輯歸結只是半可判定性的 但還是有許多用於一階邏輯上的自動定理證明 一階邏輯也符合一些使其能通過證明論分析的元邏輯定理 如勒文海姆 斯科倫定理及緊緻性定理 一階邏輯是數學基礎中很重要的一部份 許多常見的公理系統 如一階皮亞諾公理 冯诺伊曼 博内斯 哥德尔集合论和策梅洛 弗蘭克爾集合論都是一階理論 然而一階邏輯不能控制其無窮模型的基數大小 因根據勒文海姆 斯科倫定理和康托爾定理 可以構造出一種 病態 集合論模型 使整個模型可數 但模型內卻會覺得自己有 不可數集 類似地 可以證明實數系的普通一階理論既有可數模型又有不可數模型 這類的悖論被稱為斯科倫悖論 但一階的直覺主義邏輯裡 勒文海姆 斯科倫定理不可證明 2 故不會有以上之現象 目录 1 簡介 2 形式理論 2 1 基本符號 2 1 1 邏輯符號 2 1 2 斷言符號 2 1 3 函數符號 2 1 4 常數符號 2 2 語法 2 2 1 項 2 2 2 原子公式 2 2 3 公式 2 2 4 施用 2 2 5 自由變數和約束變數 2 2 6 括弧的簡寫 2 2 7 波蘭表示法 2 3 推理规则 2 3 1 MP律 2 4 公理 2 4 1 邏輯公理 2 4 2 量词公理 2 4 3 等式和它的公理 3 標準語義 3 1 項的取值 3 2 真假的賦值 3 3 代數化語義 3 4 空論域 4 常用的推理性質 4 1 定理與證明 4 2 演繹元定理 4 3 否定 4 4 實質條件 4 5 反證法 4 6 邏輯與和邏輯或 4 6 1 交換性 4 6 2 直觀意義 4 6 3 結合律 4 6 4 分配律 4 7 德摩根定理 4 8 普遍化元定理 4 9 量詞的可交換性 4 10 量詞的簡寫 4 11 等式定理 5 函數符號與唯一性 6 一阶逻辑的元定理 7 转换自然语言到一阶逻辑 8 一阶逻辑的限制 8 1 难于表达if then else 8 2 类型 种类 8 3 难于刻画模型大小 8 4 图可及性不能表达 9 参见 10 参考文献 10 1 引用 10 2 来源 11 外部链接簡介 编辑在命題邏輯裡 蘇格拉底是哲學家 柏拉圖是哲學家 只能簡單標記為 p displaystyle p 及 q displaystyle q 而一階邏輯先设符號 Phil x displaystyle text Phil x 意為 x 是哲學家 然後以 s displaystyle s 代表蘇格拉底 b displaystyle b 代表柏拉圖 則 Phil s displaystyle text Phil s 對應 p displaystyle p Phil b displaystyle text Phil b 對應 q displaystyle q 也就是賦予斷言符號 Phil x displaystyle text Phil x 語意的解釋 這個解釋預設一個 所有人類的群體 也就是語義解釋的論域 并將變數 x displaystyle x 解釋為自群體中取出來的某人 斷言符號可以包含一個以上的變數 例如 设 Cp x y displaystyle text Cp x y 意為 x 與 y 是夫妻 则 Cp s y textstyle text Cp s y 意为 蘇格拉底和 y 是夫妻 一階邏輯和命題邏輯相同 斷言符號和變數還能與邏輯符號組成更複雜的敘述 例如 设斷言符號 Schol x displaystyle text Schol x 意為 x displaystyle x 是學者 則 若 x 為哲學家 則 x 為學者 可表示為 Phil x Schol x displaystyle text Phil x Rightarrow text Schol x 而 對所有 x 若 x 為哲學家 則 x 為學者 則記為 x Phil x Schol x displaystyle forall x text Phil x Rightarrow text Schol x 也就是自左方開始閱讀 以 x displaystyle forall x 表示 对于所有 x 可以將之理解為 对于所有 x x displaystyle forall x 右方的敘述為真 其中 x displaystyle forall x 這個符號被称为 x displaystyle x 的全稱量詞 直觀上有 若所有x是哲學家 那x的長子也會是哲學家 這樣 合理 的敘述 若设 Son x displaystyle text Son x 意為 x 的長子 那么這段 合理 敘述可記為 x Phil x Phil Son x displaystyle forall x text Phil x Rightarrow text Phil text Son x displaystyle Rightarrow 表示 與 x displaystyle x 有唯一對應的那個對象 被稱為函數符號 這段直觀為真的敘述 經過適當的擴展以後就是一階邏輯其中的一條公理 而對於 有 x 是哲學家 这一叙述 則引入另一種量詞表記為 x Phil x displaystyle exists x text Phil x 自左方開始閱讀 以 x displaystyle exists x 代表 存在 x 可以將之理解為 有 x 使 x displaystyle exists x 右方的敘述為真 其中 x displaystyle exists x 被稱為 x displaystyle x 的存在量詞 全稱量詞和存在量詞一起被簡稱為量詞 直觀上 並非所有 x 不是哲學家 和 有 x 是哲學家 是等價的 且 不存在 x 不是學者 也与 所有的 x 是學者 等價 所以只要有 否定 這個邏輯概念 那么一階邏輯就能以全稱量詞為基礎 作以下的符號定義 displaystyle neg 解釋為 否定 而 A displaystyle mathcal A 代表一段 敘述 x A x A displaystyle exists x mathcal A neg forall x neg mathcal A 由此 存在量詞被定義為全稱量詞的衍伸 形式理論 编辑一階邏輯的形式理論可分成幾個部份 語法 英语 Syntax logic 決定哪些符號組合是合式公式 直觀上的 文法無誤的敘述 推理規則 由合式公式符號組合出新合式公式的規則 直觀上的 推理 公理 一套合式公式 直觀上的基本假設 基本符號 编辑 一套理論能容許多少符號 取決於人類根据物理定律能塑造多少符號 但以目前無法確知宇宙是不是有限 或是是否可無限制分割 雖然所有的公理化集合論都以量詞的形式隱晦的承認無窮的存在 如ZF集合論的無窮公理 甚至以這樣自然數意義上的無窮為基礎 去建構出不可數的實數 但將之對應到現實 還是會回到同樣的物理問題 謹慎起見 以下各種類的符號沒有特別聲明 數量將會是有限個 邏輯符號 编辑 詞彙表中存在若干個邏輯符號 通常包括 量化符號 displaystyle forall 及 displaystyle exists 某些作者 3 會把 displaystyle exists 符號定義為 x A x A displaystyle exists x mathcal A neg forall x neg mathcal A 如此便只需要 displaystyle forall 做為基礎符號 邏輯聯結詞 以下為可能的表示符號 关于波蘭表示法下的邏輯連接詞 請參見逻辑运算的波兰记法 否定 displaystyle neg 或 displaystyle sim 條件 displaystyle Rightarrow 或 displaystyle rightarrow 或 displaystyle supset 且 displaystyle land 或 amp displaystyle amp 或 displaystyle lor 或 雙條件 displaystyle Leftrightarrow 或 displaystyle leftrightarrow 某些作者 4 會作如下的符號定義 A B A B displaystyle mathcal A wedge mathcal B neg mathcal A Rightarrow neg mathcal B A B A B displaystyle mathcal A vee mathcal B neg mathcal A Rightarrow mathcal B A B A B B A displaystyle mathcal A Leftrightarrow mathcal B mathcal A Rightarrow mathcal B wedge mathcal B Rightarrow mathcal A 如此一來只需要否定和條件做為基礎符號 dd 標點符號 括號 逗號及其他 依作者的喜好有所不同 為了更有效的將括號做配對 通常還會採用大括號 跟中括號 至多跟自然數一樣多的變數 通常標記為英文字母末端的小寫字母x y z 也常會使用下標 或上標 上下標兼有 來區別不同的變數 x0 x1 x2 特別注意c有時候會被當成常數符號而引起混淆 等式符號 displaystyle 有作者會因為語義上对 相等 的不同解释 而將等式符號視為雙元斷言符號 甚至是某種合式公式的簡寫 符號相等 displaystyle asymp 為了將符號辨識上区别等同和等式符號 某些作者 5 會額外採用這個符號 注意 並非所有的符號都是必需的 比如 在比較極端的情况中 因为謝費爾豎線 或異或 的布林代數完備性使得所有不含量詞的邏輯公理都可以用謝費爾豎線表述 而大幅減少基礎的邏輯聯結詞 另外 一些作者並沒有將語義學和形式理論劃分清楚 而會將真值常數納入符號的一環 用 T Vpq 或 displaystyle top 來表示 真 並用 F Opq 或 displaystyle bot 來表示 假 斷言符號 编辑 他們兩人是夫妻 是一個關於兩個 對象 的斷言 而 他是人 三點共線 则表明斷言容許一個或者多個對象 所以對於自然數 n displaystyle n j displaystyle j 約定 A j n x 1 x 2 x n displaystyle A j n x 1 x 2 x n 為一階邏輯的合法詞彙 它在直觀上表示一個有 n displaystyle n 個 對象 的斷言 稱為 n displaystyle n 元斷言符號 下標的自然數 j displaystyle j 只是拿來和其他同為 n displaystyle n 元的斷言符號作區別 實用上只要有申明 不至於和其他詞彙引起混淆的話 可以用任意的形式簡寫一個斷言符號 如 公理化集合論裡的雙元斷言符號 A 1 2 x y displaystyle A 1 2 x y 也可以表示为 x y displaystyle x in y 函數符號 编辑 物體的顏色 夫妻的長子 这种断言說明了一组對象所唯一對應的對象 但不同的夫妻有不同的長子 不同的物體有不同的顏色 據此 形式上對於自然數 n displaystyle n j displaystyle j 約定 f j n x 1 x 2 x n displaystyle f j n x 1 x 2 x n 為一階邏輯的合法詞彙 直觀上表示 n displaystyle n 個 對象 所對應到的東西 稱它為 n displaystyle n 元函數符號 需要特別注意 這種 唯一對應 的直觀想法 必須配上關於 等式 的性質 詳見下面的等式定理章节 才能在形式理論中被實現 与斷言符號一样 只要不引起混淆 就可以用任何的形式簡寫函數符號 如 公理化集合論裡的 x y displaystyle x cup y 是依據聯集公理而定義的新函數符號 請參見下面函數符號與唯一性章節 也可以冗長的表記為 f j 2 x y displaystyle f j 2 x y 常數符號 编辑 刻度0 原點 蘇格拉底 是直觀上 唯一不變 的對象 據此 對自然數 j displaystyle j 約定 c j displaystyle c j 為一階邏輯的合法詞彙 直觀上表示一個 唯一不變 的對象 稱為常數符號 同樣的 常數的不變性 需配上等式的性質 詳見下面等式定理 才能被實現 為了不和變數的表記混淆 常數符號一樣可以用任何的形式簡寫 如公理化集合論裡的 displaystyle varnothing 是根據空集公理和函數符號與唯一性 而定義的新常數符號 亦可冗長的表示為 c j displaystyle c j 語法 编辑 和自然語言 如英語 不同 一階邏輯的語言以明確的遞迴定義判斷一個給定的詞彙是否合法 大致上來說 一階邏輯以 項 代表討論的對象 而對 項 的斷言組成了最基本的原子 合式 公式 而原子公式和邏輯符號組成了更複雜的合式公式 也就是 敘述 項 编辑 那對夫妻的長子的職業 x y z displaystyle x y times z x displaystyle x cup varnothing 代表變數可以與函數符號組成更一般的物件 據此形式 遞迴地規定一類合法詞彙 項為 變數和常數是項 若 T 1 T n displaystyle T 1 T n 全都是項 那么 f j n T 1 T n displaystyle f j n T 1 T n 也是項 項只能通过以上兩點 於有限步驟內建構出來 習慣上以大寫的西方字母 如英文字母 希伯來字母 希臘字母 代表項 如果變數不得不採用大寫字母 而可能跟項引起混淆的話 需額外規定分辨的辦法 原子公式 编辑 為了比較簡潔地規定甚麼是合式公式 先規定原子公式為 若 T 1 T n displaystyle T 1 T n 是項 A j n T 1 T n displaystyle A j n T 1 T n 這樣的形式 公式 编辑 一階邏輯的合式公式 簡稱公式或 w f displaystyle wf 以下面的規則遞迴地定義 原子公式為公式 美觀起見 在原子公式外面包一層括弧也是公式 若 A displaystyle mathcal A 為公式 則 A displaystyle neg mathcal A 為公式 若 A displaystyle mathcal A 與 B displaystyle mathcal B 為公式 則 A B displaystyle mathcal A Rightarrow mathcal B 為公式 若 A displaystyle mathcal A 為公式 x displaystyle x 為任意變數 則 x A displaystyle forall x mathcal A 為公式 美觀起見 x A x A displaystyle forall x mathcal A forall x mathcal A 也就是裡面的量詞有無外包括弧都是公式 合式公式只能通过以上四點 於有限步驟內建構出來 另外成對的中括弧跟大括弧 符號辨識上視為成對的小括弧 而草書的大寫西方字母為公式的代號 舉例來說 y A 1 2 x f 1 1 y displaystyle forall y A 1 2 x f 1 1 y 是公式而 x x displaystyle forall x x Rightarrow 則不是公式 而接下來只要對任意公式A displaystyle mathcal A B displaystyle mathcal B 與變數 x displaystyle x 做以下符號定義 A B A B displaystyle mathcal A wedge mathcal B neg mathcal A Rightarrow neg mathcal B A B A B displaystyle mathcal A vee mathcal B neg mathcal A Rightarrow mathcal B A B A B B A displaystyle mathcal A Leftrightarrow mathcal B mathcal A Rightarrow mathcal B wedge mathcal B Rightarrow mathcal A x A x A displaystyle exists x mathcal A neg forall x neg mathcal A 同樣美觀起見 x A x A displaystyle exists x mathcal A exists x mathcal A 這樣所有的邏輯連接詞與量詞就納入了合式公式的規範 施用 编辑 所謂的施用 作用 是以下公式形式的口語說法 其中 A displaystyle mathcal A 與 B displaystyle mathcal B 都是公式 A displaystyle neg mathcal A 稱為 displaystyle neg 施用於 A displaystyle mathcal A 上 A B displaystyle mathcal A Rightarrow mathcal B 稱為 displaystyle Rightarrow 施用於 A displaystyle mathcal A 和 B displaystyle mathcal B 上 A B displaystyle mathcal A wedge mathcal B 稱為 displaystyle wedge 施用於 A displaystyle mathcal A 和 B displaystyle mathcal B 上 A B displaystyle mathcal A vee mathcal B 稱為 displaystyle vee 施用於 A displaystyle mathcal A 和 B displaystyle mathcal B 上 A B displaystyle mathcal A Leftrightarrow mathcal B 稱為 displaystyle Leftrightarrow 施用於 A displaystyle mathcal A 和 B displaystyle mathcal B 上 x A displaystyle forall x mathcal A 稱為 x displaystyle forall x 施用於 A displaystyle mathcal A 上 x A displaystyle exists x mathcal A 稱為 x displaystyle exists x 施用於 A displaystyle mathcal A 上 就类似于運算子作用在它們身上 自由變數和約束變數 编辑 量詞所施用的公式被稱為量詞的範圍 scope 同一個變數在公式一般來說不只出現一次 若變數 x displaystyle x 出現在 x displaystyle forall x 的範圍內 稱這樣出現的 x displaystyle x 為不自由 被約束的 x displaystyle x not free bounded 反過來說 不出現在 x displaystyle forall x 的範圍內的某個 x displaystyle x 被稱為自由的 x displaystyle x 例如 對於公式 x A 1 1 x A 2 1 y displaystyle forall x A 1 1 x Rightarrow A 2 1 y A 1 1 x A 2 1 y displaystyle A 1 1 x Rightarrow A 2 1 y 就是量詞 x displaystyle forall x 的範圍 而 A 1 1 x displaystyle A 1 1 x 裡的 x displaystyle x 就是不自由的 反之 A 2 1 y displaystyle A 2 1 y 裡的 y displaystyle y 就是自由的 說 x displaystyle x 於公式 A displaystyle mathcal A 完全自由 意為於 A displaystyle mathcal A 出現的 x displaystyle x 都是自由的 反之 說 x displaystyle x 於公式 A displaystyle mathcal A 完全不自由 完全被約束 意為 A displaystyle mathcal A 內根本沒有 x displaystyle x 或是 A displaystyle mathcal A 內沒有自由的 x displaystyle x 若 A displaystyle mathcal A 內所有的變數都完全不自由 A displaystyle mathcal A 特稱為封閉公式 句子 closed formula sentence 括弧的簡寫 编辑 括弧是為了保證語意解釋符合預期 但太多的括弧書寫不易 為此規定以下的 重構法 反過來就是 簡寫法 從表面上不合法的一串符號找出作者原來想表達的公式 若整串符號的括弧不成對 直接視為無法重構 以 displaystyle lnot land lor forall exists Rightarrow Leftrightarrow 左至右 的施用順序重構括弧 相鄰的邏輯連接詞或量詞無法決定施用順序的話 以右邊為先 重構施用的順序 以被成對括弧包住的部分為優先施用 其次才是落單的斷言符號 舉例來說 x A 1 1 x x A 2 1 x displaystyle lnot forall xA 1 1 x Rightarrow exists x lnot A 2 1 x 的重構過程如下 x A 1 1 x x A 2 1 x displaystyle lnot forall xA 1 1 x Rightarrow exists x lnot A 2 1 x 優先施用 displaystyle lnot x A 1 1 x x A 2 1 x displaystyle lnot forall xA 1 1 x Rightarrow exists x lnot A 2 1 x 施用 displaystyle exists x A 1 1 x x A 2 1 x displaystyle lnot forall xA 1 1 x Rightarrow exists x lnot A 2 1 x 最後施用 displaystyle Rightarrow 可以被重構為公式的一串符號則寬鬆的認定為 合式公式 最明顯的例子就是合式公式最外層的括弧可以省略 波蘭表示法 编辑 波蘭表示法將邏輯連接詞前置於被施用的公式而非傳統的中間 如果沿用以上的 施用順序 這個表示法允許捨棄所有括弧 如公式 x y A 1 1 f 1 1 x A 1 1 x A 1 3 f 1 1 y x z displaystyle forall x forall y A 1 1 f 1 1 x Rightarrow neg A 1 1 x Rightarrow A 1 3 f 1 1 y x z 轉成波蘭表示法的過程如下 x y A 1 1 f 1 1 x A 1 1 x A 1 3 f 1 1 y x z displaystyle forall x forall y Rightarrow A 1 1 f 1 1 x neg Rightarrow A 1 1 xA 1 3 f 1 1 yxz 轉成波蘭表示法的順序 P x P y C A 1 1 f 1 1 x N C A 1 1 x A 1 3 f 1 1 y x z displaystyle Pi x Pi y text C A 1 1 f 1 1 x text N text C A 1 1 xA 1 3 f 1 1 yxz 邏輯連結詞的符號轉換 推理规则 编辑 MP律 编辑 對於公式 A displaystyle mathcal A 和 B displaystyle mathcal B A B displaystyle mathcal A Rightarrow mathcal B 和 A displaystyle mathcal A 組合出 B displaystyle mathcal B 直觀意義非常明顯 就是p gt q且p可以推出q 公理 编辑 邏輯公理 编辑 如果B displaystyle mathcal B C displaystyle mathcal C D displaystyle mathcal D 都是公式 則 A1 B C B displaystyle mathcal B Rightarrow mathcal C Rightarrow mathcal B A2 B C D B C B D displaystyle mathcal B Rightarrow mathcal C Rightarrow mathcal D Rightarrow mathcal B Rightarrow mathcal C Rightarrow mathcal B Rightarrow mathcal D A3 B C B C B displaystyle neg mathcal B Rightarrow neg mathcal C Rightarrow neg mathcal B Rightarrow mathcal C Rightarrow mathcal B 都是公理 它们实际上是公理模式 代表著 跟自然數一樣多 條的公理 量词公理 编辑 以下的 x displaystyle x 為任意變數 B displaystyle mathcal B C displaystyle mathcal C 為任意公式 A4 T displaystyle T 是一個項 t displaystyle t 為 T displaystyle T 中出現的任意變數 若 B displaystyle mathcal B 裡 所有 t displaystyle forall t 的的範圍裡都沒有自由的 x displaystyle x 這個情況稱為 B displaystyle mathcal B 裡項 T displaystyle T 對 x displaystyle x 是自由的 則 x B x B T displaystyle forall x mathcal B x Rightarrow mathcal B T dd 為公理 其中 B T displaystyle mathcal B T 代表把 B displaystyle mathcal B 裡自由的 x displaystyle x 都取代為 T displaystyle T 所得到的新公式 A5 如果 x displaystyle x 在 B displaystyle mathcal B 裡完全被約束 則 x B C B x C displaystyle forall x mathcal B Rightarrow mathcal C Rightarrow mathcal B Rightarrow forall x mathcal C dd 為公理 A6 x B C x B x C displaystyle forall x mathcal B Rightarrow mathcal C Rightarrow forall x mathcal B Rightarrow forall x mathcal C 為公理 A7 若 B displaystyle mathcal B 是公理 x displaystyle x 是任意變數 則 x B displaystyle forall x mathcal B dd 也是公理 它们实际上是公理模式 等式和它的公理 编辑 根據不同作者的看法 甚至是理論本身的需求 等式 在形式理論裡可能是斷言符號或是一段公式 如 a 等於 b 可定義為對所有的 x x 屬於 a 等價於 x 屬於 b 而如何刻劃直觀上 等式的性質 有一開始就將 等式的性質 視為公理 模式 但也有視為元定理的另一套處理方法 以下暫且以公理模式的方式處理 以元定理處理的方法會在等式定理詳述 x y displaystyle x y 是一段變數 x displaystyle x y displaystyle y 完全自由 且型式完全被確定的公式 E x y displaystyle mathcal E x y 的簡寫 要求 E1 對任意變數 x displaystyle x x x displaystyle x x 為公理 E2 對於任意變數 x displaystyle x 和 y displaystyle y 若在公式 A displaystyle mathcal A 中自由的 y displaystyle y 都不在 x displaystyle forall x 的範圍內 若以A y displaystyle mathcal A y 代表 A displaystyle mathcal A 某些 而非全部 自由的 x displaystyle x 被取代成 y displaystyle y 而成的新公式 則 x y A A y displaystyle x y Rightarrow mathcal A Rightarrow mathcal A y dd 為公理 事實上這兩個公理模式也確保了函數符號 唯一對應 和常數符號的 唯一性 但證明這些性質需要一些元定理 簡便起見合併於下面的等式定理一節講述 標準語義 编辑一階邏輯的標準語義源於波蘭邏輯學家阿尔弗雷德 塔斯基所著 On the Concept of Truth in Formal Languages 根據上面語法一節 公式是由原子公式遞迴地添加邏輯連結詞而來的 而原子公式是由斷言符號與項所構成的 所以要檢驗一條公式在特定的論域下正不正確 就要規定項的取值 然後檢驗這樣的取值會不會落在斷言符號所對應的關係裡 由此延伸出所有公式的 真假值 也就是一套一階邏輯的語義解釋 要包含 變數取值的論域 如何解釋函數符號 為論域中的某個函數 與常數符號 為論域中的某特定元素 以便從特定的變數取值得出項的取值 如何將斷言符號與論域裡的某關係做對應 通常一套解釋方法 簡稱為解釋 會以代號 M displaystyle M 表示 項的取值 编辑 量詞的解釋需要指明變數取值範圍的論域 也就是一個集合 D displaystyle D 而變數可能跟自然數一樣多 換句話說 所有變數在論域 D displaystyle D 取的值可以依序以自然數標下標 也就是一個在 D displaystyle D 取值的數列 如果以 x 1 x 2 x 3 displaystyle x 1 x 2 x 3 cdots 的代號 不一定是變數本身的表示符號 來列舉變數 那麼從 D displaystyle D 的某套變數取值就以 a k k N displaystyle left langle a k right rangle k in mathbb N 或較直觀的符號 a 1 a 2 a 3 displaystyle left langle a 1 a 2 a 3 cdots right rangle 來表示 一套解釋 M displaystyle M 會將 n displaystyle n 元函數符號 f i n displaystyle f i n 解釋成某個 f i n M D n D displaystyle f i n M D n to D 的 n displaystyle n 元函數 而常數符號 c l displaystyle c l 解釋成特定的 c l M D displaystyle c l M in D 亦稱為 c l displaystyle c l 的取值為 c l M displaystyle c l M 這樣就可以用上面語法一節定義項的方式 遞迴地規定項的取值 在解釋 M displaystyle M 下的某套變數取值下 一列項 T 1 T n displaystyle T 1 cdots T n 的取值分別為 T 1 M T n M displaystyle T 1 M cdots T n M 則這套變數取值下 項 f i n T 1 T n displaystyle f i n T 1 cdots T n 的取值規定為 f i n M T 1 M T n M displaystyle f i n M T 1 M cdots T n M 真假的賦值 编辑 直觀上要解釋關係最直接的方法 就是列舉所有符合關係的對象 例如如果想說明夫妻關係 可以列舉所有 老公 老婆 的雙元有序對 但並非所有的人類有序對都會在這個關係中 以此為基礎 若以 D m displaystyle D m 代表所有以 m displaystyle m 個 D displaystyle D 中的元素構成的 m displaystyle m 元有序對的集合 也就是 m displaystyle m 元笛卡兒積 那一套解釋 M displaystyle M 會將 m displaystyle m 元斷言符號 A j m displaystyle A j m 解釋為一個 A j m M D m displaystyle A j m M subseteq D m 的m displaystyle m 元有序對子集合 這樣就可以依據語法的遞迴定義 以下面的規則對每條公式賦予真值 這種賦值方式稱為T 模式 取名於邏輯學家阿尔弗雷德 塔斯基 在一套解釋 M displaystyle M 下 在一套特定的變數取值下 一列項 T 1 T m displaystyle T 1 cdots T m 的取值為 T 1 M T m M displaystyle T 1 M cdots T m M 那 A j m T 1 T m displaystyle A j m T 1 cdots T m 為真定義為 T 1 M T m M A j m M displaystyle T 1 M cdots T m M in A j m M dd 反之 T 1 M T m M A j m M displaystyle T 1 M cdots T m M notin A j m M dd 則定義為假 dd 在一套特定的變數取值下 B displaystyle neg mathcal B 為真 等價於 B displaystyle mathcal B 為假 在一套特定的變數取值下 B C displaystyle mathcal B Rightarrow mathcal C 為真 意為 B displaystyle mathcal B 為假或是 C displaystyle mathcal C 為真 p gt q為假只有p為真且q為假的狀況 在變數取值 a k k N displaystyle left langle a k right rangle k in mathbb N 下 x i B displaystyle forall x i mathcal B 為真 意為 對所有的 d D displaystyle d in D B displaystyle mathcal B 於變數取值 a 1 a i 1 d a i 1 displaystyle left langle a 1 cdots a i 1 d a i 1 cdots right rangle 下為真 也就是把變數 x i displaystyle x i 的取值換為論域的任意元素仍然為真 更進一步的來說 在一套解釋 M displaystyle M 下 不管怎麼樣的變數取值 公式 B displaystyle mathcal B 都為真 則稱為M displaystyle M 下 B displaystyle mathcal B 為真 以符號 M B displaystyle M vDash mathcal B 簡記 若沒有變數取值可以滿足 B displaystyle mathcal B 則稱M displaystyle M 下 B displaystyle mathcal B 為假 若任意解釋下公式 B displaystyle mathcal B 都為真 稱 B displaystyle mathcal B 為邏輯有效的 logically valid 類似於命題邏輯的恆真式 若一階邏輯理論 L displaystyle mathcal L 的公理都於 M displaystyle M 為真 稱解釋 M displaystyle M 為 L displaystyle mathcal L 之模型 model 代數化語義 编辑 另一種一階邏輯語義的方法可經由命題邏輯的林登鮑姆 塔斯基代數擴展而成 有如下幾種類型 圓柱代數 由阿爾弗雷德 塔斯基和其同事提出 多元代數 由保羅 哈爾莫斯提出 斷言函子邏輯 主要是基於威拉德 范 奧曼 奎因的工作成果 這些代數都是純粹擴展兩元素布林代數而成的格 塔斯基和葛范德於1987年證明 沒有超過包在三個以上的量化內的原子句子的部份一階邏輯 其表示力和關係代數相同 上述部份一階邏輯令人十分地感到有興趣 因為它已足夠表示皮亞諾算術和公理化集合論 包括典型的ZFC 他們亦證明了 具有簡單有序對的一階邏輯和具有兩個有序的投影函數的關係代數等價 空論域 编辑 主条目 空論域 上述的語義解釋都要求論域為非空集合 但在如自由邏輯之中 設定空論域是被允許的 甚至代數結構的類包含一個空結構 如空偏序集 當允許空論域時 這個類只能是一階邏輯中的一個基本類 不然就要將空結構由類中移除 不過 空論域存在著一些難點 許多常見的推理規則只在論域被要求是非空時才為有效的 一個例子為 當x不是ϕ displaystyle phi 內的自由變數時 ϕ x ps displaystyle phi lor exists x psi 會薀涵 x ϕ ps displaystyle exists x phi lor psi 這個用來將公式寫成前束範式的規則在非空論域中是可靠的 但在允許空論域時則是不可靠的 在使用變數賦值函數的解釋中 真值的定義不能和空論域一起運作 因為不存在範圍為空的變數賦值函數 相似地 也無法將解釋賦予上常數符號 在甚至是原子公式的真值可被定義之前 都必須選定一個變數賦值函數 然後一個句子的真值即可在任一個變數賦值之下定義出其真值 且可證明其真值不依選定的賦值而變 這個做法在賦值函數不存在時不能運作 除非將其改成配上空論域 因此 若空論域是被允許的 通常也必須被視成特例 不過 大多數的作家會簡單地將空論域由定義中排除 常用的推理性質 编辑定理與證明 编辑 以下介紹一些基本用語和符號 在一階邏輯理論 L displaystyle mathcal L 下 L A displaystyle vdash mathcal L mathcal A 代表有一列公式 C i 1 i n displaystyle mathcal C i 1 leq i leq n 滿足 C n displaystyle mathcal C n 符號辨識上為 A displaystyle mathcal A 所有的 C k displaystyle mathcal C k 有下列兩種可能情況C k displaystyle mathcal C k 為 L displaystyle mathcal L 的公理 存在 i j lt k displaystyle i j lt k 使得 C i displaystyle mathcal C i 為 C j C k displaystyle mathcal C j Rightarrow mathcal C k 也就是由前面的公式以MP律組合出來 dd 口語上會稱公式 A displaystyle mathcal A 或 L A displaystyle vdash mathcal L mathcal A 為 L displaystyle mathcal L 下的定理 theorem 而這列C i 1 i n displaystyle mathcal C i 1 leq i leq n 會稱為 L A displaystyle vdash mathcal L mathcal A 的證明 例如定理 I displaystyle I L B B displaystyle vdash mathcal L mathcal B Rightarrow mathcal B 的證明 C 1 displaystyle mathcal C 1 B B B B B B B B B displaystyle mathcal B Rightarrow mathcal B Rightarrow mathcal B Rightarrow mathcal B Rightarrow mathcal B Rightarrow mathcal B Rightarrow mathcal B Rightarrow mathcal B Rightarrow mathcal B 公理A2 C 2 displaystyle mathcal C 2 B B B B displaystyle mathcal B Rightarrow mathcal B Rightarrow mathcal B Rightarrow mathcal B 公理A1 C 3 displaystyle mathcal C 3 B B B displaystyle mathcal B Rightarrow mathcal B Rightarrow mathcal B 公理A1 C 4 displaystyle mathcal C 4 B B B B B displaystyle mathcal B Rightarrow mathcal B Rightarrow mathcal B Rightarrow mathcal B Rightarrow mathcal B C 1 displaystyle mathcal C 1 和C 2 displaystyle mathcal C 2 加上MP律 C 5 displaystyle mathcal C 5 B B displaystyle mathcal B Rightarrow mathcal B C 4 displaystyle mathcal C 4 和C 3 displaystyle mathcal C 3 加上MP律 以上其實是蘊含了無限多定理的元定理的證明 因為沒有給出合式公式的明確形式 方便起見 這種元定理還是會稱為定理並以同樣的形式來表達 直觀上的證明 總是會有一些 前提假設 對此 若以 G displaystyle Gamma 代表一列有限數目的公式 那 G L A displaystyle Gamma vdash mathcal L mathcal A 代表有一列公式 C i 1 i n displaystyle mathcal C i 1 leq i leq n 滿足 C n displaystyle mathcal C n 符號辨識上為 A displaystyle mathcal A 所有的 C k displaystyle mathcal C k 有下列三種可能情況C k displaystyle mathcal C k 為 L displaystyle mathcal L 的公理 C k displaystyle mathcal C k 為 G displaystyle Gamma 中的其中一條公式 存在 i j lt k displaystyle i j lt k 使得 C i displaystyle mathcal C i 為 C j C k displaystyle mathcal C j Rightarrow mathcal C k 也就是由前面的公式以MP律組合出來 dd 這樣稱 C i 1 i n displaystyle mathcal C i 1 leq i leq n 為在前提 G displaystyle Gamma 下 A displaystyle mathcal A 的證明 或是說 A displaystyle mathcal A 是 G displaystyle Gamma 的推論結果 若要特別凸顯 G displaystyle Gamma 裡的一條 前提條件 B displaystyle mathcal B 對 證明過程 的重要性 可以用 G B L A displaystyle Gamma mathcal B vdash mathcal L mathcal A 的符號去特別凸顯 若 G displaystyle Gamma 裡的公式列舉出來有 B 1 B n displaystyle mathcal B 1 mathcal B n 那亦可表示為 B 1 B n L A displaystyle mathcal B 1 mathcal B n vdash mathcal L mathcal A 證明過程沒有被引用的公式盡可能不寫出來 另一方面從以上對於證明定義可以發現 依怎樣的順序列舉前提條件 對於證明本身是不會有任何影響的 本節所介紹的符號 在引用哪個理論很顯然的情況下 L displaystyle vdash mathcal L 的下標L displaystyle mathcal L 可以省略 實際的證明常常會 引用 別的 元 定理 嚴格來說 就是照抄 元 定理的證明過程 然後作一些修改使符號一致 為了節省證明的篇幅 引用時只會單單列出配合引用 元 定理所得出的公式 形式 並在後面註明引用的 元 定理代號 演繹元定理 编辑 從公理 A1 和 A2 會得出不但直觀且實用的演繹元定理 D Metatheorem of Deduction 一階邏輯理論 L displaystyle mathcal L 下 若有 G B L C displaystyle Gamma mathcal B vdash mathcal L mathcal C 則有 G L B C displaystyle Gamma vdash mathcal L mathcal B Rightarrow mathcal C 證明 注意這是元邏輯 英语 Metalogic 下的證明 假設 C 1 C 2 C n displaystyle mathcal C 1 mathcal C 2 mathcal C n 為條件所說 C displaystyle mathcal C 的證明 如果 C 1 displaystyle mathcal C 1 是G displaystyle Gamma 裡的公式或 L displaystyle mathcal L 的公理 那根據 A1 C 1 B C 1 displaystyle vdash mathcal C 1 Rightarrow mathcal B Rightarrow mathcal C 1 所以由MP律有 G B C 1 displaystyle Gamma vdash mathcal B Rightarrow mathcal C 1 若 C 1 displaystyle mathcal C 1 是 B displaystyle mathcal B 那因為 B B displaystyle vdash mathcal B Rightarrow mathcal B 所以有 G B C 1 displaystyle Gamma vdash mathcal B Rightarrow mathcal C 1 至此C 1 displaystyle mathcal C 1 的部分證明完畢 接下來要用歸納法 假設對 i lt k displaystyle i lt k 都有 G B C i displaystyle Gamma vdash mathcal B Rightarrow mathcal C i 若C k displaystyle mathcal C k 是公理 或從 G displaystyle Gamma 來的 或是根本就是 B displaystyle mathcal B 仿造上面 C 1 displaystyle mathcal C 1 的部分就有 G B C k displaystyle Gamma vdash mathcal B Rightarrow mathcal C k 剩下沒考慮的狀況是由MP律組合出 C k displaystyle mathcal C k 的狀況 也就是有 l m lt k displaystyle l m lt k 使C m displaystyle mathcal C m 是 C l C k displaystyle mathcal C l Rightarrow mathcal C k 由公理A2有 B C l C k B C l B C k displaystyle vdash mathcal B Rightarrow mathcal C l Rightarrow mathcal C k Rightarrow mathcal B Rightarrow mathcal C l Rightarrow mathcal B Rightarrow mathcal C k span, 维基百科,wiki,书籍,书籍,图书馆,

文章

,阅读,下载,免费,免费下载,mp3,视频,mp4,3gp, jpg,jpeg,gif,png,图片,音乐,歌曲,电影,书籍,游戏,游戏。