一阶逻辑

使用於數學、哲學、語言學及電腦科學中的一種形式系統

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

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

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

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

簡介编辑

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

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

其實斷言符號可以包含一個以上的變數,像是把   解釋為「xy是夫妻」,這樣

 

就解釋成「蘇格拉底和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)。而如何刻劃直觀上「等式的性質」,有一開始就將「等式的性質」視為公理(模式),但也有視為元定理英语Metatheorem的另一套處理方法,以下暫且以公理模式的方式處理。以元定理處理的方法會在等式定理詳述。

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

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

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

標準語義编辑

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

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

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

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

項的取值编辑

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

 

或較直觀的符號

 

來表示。

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

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

 

真假的賦值编辑

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

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

 

 有序對子集合。

這樣就可以依據語法的遞迴定義,以下面的規則對每條公式賦予真值。(這種賦值方式稱為T-模式,取名於邏輯學家Alfred Tarski

在一套解釋   下:

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

更進一步的來說

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

代數化語義编辑

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

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

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

空論域编辑

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

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

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

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

常用的推理性質编辑

定理與證明编辑

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

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

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

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

例如定理   的證明:

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

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

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

  代表有一列公式   滿足:

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

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

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

 

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

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

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

演繹元定理编辑

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

(D)Metatheorem of Deduction:

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

證明

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

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

 

所以由MP律有

 

  ,那因為

 

所以有

 

至此 的部分證明完畢。

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

 

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

由公理A2有

 

套用歸納法的假設,加上MP律,就會發現

 

如此可以一路歸納到   也就是   的情況,故元定理得證。 

因為   代表的是有限條公式,所以透過演繹元定理可以將證明過程必要的前提條件遞迴地移到   後,直到不需要任何前提為止;然後由MP律可以知道,若有   ,則有  ,如此一來透過演繹元定理搬到推論結果的合式公式,也可以任意的搬回來。所以   等價於某定理   。因此也會將   稱為一個定理

而從演繹元定理和MP律,會有以下直觀且實用的元定理

(D1)  

(D2)  

以下如果需要將引用的定理以演繹元定理進行"搬移",會省略掉搬移的過程並在搬移後得到的結果後標註(D)。如果引用以上的(D1)和(D2)也會省略過程,單有結果和代號標註。

否定编辑

(DNe) Double negation, elimination

 

證明

(1)  (A3)

(2)  (I)

(3)  (D2 with 1, 2)

(4)  (A1)

(5)  (D1 with 3, 4)

(DNi) Double negation, introduction

 

證明

(1)  (A3)

(2)  (MP with DNe, 1)

(3)  (A1)

(4)  (D1 with 2,3)

上面兩定理表達了雙否定推理上等價於於原公式,引用兩者任一會都以(DN)簡寫。

(T1) Transposition-1

 

證明

(1)  (A3)

(2)  (Hyp)

(3)  (MP with 1, 2)

(4)  (A1)

(5)  (D1 with 3, 4)

(T2) Transposition-2

 

證明

(1)  (DN)

(2)  (Hyp)

(3)  (D with 1, 2)

(4)  (DN)

(5)  (D1 with 3,4)

(6)  (T1, D)

(7)  (MP with 5, 6)

以上二定理表說明   推理上等價於   ,引用這兩個定理中任一都以(T)表示。

由(T)可以得到形式上類似於公理(A3)的定理

(A3') 

證明

(1)  (A3)

(2)  (T, D)

(3)  (Hyp)

(4)  (MP with 2, 3)

(5)  (MP with 1, 4)

(6)  (T, D)

(7)  (Hyp)

(8)  (MP with 6, 7)

(9)  (MP with 5, 8)

實質條件编辑

以下的定理重現了實質條件的直觀理解。

(M0)material condition

 

(也就是 

證明

(1)  (Hyp)

(2)  (Hyp)

(3)  (A3)

(4)  (A1)

(5)  (MP with 4, 1)

(6)  (A1)

(7)  (MP with 6, 2)

(8)  (MP with 3,5)

(9)  (MP with 8,7)

(M1)material condition

 

證明

首先注意到  (MP)

(1)  (0, D)

(2)  (T)

(3)  (Hyp)

(4)  (MP with 1, 3)

(5)  (MP with 2, 4)

(6)  (Hyp)

(7)  (MP 5, 6)

(M2)material condition

 

證明

(1)  (A1)

(2)  (T)

(3)  (MP with 1, 2)

(4)  (Hyp)

(5)  (MP with 3, 4)

(M3)material condition

 

證明

(1)  (M0, D)

(2)  (T)

(3)  (MP with 1, 2)

(4)  (Hyp)

(5)  (MP with 3,4)

(6)  (MP with 5, DN)

反證法编辑

(C1)Proof by Contradiction

 

證明

(1)  (T, D)

(2)  (Hyp)

(3)  (MP with 1, 2)

(4)  (Hyp)

(5)  (MP with DN, 4)

(6)  (MP with 3, 5)

(C2)Proof by Contradiction

 

證明提示:仿(C1)。

邏輯與邏輯或编辑

交換性编辑

以下為"且"的交換性

 

證明

(1)  (C1, D)

(2)  (T, D)

(3)  (MP with 1,2)

類似的,(C2)正是"或"的"可交換性":

  (C2, D)

直觀意義编辑

"且"的直觀意義是實質條件元定理的直接結果

(AND)Intuitive meaning of And:

  (M1)

  (M3)

  (M2)

從(AND)和   的符號定義可知,  的證明可以拆成兩部分;習慣上會以「(   ) 」標示   部分的證明,而「(   ) 」標示   部分的證明。

類似的,"或"的直觀意義是(M0)跟(D)的直截結果

(OR)Intuitive meaning of OR:

  (M0, DN)

  (A1, D)

  (D)

  (交換性, D)

以下的定理則是(A3')的直截結果

(DisJ)Disjunction:

 

證明

(1)   (Hyp)

(2)   (Hyp)

(3)   (D1 with 1, 2)

(4)   (Hyp)

(5)   (A3' with 3, 4)

結合律编辑

對於"且",展開符號定義後,可以從直觀意義輕鬆地得到

(ASO-AND)Associativity of AND:

 

證明提示: (AND)

"或"也有類似的性質

(ASO-OR)Associativity of OR

 

證明提示: (M1), (M2), (M3)

分配律编辑

"且"和"或"之間還有分配律

(DIS-1)Distribution:

 

證明

 

(1)  (Hyp)

(2)  (MP with 1, AND)

(3)  (MP with 1, AND)

(4)  (Hyp)

(5)  (MP with 4, DN)

(6)  (D1 with 3, 5)

(7)  (MP with 2, 5)

(8)  (MP twice with 2, 7, AND)

也就是

 

再套用(D)就會得到

 

 

(1)  (Hyp)

(2)  (D1 with 1, AND)

(3)  (D1 with 1, AND)

(4)  (MP with 2, C2)

(5)  (MP with 3, C2)

(6)  (D1 with 4, AND)

(7)  (D1 with 4, AND)

(8)  (A3' with 6, I)

(9)  (MP twice with 7, 8, AND)

也就是

 

(DIS-2)Distribution:

 

證明

 

(1) (Hyp)

(2)  (D1 with 1, AND)

(3)  (D1 with 1, AND)

(4) (MP twice with 2, 3,AND)

也就是

 

 

(1)  (Hyp)

(2)  (MP with 1, AND)

(3)  (MP with 1, AND)

(4)  (Hyp)

(5)  (MP with 2,4)

(6)  (MP with 3,4)

(7)  (MP twice with 5, 6, AND)

也就是

 

再使用一次推論元定理會得到

 

德摩根定理编辑

以下的元定理的名字來自於英國邏輯學家奧古斯塔斯·德摩根

De Morgan I

 

證明

 

(1)  (Hyp)
(2)  (MP with 1, DN)
(3)  (DN)
(4)  (D1 with 2, 3)

 

(1)  (Hyp)
(2)  (DN)
(3)  (D1 with 1, 2)
(4)  (MP with DN, 3)

De Morgan II

 

證明

證明

 

(1)  (Hyp)
(2)  (MP with M2, 1)
(3)  (MP with M3, 1)
(4)  (AND with 2, 3)

 

(1)  (Hyp)
(2)  (Hyp)
(3)  (M1)

普遍化元定理编辑

公理模式(A7)可以稍加延伸成以下的元定理

元定理(定理的普遍化):

對任意變數   ,若   則有  

證明

假設  就是  的證明,那  一定是公理,根據(A7)可以得到

 

若對   都有   ,如果   是公理的話顯然  

若有   使得

 

那根據歸納法的假設跟(A6)有

 

上式配上

 

就可以得到

 

以此歸納到  也就是  ,故本元定理得證。 

更進一步,有以下元定裡

元定理普遍化, GEN):

  裡變數   都完全被約束,若

 

則有

 
證明

以下對前提條件的數量   做歸納。

 ,根據前提有

 

以(D)將   往前搬,再套用定理的普遍化,會得到

 

再根據(A5)和MP律,就可以得到

 

也就是本元定理要求的結果。

現在假設   的情況下元定理會成立。元定理的前提條件根據(D)可以寫為

 

則根據歸納法的假設

 

上式配上(A5),本元定理在   的情況就可以得到證明,故本元定理得證。 

(GEN)可以稍加修飾,以套用在含有存在量詞的公式上

元定理(GENe):

若變數    的公式和   裡都完全被約束則

(1) 若   

(2) 若   

證明提示:對(GEN)使用(T)和(A5)

量詞的可交換性编辑

由普遍化,很容易證明以下關於"交換性"的定理

(1)  

(2)  

(3)  

注意最後(3)一般來說是不能反向的,只要想到"對每個  ,都有一個數(也就是   ),使  ",但是任取一個   的數   和任意的數