標籤：

你好，類型（四）：Propositional logic

04-07

前兩篇中，我們介紹了 lambda 演算和 CL （組合子邏輯），

我們採用了公理化的方法，先定義系統中的公理，然後定義推導規則，

最終得到了兩個形式系統， lambda_eta 系統以及 CL_w 系統。

值得注意的是，公理系統不僅僅包含由公理和推導構成的形式系統，

還包含給這個形式系統所選擇的語義。

給形式系統選擇一個可靠的語義，是複雜的，我們將在後文再詳細介紹。

從這一篇開始，我們先開始介紹數理邏輯，看看邏輯學是怎麼看待形式化問題的。

1. 命題邏輯形式系統

下文中，我們採用與 lambda_eta 系統， CL_w 系統相同的方式，

來介紹命題邏輯（propositional logic）。

命題邏輯，是在研究命題的證明和推理的過程中抽象出來的，

先不考慮語義，僅僅從符號的角度（形式化）來考慮它，則是更簡單直接的。

1.1 公理和推導規則

首先我們給出命題邏輯形式系統中的公理（有三條公理），

（1） alpha o(eta oalpha)

（2） (alpha o(eta ogamma)) o((alpha oeta) o(alpha ogamma))

（3） ( egalpha o egeta) o(eta oalpha)

然後，我們給出命題邏輯形式系統中的推導規則（只有一條），

（1） frac{alpha,alpha oeta}{eta}

以上推導規則可以理解為，如果 alpha 和 alpha oeta 成立，則 eta 成立。

這裡我們採用了推導規則的常用寫法， frac{P_1,P_2,cdots,P_n}{C} ，

橫線上面的部分「 P_1,P_2,cdots,P_n 」稱為規則的前提（premise），

橫線下面的部分「 C 」，稱為結論（conclusion）。

在命題邏輯中，根據公理和推導規則，得到的公式稱為定理。

根據公理，定理和推導規則，得到的公式也是定理。

1.2 例子

下面我們來看一個例子，

求證： (alpha oeta) o(alpha oalpha) 是一個定理。

證明：

首先，我們使用公理（1），我們有下式成立，

alpha o(eta oalpha)

然後，我們使用公理（2），並令其中的 gamma=alpha ，

(alpha o(eta oalpha)) o((alpha oeta) o(alpha oalpha))

最後，我們結合以上兩個結論，再使用推導規則（1），就得到了，

(alpha oeta) o(alpha oalpha)

證畢。

2. Hilbert-style和Gentzen-style

以上的證明過程中，每一行斷言，是一個不包含條件的定理，

這種風格的演繹系統（deduction system）稱為具有Hilbert-style。

如果 Gamma,Delta 是有限的公式集合，則， GammavdashDelta ，稱為一個序貫（sequent）。

其中， Gamma 稱為序貫的前提（antecedent）， Delta 稱為序貫的結論（succedent）。

它表示，如果公式集 Gamma 都成立，那麼 Delta 中至少有一個成立。

如果證明過程中，每一行斷言是一個序貫，

這種風格的演繹系統，稱為具有Gentzen-style。

Hilbert-style演繹系統，通常具有較多的公理，但是具有較少的推導規則，

Gentzen-style演繹系統，則反之，具有較少的公理，卻具有較多的推導規則。

如果 Delta 中總是只包含一個公式，

則稱該演繹系統為自然演繹系統（natural deduction system）。

如果有限序列， Gamma_1vdashalpha_1,Gamma_2vdashalpha_2,cdots,Gamma_nvdashalpha_n ，滿足，

（1） Gamma_1,Gamma_2,cdots,Gamma_n 為有限公式集，

（2） alpha_1,alpha_2,cdots,alpha_n 為公式，

（3）每個 Gamma_ivdashalpha_i ， (1leqslant ileqslant n) ，都是它之前若干個 Gamma_jvdashalpha_j ， (1leqslant j<ileqslant n) ，應用某條推導規則得到的。

我們就稱這個有限序列，為 Gamma_nvdashalpha_n 的一個（形式）證明序列。

此時，也稱 alpha_n 可由 Gamma_n （形式）證明。

3. 命題邏輯的自然演繹系統

以上定義的形式系統，稱為命題邏輯形式系統 P ，

下面我們再定義一個與之等價的，命題邏輯的自然演繹系統 N 。

3.1 語法

（1）可數個命題符號： p_1,p_2,cdots

（2）5個聯接詞符號： eg,lor,land, o,leftrightarrow

（3）2個輔助符號： ),(

3.2 合法的公式

我們使用BNF來定義，

alpha::=p|( egalpha)|(alpha_1loralpha_2)|(alpha_1landalpha_2)|(alpha_1 oalpha_2)|(alpha_1leftrightarrowalpha_2)

3.3 推導規則

（1）包含律： frac{alphainGamma}{Gammavdashalpha}

（2） eg 消去律： frac{Gamma, egalphavdasheta;Gamma, egalphavdash egeta}{Gammavdashalpha}

（3） o 消去律： frac{Gammavdash(alpha oeta);Gamma oalpha}{Gammavdasheta}

（4） o 引入律： frac{Gamma,alphavdasheta}{Gammavdashalpha oeta}

（5） lor 消去律： frac{Gamma,alphavdashgamma;Gamma,etavdashgamma}{Gamma,alphaloretavdashgamma}

（6） lor 引入律： frac{Gammavdashalpha}{Gammavdashalphaloreta;Gammavdashetaloralpha}

（7） land 消去律： frac{Gammavdashalphalandeta}{Gammavdashalpha;Gammavdasheta}

（8） land 引入律： frac{Gammavdashalpha;Gammavdasheta}{Gammavdashalphalandeta}

（9） leftrightarrow 消去律： frac{Gammavdashalphaleftrightarroweta;Gammavdashalpha}{Gammavdasheta} ， frac{Gammavdashalphaleftrightarroweta;Gammavdasheta}{Gammavdashalpha}

（10） leftrightarrow 引入律： frac{Gamma,alphavdasheta;Gamma,etavdashalpha}{Gammavdashalphaleftrightarroweta}

3.4 例子

以上，我們定義了命題邏輯的自然演繹系統 N ，

它比命題邏輯形式系統 P 更複雜一些，但是這兩個系統是等價的。

我們來看一個例子。

求證， alpha oeta,alphavdasheta 是一個定理。

證明：

首先，我們根據包含律有，

alpha oeta,alphavdashalpha oeta

alpha oeta,alphavdashalpha

然後，根據這兩個結論，以及 o 消去律，就有，

alpha oeta,alphavdasheta 。

證畢。

4. 系統N和系統P的等價性

本文我們介紹了兩個形式系統，

命題邏輯形式系統 P ，以及命題邏輯的自然演繹系統 N ，

可以證明，對於 P （或 N ）中的公式 alpha ， vdash_Nalpha 當且僅當 vdash_Palpha 。

因此，這兩個系統中的定理集是一樣的，

某個定理在 P 中可證，當且僅當在 N 中也可證。

其中，我們令，

egalpha oeta ，表示 alphaloreta ，

eg( egalphalor egeta) ，表示 alphalandeta ，

(alpha oeta)land(eta oalpha) ，表示 alphaleftrightarroweta 。

對於這兩個系統而言，如上文所示，

我們只進行了符號的推導操作，即對公式進行形式證明，

至於這些符號到底代表什麼意思，我們卻故意沒有提及。

我們並沒有說 lor 表示「或」，也沒有說 land 表示「與」，

在學數理邏輯的時候，一開始就將形式系統與它的語義模型相區分，

是非常有益的，後文我們將看到這樣做的好處。

5. 總結

本文介紹了命題邏輯，以及與之相關的兩個形式系統 P 和 N ，

和 lambda_eta ， CL_w 一樣，我們採用了公理化的方式構建它們，

這樣得到的形式系統，只是符號演算，還沒有被賦予特定的語義，

下文我們開始介紹一階謂詞邏輯。

參考

離散數學教程

數理邏輯

Proof calculus

Hilbert system

Natural deduction

Sequent calculus

Practical Foundations for Programming Languages

Lambda-Calculus and Combinators，an Introduction

下一篇：你好，類型（五）：Predicate logic


推薦閱讀：

TAG:邏輯 | 證明 |