陳鈺

1 引言

直覺(jué)主義邏輯（Intuitionistic Logic,簡(jiǎn)稱Int）相對(duì)于滿足賦值單調(diào)性的自返和傳遞的克里普克模型類是可靠且完全的。所謂賦值單調(diào)性，指的是如果一個(gè)命題變?cè)猵 在一個(gè)點(diǎn)w 上為真，那么p 在w 的每一個(gè)可及點(diǎn)上都為真。（[4]）將直覺(jué)主義邏輯的克里普克模型類擴(kuò)大為滿足賦值單調(diào)性的傳遞模型類，則可以得到一個(gè)比直覺(jué)主義邏輯更弱的邏輯——維瑟（A.Visser）在[21]中提出的基本命題邏輯（Basic Propositional Logic，簡(jiǎn)稱BPL）。克羅西（G.Crosi）在[6]中研究了一些現(xiàn)在所說(shuō)的亞直覺(jué)主義邏輯（Subintuitionistic Logics），將其稱之為弱邏輯。亞直覺(jué)主義邏輯與直覺(jué)主義邏輯和基本命題邏輯一樣，其蘊(yùn)涵也是嚴(yán)格蘊(yùn)涵，而非實(shí)質(zhì)蘊(yùn)涵。使用嚴(yán)格蘊(yùn)涵和嚴(yán)格否定但不使用實(shí)質(zhì)蘊(yùn)涵和實(shí)質(zhì)否定的命題邏輯一般也稱為嚴(yán)格蘊(yùn)涵邏輯。（[9]）

克羅西在[6]中給出的最弱的邏輯是F。雷斯塔爾（G.Restall）在[17]中也研究了亞直覺(jué)主義邏輯，并且其提出的邏輯SJ 與F 是等價(jià)的（[22]）。就F 的證明系統(tǒng)而言，克羅西（[6]）和雷斯塔爾（[17]）給出的是希爾伯特式公理系統(tǒng)。萬(wàn)星（H.Wansing，[22]）給出了F 及其一些擴(kuò)張的顯示演算（Display Calculus）。塞拉特（C.Cerrato）給出了嚴(yán)格蘊(yùn)涵邏輯的自然演繹系統(tǒng)。（[3]）石垣和鹿島（R.Ishigaki&R.Kashima）給出了嚴(yán)格蘊(yùn)涵邏輯的矢列演算，這些演算使用的是基于集合的矢列。（[9]）此外，他們運(yùn)用語(yǔ)義的方法證明了切割規(guī)則的可容許性在這些演算中成立。馬明輝和趙之光（M.Ma&Z.Zhao）使用[5]中提出的統(tǒng)一對(duì)應(yīng)理論（unified correspondence theory）建立起嚴(yán)格蘊(yùn)涵邏輯的模塊化的無(wú)切割規(guī)則的矢列演算，而且這些演算中關(guān)于蘊(yùn)涵的規(guī)則分為左引入規(guī)則和右引入規(guī)則。（[12]）山崎和佐野（S.Yamasaki&K.Sano）給出了F 和其他嚴(yán)格蘊(yùn)涵邏輯的G3-型加標(biāo)的矢列演算，并且證明切割規(guī)則在這些演算中是可容許的。（[23]）在最近的研究中，艾博利安和艾利扎德（N.Aboolian&M.Alizadeh）沿著佐佐木（K.Sasaki，[19]）以及阿蓋伊和阿德希爾（M.Aghaei&M.Ardeshir，[2]）提出的方法，通過(guò)引入受限的實(shí)質(zhì)蘊(yùn)涵來(lái)刻畫嚴(yán)格蘊(yùn)涵，從而建立起F 的G3-型矢列演算GF。（[1]）據(jù)我所知，除此之外，沒(méi)有學(xué)者給出F 的其他的G3-型（不加標(biāo)的）矢列演算，但是山崎和佐野（[24]）以及朱吟秋（[26]）給出了BPL 的G3-型矢列演算G3BPL。

本文基于山崎和佐野（[24]）以及朱吟秋（[26]）給出F 的G3-型矢列演算G3F。實(shí)際上，通過(guò)對(duì)G3BPL 中的蘊(yùn)涵規(guī)則(B→)進(jìn)行修改就可以得到G3F 的蘊(yùn)涵規(guī)則，并且G3F 的蘊(yùn)涵規(guī)則嚴(yán)格簡(jiǎn)單于G3BPL 中的蘊(yùn)涵規(guī)則。另外，這組規(guī)則都源自石井（K.Ishii）等學(xué)者在[10]中給出的BPL 的矢列演算LBP。更為重要的是，本文通過(guò)語(yǔ)法的方法證明切割規(guī)則在G3F 中是可容許的。眾所周知，直覺(jué)主義邏輯可以通過(guò)哥德?tīng)枿C麥金西–塔斯基翻譯（見(jiàn)定義5.2）嵌入到模態(tài)邏輯S4 中。（[7,13,20]）本文根據(jù)特羅埃斯特拉和施維滕伯格（A.Troelstra&H.Schwichtenberg）的思路（[20]），運(yùn)用證明論的方法建立起從G3F 到正規(guī)模態(tài)邏輯K 的矢列演算G3K 的嵌入定理的一個(gè)新證明。嵌入定理的一個(gè)重要作用就是可以將G3F 中的切割規(guī)則的可容許性證明規(guī)約到G3K 中。另外，本文還討論了弱邏輯F 的一些擴(kuò)張及其與模態(tài)邏輯的關(guān)系。具體而言，首先建立起這些邏輯的G3-型矢列演算，然后利用證明論的方法建立它們通過(guò)哥德?tīng)枿C麥金西–塔斯基翻譯到模態(tài)邏輯的嵌入定理，從而證明切割規(guī)則在這些矢列演算中的可容許性。

本文結(jié)構(gòu)安排如下。第2 節(jié)介紹弱邏輯F 的語(yǔ)言和語(yǔ)義。在第3 節(jié)中將給出F的G3-型矢列演算G3F，并證明切割規(guī)則在G3F 中是可容許的。第4 節(jié)將證明G3F與希爾伯特式公理系統(tǒng)HF 之間的等價(jià)性，從而證明G3F 的可靠性與完全性。第5 節(jié)運(yùn)用證明論的方法證明弱邏輯F 可以嵌入到正規(guī)模態(tài)邏輯K 中。第6 節(jié)討論了弱邏輯F 的一些擴(kuò)張的G3-型矢列演算，并探討了它們與模態(tài)邏輯之間的關(guān)系。第7 節(jié)是結(jié)語(yǔ)和將來(lái)的工作。

2 弱邏輯F

2.1 語(yǔ)言和語(yǔ)義

以下介紹弱邏輯F 的語(yǔ)言和語(yǔ)義。

定義2.1(形式語(yǔ)言LF).令Prop 為可數(shù)的命題變?cè)xF 的語(yǔ)言LF中的公式如下：

其中p ∈Prop。?A 定義為(A→⊥), ?定義為?⊥，(A ?B) 定義為((A→B)∧(B→A))。

本文約定，公式的最外層括號(hào)可以省略。而且為了簡(jiǎn)化表達(dá)式，再約定∧,∨的聯(lián)結(jié)比→優(yōu)先。例如，((A∧B)→C)可以寫成A∧B→C。

下面介紹F 的語(yǔ)義。

定義2.2(框架,模型).一個(gè)框架F 是一個(gè)有序?qū)?W,R)，其中W 是非空點(diǎn)集，R ?W ×W?？蚣蹻=(W,R)上的賦值是一函數(shù)V :Prop ?→2W。

一個(gè)模型M 是一個(gè)有序?qū)?F,V),其中V 是F 上的賦值函數(shù)。

定義2.3(公式的真).令M=(F,V)為任意模型以及w ∈W。公式A 在M 中的點(diǎn)w 上為真（寫作M,w ?A）歸納定義如下：

M,w ?p當(dāng)且僅當(dāng) w ∈V(p)，其中p ∈Prop；

M,w ?⊥即，并非M,w ?⊥；

M,w ?A∧B 當(dāng)且僅當(dāng) M,w ?A 并且M,w ?B；

M,w ?A∨B 當(dāng)且僅當(dāng) M,w ?A 或者M(jìn),w ?B；

M,w ?A→B 當(dāng)且僅當(dāng) 對(duì)任意v ∈W，wRv，若M,v ?A 則M,v ?B。

令M=(F,V)為任意模型。如果對(duì)所有w ∈W 都有M,w ?A，就說(shuō)公式A 在模型M 中為真（寫作M ?A）。如果公式A 在模型M 上不真，就說(shuō)公式A被模型M 反駁或者模型M 是公式A 的反模型。如果公式A 在基于框架F 的每一個(gè)模型上都為真，就說(shuō)公式A 在框架F 上是有效的（寫作F ?A）。令F 為一個(gè)框架類，如果公式A 在F 中的每一個(gè)框架上都是有效的，則說(shuō)A 是F-有效的（寫作F ?A）。

2.2 弱邏輯F 的希爾伯特式公理系統(tǒng)HF

現(xiàn)在介紹克羅西（[6]）給出的F 的希爾伯特式公理系統(tǒng)HF。

定義2.4(希爾伯特式公理系統(tǒng)HF).希爾伯特式公理系統(tǒng)HF 包含如下公理模式和推理規(guī)則：

1.A→A

2.(A→B)∧(B→C)→(A→C)

3.A∧B→A

4.A∧B→B

5.(A→B)∧(A→C)→(A→B∧C)

6.A→A∨B

7.B→A∨B

8.(A→C)∧(B→C)→(A∨B→C)

9.A∧(B∨C)→(A∧B)∨(A∧C)

10.⊥→A

推理規(guī)則

HF 中證明和定理的概念與通常定義的一樣。如果公式A 是HF 的一個(gè)定理，寫作?HFA。

定理2.1(HF 的可靠性與完全性，[6]).令FF為所有框架的類。對(duì)任意公式A 都有：?HFA 當(dāng)且僅當(dāng)FF?A。

3 F 的矢列演算G3F

本節(jié)將給出F 的矢列演算G3F。首先引入一些概念。

定義3.1(矢列).給定有窮的公式多重集（multiset）Γ 和?,一個(gè)矢列是形如Γ ??的表達(dá)式,其中Γ 和?分別稱作矢列的前件和后件。

本文約定，矢列?！圈???∪Π（其中∪表示多重集的并）簡(jiǎn)記為Γ,Σ ??,Π。例如，A,Γ,A ?A,?,A,B 表示的是前件為Γ ∪{A,A}，后件為?∪{A,A,B}的矢列。另外，用≡表示兩表達(dá)式相等。對(duì)有窮的公式多重集Γ，∧Γ(∨Γ)表示Γ 中所有出現(xiàn)的公式的任意順序的合?。ㄎ鋈。?。特殊地，∧?≡?，∨?≡⊥。矢列Γ ??對(duì)應(yīng)的公式定義為∧?！?。

定義3.2(子公式多重集).對(duì)任意LF公式A，A 的子公式多重集Sub(A)歸納定義如下：

? 如果A ≡p（其中p ∈Prop），那么Sub(A)={p}，

? 如果A ≡⊥，那么Sub(A)={⊥}，

? 如果A ≡B ?C（其中?∈{∧,∨,→}），那么Sub(A)={B ?C}∪Sub(B)∪Sub(C)。

有窮的公式多重集Γ ≡A1,...,An的子公式多重集。

一個(gè)有n 個(gè)前提的規(guī)則r 有如下形式：

其中Γ1??1，...，Γn??n為規(guī)則r 的前提，Γ ??為r 的結(jié)論。為了書(shū)寫的簡(jiǎn)便，可以把它簡(jiǎn)寫成：

有0 個(gè)前提的規(guī)則又稱公理。

現(xiàn)在介紹F 的矢列演算G3F。

定義3.3(G3F).G3F 的公理和規(guī)則定義如下：

公理

邏輯規(guī)則

在G3F 的公理和規(guī)則中，Γ 和?稱為語(yǔ)境。在一個(gè)前提數(shù)> 0 的規(guī)則的結(jié)論中，如果出現(xiàn)的公式在前提中有對(duì)應(yīng)的真子公式出現(xiàn)，則稱該公式為這個(gè)規(guī)則的主公式（principal formula），其對(duì)應(yīng)的出現(xiàn)在前提中的真子公式稱為活動(dòng)公式（active formula）。如果出現(xiàn)的公式同時(shí)在前提中也出現(xiàn)，則稱該公式為邊公式（side formula）。如果出現(xiàn)的公式既不是主公式也不是邊公式，稱該公式為弱化公式（weakening formula）。特殊地，在公理中，Γ 和?中出現(xiàn)的公式都是弱化公式，Id 中兩次出現(xiàn)的公式p 都是主公式，L⊥中出現(xiàn)的公式⊥為主公式。在規(guī)則(→)中，C1→D1,...,Cn→Dn和A→B 都是主公式。在這里，用{Ci→Di}i∈n表示結(jié)論的前件中的這n 個(gè)主公式，因此，前件中的每一個(gè)主公式都被n 中的一個(gè)元素標(biāo)記。

G3F 中的規(guī)則(→)有點(diǎn)復(fù)雜，現(xiàn)對(duì)其作出一些解釋。在規(guī)則(→)中，每一個(gè)前提被n 中的一個(gè)子集索引，對(duì)s ?n，s 挑出指標(biāo)n 中的子集，然后將被挑出的蘊(yùn)含式的前件放在被s 索引的前提的后件（即{Cj}j∈s）中，同時(shí)將未被挑出的蘊(yùn)含式的后件放在該前提的前件（即{Dk}k∈ns）中。容易看出，該規(guī)則的前提數(shù)量由n 決定，即如果該規(guī)則結(jié)論的前件中有n 個(gè)主公式，則該規(guī)則的前提數(shù)量為2n。再通過(guò)一些例子進(jìn)行說(shuō)明。當(dāng)n=0,1,2 時(shí)，規(guī)則(→)的形式分別如下所示：

注1.正如在引言中提到的，本文是通過(guò)對(duì)山崎和佐野（[24]）和朱吟秋（[26]）給出的G3BPL 中的蘊(yùn)涵規(guī)則進(jìn)行修改而得到G3F 的蘊(yùn)涵規(guī)則。因此，只需要將G3F中的規(guī)則(→)替換為如下規(guī)則(B→)就可以得到G3BPL：

注2.石垣和鹿島（[9]）給出了F 的矢列演算GKI并且證明了它的可靠性與完全性。而克羅西（[6]）證明了HF 的可靠性和完全性，因此，易知GKI和HF 是等價(jià)的。根據(jù)本文在第4 節(jié)中證明的G3F 與HF 之間的等價(jià)性可知，GKI與G3F 是等價(jià)的。

GKI使用集合矢列。而G3F 使用多重集矢列，是[15,20]中的G3-型演算。G3-型演算的一個(gè)特點(diǎn)就是將結(jié)構(gòu)規(guī)則吸收在公理和邏輯規(guī)則中。另外，本文與[9]最重要的一個(gè)區(qū)別是，本文給出了G3F 中切割規(guī)則可容許性的純語(yǔ)法的證明，這也是本文的主要貢獻(xiàn)之一，而[9]則是通過(guò)語(yǔ)義的方法證明切割規(guī)則在GKI中是可容許的。

定義3.4(“矢列的”證明).G3F 中的一個(gè)證明是一棵有窮的有向樹(shù)，該樹(shù)的每一個(gè)節(jié)點(diǎn)上都是矢列，并且每個(gè)節(jié)點(diǎn)上的矢列作為結(jié)論，與其所有子節(jié)點(diǎn)上的矢列作為前提，構(gòu)成對(duì)G3F 中一規(guī)則的一個(gè)運(yùn)用。每一個(gè)證明被稱為其根矢列的證明，并且0 前提規(guī)則的結(jié)論是證明（樹(shù)）的葉子。一個(gè)證明的高度h 是該證明（樹(shù)）中最長(zhǎng)有向路徑的節(jié)點(diǎn)之間的距離，其中公理的高度為0。矢列Γ ??在G3F 中是可證的（寫作?G3FΓ ??）當(dāng)且僅當(dāng)Γ ??在G3F 中有一個(gè)證明。此外，用?hΓ ??表示Γ ??在G3F 中有一個(gè)高度至多為h 的證明。

容易觀察到，在G3F 的規(guī)則中，前提中出現(xiàn)的每個(gè)公式都是結(jié)論中出現(xiàn)的公式的子公式。因此，G3F 具有子公式性質(zhì)。

命題3.1(子公式性質(zhì)).如果Γ ??在G3F 中有一個(gè)證明，那么該證明中出現(xiàn)的每一個(gè)公式都是Γ,?的子公式。

這樣，給定一個(gè)矢列Γ ??，可以在G3F 中構(gòu)造一棵從下到上的證明搜索樹(shù)，因而F 是可判定的。

定義3.5(規(guī)則的可容許、保高可容許、保高可逆).對(duì)任意規(guī)則r，(1)如果該規(guī)則的所有前提在G3F 中是可證的蘊(yùn)涵其結(jié)論在G3F 中也是可證的，則稱規(guī)則r 在G3F中是可容許的。如果該可容許規(guī)則r 還滿足：若其前提在G3F 中有高度≤h 的證明，其結(jié)論在G3F 中也有高度≤h 的證明，則稱該規(guī)則在G3F 中是保高可容許的。(2)如果該規(guī)則的結(jié)論在G3F 中有高度≤h 的證明蘊(yùn)涵其所有前提在G3F 中也有高度≤h 的證明，則稱該規(guī)則在G3F 中是保高可逆的。

定義3.6(公式的度).一個(gè)公式A 的度（degree）dg(A)定義如下：

? dg(⊥)=0,

? dg(p)=1，其中p ∈Prop,

? dg(A ?B)=dg(A)+dg(B)+1，其中?∈{∧,∨,→}。

定義3.7(切割規(guī)則).切割規(guī)則(Cut)定義如下：

其中公式A 稱為切割公式。切割公式的度稱為(Cut)的秩（rank），(Cut)的前提的證明高度之和稱為(Cut)的級(jí)（level）。

如果(Cut)的秩為r 且級(jí)為l，則其等級(jí)d（grade）為ω·r+l（其中ω 為最小的無(wú)窮序數(shù)）。用表示將(Cut)的等級(jí)限制為≤ω·r+l，G3F⊕(Cut)rl表示通過(guò)受限等級(jí)的擴(kuò)張G3F 得到的演算，G3F⊕(Cut)表示通過(guò)不受限等級(jí)的(Cut)擴(kuò)張G3F 得到的演算。

接下來(lái)將證明切割規(guī)則在G3F 中是可容許的，這也是本文的一個(gè)主要定理。但在這之前，首先證明一些需要用到的引理。

引理3.1.對(duì)任意公式A，都有：?G3FA,Γ ??,A。

證明.施歸納于公式A 的復(fù)雜度?？紤]A ≡B→C 的情形，那么最后一步如下所示：

運(yùn)用歸納假設(shè),B ?C,B 和C,B ?C 是可證的。因此Γ,B→C ? B→C,?也是可證的.

引理3.2(弱化規(guī)則保高可容許).令Γ,?為公式多重集，A 為L(zhǎng)F中的公式。在G3F或（其中r,l ∈N）中，有

(1) 如果?hΓ ??,那么?hA,Γ ??。

(2) 如果?hΓ ??,那么?hΓ ??,A。

證明.選證(1)。(2)的證明與(1)類似。施歸納于h。如果h=0，那么Γ ??是公理，因此A,Γ ??也是公理。

如果h > 0。如果在Γ ??的證明中，最后運(yùn)用的規(guī)則是L∧,R∧,L∨,R∨或中的一個(gè),那么先運(yùn)用歸納假設(shè)于前提中，再對(duì)得到的結(jié)果運(yùn)用該規(guī)則即可。

如果最后運(yùn)用的規(guī)則是(→)。不失一般性，令Γ ≡?！?{Ci→Di}i∈n以及?≡E→F,?′,那么有：

由于[?h?1{Dk}k∈ns,E ?F,{Cj}j∈s]s?n，則運(yùn)用規(guī)則(→)得到?h?！洹?{Ci→Di}i∈n?E→F,?′，其中?！洹洹訟,Γ′。

在證明收縮規(guī)則保高可容許之前，先引入如下可逆引理。

引理3.3(可逆引理).在G3F 或G3F⊕(Cut)rl（其中r,l ∈N）中，除規(guī)則(→)外的所有邏輯規(guī)則都是保高可逆的。

證明.選證規(guī)則L∨是保高可逆的，其余規(guī)則的證明類似。因此只需證：如果?hA∨B,Γ ??,那么有：?hA,Γ ??以及?hB,Γ ??。

施歸納于h。如果h=0，那么A∨B,Γ ??是公理，則A,Γ ??和B,Γ ??也是公理。

如果h>0。如果A∨B 是主公式或弱化公式，顯然。

如果A∨B 是邊公式，則最后運(yùn)用的規(guī)則不可能是公理或(→)，則直接運(yùn)用歸納假設(shè)于該規(guī)則的前提，然后對(duì)得到的結(jié)果運(yùn)用該規(guī)則即可。

引理3.4(收縮規(guī)則保高可容許).令Γ,?為公式多重集，A 為L(zhǎng)F中的公式。在G3F或（其中r,l ∈N）中，有

(1) 如果?hA,A,Γ ??,那么?hA,Γ ??。

(2) 如果?hΓ ??,A,A,那么?hΓ ??,A。

證明.同時(shí)施歸納于(1)和(2)中的h。如果h=0，顯然。

如果h>0。(1)如果A 的兩次出現(xiàn)的其中一次是弱化公式，則在運(yùn)用同樣的規(guī)則于前提得到的結(jié)論中且不引入A 作為弱化公式即可。如果A 的兩次出現(xiàn)都是邊公式，則最后運(yùn)用的規(guī)則一定是L∧,R∧,L∨,R∨或中的一個(gè)，那么由歸納假設(shè)易得。如果A 的兩次出現(xiàn)其中一次是邊公式，另一次是主公式，則最后運(yùn)用的規(guī)則一定是L∨或L∧，則根據(jù)引理3.3 和歸納假設(shè)可得。如果A 的兩次出現(xiàn)都是主公式。不妨令其分別為Cu→Du,Cv→Dv，則有

其中Γ′,{Ci→Di}i∈n{u,v}≡Γ 以及E→F,?′≡?。

這時(shí)有：對(duì)任意r ?n，如果u,v/∈r，則有

由歸納假設(shè)得?h?1{Dk}k∈(n ){u,v},Du,E ?F,{Cj}j∈r，

因此有[?h?1{Dk}k∈n {u,v},Du,E ?F,{Cj}j∈r]r?(n{u,v})；

對(duì)任意t ?n，如果u,v ∈t，則有

由歸納假設(shè)得?h?1{Dk}k∈n ,E ?F,Cu,{Cj}j∈t{u,v}。

因此有[?h?1{Dk}k∈n ,E ?F,Cu,{Cj}j∈t{u,v}]u,v∈t,t?n；

運(yùn)用規(guī)則(→)可以得到?！?{Ci→Di}i∈n{u,v},Cu→Du,?E→F,?′。

(2) 如果A 的兩次出現(xiàn)的其中一次是弱化公式或者邊公式，證明與(1)類似。如果A 的兩次出現(xiàn)都是主公式，但這顯然不可能，因?yàn)镚3F 或的規(guī)則沒(méi)有結(jié)論的后件出現(xiàn)兩個(gè)（及兩個(gè)以上）主公式的情況。

定理3.5.規(guī)則(Cut)在G3F 中是可容許的。

證明.對(duì)(Cut)的秩和級(jí)進(jìn)行雙重歸納。由于A 在左右前提中的每一次出現(xiàn)可以是主公式、邊公式或弱化公式中的一種，因此有以下三種情況：

情況1：A 在(Cut)的左前提或右前提中為弱化公式。顯然有Γ ??。

情況2：A 在(Cut) 的左前提或右前提中為邊公式。由于規(guī)則(→) 沒(méi)有邊公式出現(xiàn)，因此得到左或右前提的最后一步運(yùn)用的規(guī)則必定是L∧,R∧,L∨,R∨或秩

然后將(Cut)規(guī)則的運(yùn)用向上置換可以得到

情況3：A 在(Cut)的左前提和右前提中都為主公式?？紤]A 是蘊(yùn)含式的情況，不妨令A(yù) ≡Cz→Dz，Γ ≡Θ,{Gi′→Hi′}i′∈n≡Π,{Ci→Di}i∈m，?≡E→F,Σ，則有

將[{Dk}k∈m ,E ?F,{Cj}j∈t]t?m劃分成兩部分：[{Dk}k∈(m{z}) ,E ?F,Cz,{Cj}j∈t]t?m{z}以及[Dz,{Dk}k∈(m{z}) ,E ?F,{Cj}j∈t]t?m{z}。容易知道，這兩部分包含的矢列數(shù)量皆為2m?1。

對(duì)任意s ?n 以及t ?m {z}，令Λ1≡{Dk}k∈(m{z}) ,E 以及Λ2≡F,{Cj}j∈t，則可以得到：

然后有

由于有2n+m?1個(gè)上述形式的子證明，因此其結(jié)論也有2n+m?1個(gè)。

現(xiàn)在令n′= {1,...,n,n+1,...,n+z ?1,n+z +1,...,n+m}。對(duì)任意i′′∈n′，定義Gi′′和Hi′′如下：

然后有

因此有Θ,{Gi′→Hi′}i′∈n,Π,{Ci→Di}i∈m{z}?E→F,Σ，運(yùn)用規(guī)則(C)可以得到Θ,{Gi′→Hi′}i′∈n?E→F,Σ。

4 G3F 與HF 之間的等價(jià)性

本節(jié)證明矢列演算G3F 與希爾伯特式公理系統(tǒng)HF 是等價(jià)的。

引理4.1.對(duì)任意公式A,如果?HFA,那么?G3F?A。證明.施歸納于HF 中公式A 的證明結(jié)構(gòu)。容易看到，對(duì)HF 中的所有公理A，都有?G3F?A。例如,(A→B)∧(A→C)→(A→B∧C)在G3F 中的一個(gè)證明如下所示：

(AF) 的情形是平凡的。至于(MP)，假設(shè)?G3F?Ai（其中1 ≤i ≤n）和?G3F?A1∧···∧An→B，運(yùn)用有窮多次規(guī)則R∧得到?G3F?A1∧···∧An，因此有?G3F?A1∧···∧An,B。而得到?A1∧···∧An→B 最后一步運(yùn)用的規(guī)則一定是(→)，因此?G3FA1∧···∧An?B。運(yùn)用規(guī)則(Cut)可以得到?G3F?B。

在證明引理4.1 的相反方向之前，需要證明一系列引理。

引理4.2.對(duì)任意公式A,B,如果?HFA 以及?HFB,那么?HFA∧B。

證明.運(yùn)用(MP)到?HFA,?HFB 以及?HFA∧B→A∧B 即可。

引理4.3([6]).對(duì)任意公式A,B,C, 如果?HFA→B 以及?HFB→C, 那么?HFA→C。

證明.假設(shè)?HFA→B 和?HFB→C。根據(jù)引理4.2 有?HF(A→B)∧(B→C)。因?yàn)?HF(A→B)∧(B→C)→(A→C)。運(yùn)用(MP)可得?HFA→C。

引理4.4.對(duì)任意公式A,B,C,D，如果?HFA→B，那么?HFA∧C→B∨D。

證明.假設(shè)?HFA→B。因?yàn)?HFA∧C→A，根據(jù)引理4.3 有?HFA∧C→B，又?HFB→B∨D，再根據(jù)引理4.3有?HFA∧C→B∨D。

引理4.5.對(duì)任意公式A,B,C, 如果?HFA→B 和?HFA→C, 那么?HFA→B∧C。

證明.假設(shè)?HFA→B 和?HFA→C。由于?HF(A→B)∧(A→C)→(A→B∧C)，運(yùn)用(MP)得?HFA→B∧C。

引理4.6.對(duì)任意公式A,B,C,D，如果?HFA→(B→C)和?HFA→(C→D)，那么?HFA→(B→D)。

證明.假設(shè)?HFA→(B→C)和?HFA→(C→D)，根據(jù)引理4.5，可以得到?HFA→(B→C)∧(C→D)。又因?yàn)?HF(B→C)∧(C→D)→(B→D)，根據(jù)引理4.3，可得?HFA→(B→D)。

引理4.7.對(duì)任意公式A,B,C,D1,D2，如果?HFA→B∨C，?HFB→D1和?HFC→D2，那么?HFA→D1∨D2。

證明.假設(shè)?HFB→D1和?HFC→D2，則易知?HFB∨C→D1∨D2。又因?yàn)?HFA→B∨C，根據(jù)引理4.3 得?HFA→D1∨D2。

引理4.8.對(duì)任意公式A,B,C,D1,D2，如果?HFA→(B→C∨D1)和?HFA→(B→C∨D1)，那么?HFA→(B→C∨(D1∧D2))。

證明.首先證明?HF(C∨D1)∧(C∨D2)→C∨(D1∧D2)。

因?yàn)?HF(C∨D1)∧(C∨D2)→((C∨D1)∧C)∨((C∨D1)∧D2)，?HF(C∨D1)∧C→(C∧C)∨(C∧D1)，?HF(C∨D1)∧D2→(C∧D2)∨(D1∧D2)，由引理4.7 得?HF(C∨D1)∧(C∨D2)→(C∧C)∨(C∧D1)∨(C∧D2)∨(D1∧D2)。易知?HFC∧C→C，?HFC∨(C∧Di)→C（其中i ∈{1,2}），可得?HF(C∨D1)∧(C∨D2)→C∨(D1∧D2)。

假設(shè)?HFA→(B→C∨D1)和?HFA→(B→C∨D1)，易知?HFA→(B→(C∨D1)∧(C∨D2))。又因?yàn)?HFA→((C∨D1)∧(C∨D2)→C∨(D1∧D2))，根據(jù)引理4.6 可得?HFA→(B→C∨(D1∧D2))。

引理4.9([6]).對(duì)任意公式A,B,C,如果?HFA→B，那么?HF(C→A)→(C→B)。

證明.假設(shè)?HFA→B。運(yùn)用(AF) 可以得到?HF(C→A)→(A→B)。因?yàn)?HF(C→A)→(C→A),那么根據(jù)引理4.5 有?HF(C→A)→((C→A)∧(A→B))。因?yàn)?HF(C→A)∧(A→B)→(C→B)，由引理4.3 可得?HF(C→A)→(C→B)。

引理4.10.對(duì)任意公式A,B 以及k ∈n={1,...,n}，如果?HF∧{Ci→Di}i∈n→(A→B∨Ck)那么?HF∧{Ci→Di}i∈n→(A→B∨Dk)。

證明.首先，(Ck→Dk)→((B→B∨Dk)∧(Ck→B∨Dk)在HF 中的證明如下：

因?yàn)?HF(B→B∨Dk)∧(Ck→B∨Dk)→(B∨Ck→B∨Dk)以及?HF∧{Ci→Di}i∈n→(Ck→Dk)，根據(jù)引理4.3 有?HF

∧{Ci→Di}i∈n→(B∨Ck→B∨Dk)。此外，?HF∧{Ci→Di}i∈n→(A→B∨Ck)，然后根據(jù)引理4.5有?HF∧{Ci→Di}i∈n→((A→B∨Ck)∧(B∨Ck→B∨Dk))。又因?yàn)?HF(A→B∨Ck)∧(B∨Ck→B∨Dk)→(A→B∨Dk)，根據(jù)引理4.3 可以得到?HF∧{Ci→Di}i∈n→(A→B∨Dk)。

引理4.11.對(duì)任意公式A,B,C 和D,如果?HFC→(A∧D→B)那么?HFC→(A∧(B∨D)→B)。

證明.首先考慮HF 中的如下證明：

由于?HF(A∧B→B)∧(A∧D→B)→((A∧B)∨(A∧D)→B)，然后根據(jù)引理4.3，可以得到?HFC→((A∧B)∨(A∧D)→B)。然后有

由于?HF(A∧(B∨D)→(A∧B)∨(A∧D))∧((A∧B)∨(A∧D)→B)→(A∧(B∨D)→B)，根據(jù)引理4.3 得到?HFC→(A∧(B∨D)→B)。

引理4.12.對(duì)任意公式A，如果?G3F?A,那么?HFA。

證明.令∧Γ(∨Γ)為Γ中∧所有公∨式的合?。ㄎ鋈。?。證明對(duì)任意矢列Γ ??,如果?G3FΓ??那么?HF?！?。

施歸納于Γ ??在G3F 中的證明高度。這里只考慮規(guī)則為(→)時(shí)的情況。根據(jù)歸納假設(shè)，對(duì)所有s ?n，有?HF∧({Dk}k∈ns,A)→∨(B,{Cj}j∈s)。然后運(yùn)用有窮多次(AF)可得，對(duì)任意s ?n，有?HF

∧{Ci→Di}i∈n→(∧({Dk}k∈ns,A)→∨(B,{Cj}j∈s))。然后多次運(yùn)用引理4.10 可得：對(duì)所有s ? n，?HF∧{Ci→Di}i∈n→(∧({Dk}k∈ns,A)→∨(B,{Dj}j∈s))。因此只需證：

然后取s=?，即可得到?HF∧{Ci→Di}i∈n→(A→B)。最后運(yùn)用有窮多次引理4.4，有?HF∧(Γ,{Ci→Di}i∈n)→∨(A→B,?)。

現(xiàn)在證明(#)。首先根據(jù)基數(shù)大小將n 的所有子集按如下順序排列：

令sm是n 的第m（1 ≤m ≤2n)個(gè)子集。施歸納于m。

如果m=1,顯然有?HF∧{Ci→Di}i∈n→(A→∨(B,{Dj}j∈n))，因?yàn)閧Dk}k∈ns=?。

如果m > 1。由于?HF∧{Ci→Di}i∈n→(∧({Dk}k∈nsm,A)→∨(B,{Dj}j∈sm)),根據(jù)

引理4.11 可得令Dk1,Dk2,...,Dkk′為{Dk}k∈nsm中公式的一個(gè)枚舉。則對(duì)任意1 ≤l ≤k′,存在m′

因此根據(jù)引理4.1 和引理4.12 可以得到G3F 和HF 之間的等價(jià)性。

5 F 到模態(tài)邏輯K 的嵌入定理

命題模態(tài)語(yǔ)言L□由語(yǔ)言LF加上模態(tài)算子□組合而成。所有其他邏輯聯(lián)結(jié)詞以及模態(tài)算子◇與通常的定義一樣。

現(xiàn)在介紹正規(guī)模態(tài)邏輯K 的矢列演算G3K。

定義5.1(G3K).G3K 的公理和規(guī)則定義如下：

公理

邏輯規(guī)則

其中□Θ={□B |B ∈Θ}。

模態(tài)邏輯K 的矢列演算首先由萊萬(wàn)特（D.Leivant，[11]）,敏茲（G.Mints，[14]）以及桑賓和瓦倫蒂尼（G.Sambin&S.Valentini，[18]）給出。不過(guò)他們給出的矢列演算是基于集合的矢列而不是多重集的矢列，而且模態(tài)算子□的規(guī)則如下式：

G3K 中主公式、邊公式、弱化公式、證明、證明的高度以及規(guī)則的（保高）可容許等的定義與G3F 中的類似。此外，易知弱化、收縮和切割規(guī)則在G3K 中是可容許的。（[8]）

現(xiàn)在介紹哥德?tīng)枿C麥金西–塔斯基翻譯。（[20]）

定義5.2(翻譯τ).

令Γ ≡A1,···,An為有窮的公式多重集，定義Γτ:=,···,。

接下來(lái)將運(yùn)用證明論的方法證明弱邏輯F 可以通過(guò)哥德?tīng)枿C麥金西–塔斯基翻譯嵌入到模態(tài)邏輯K 中，即：對(duì)LF中的每個(gè)公式A，

注3.克羅西（[6]）定義了一個(gè)翻譯?，其與翻譯τ 的不同之處僅在于對(duì)原子命題的翻譯：p?:=p，并且通過(guò)模型論的方法證明F 可以通過(guò)翻譯?嵌入到模態(tài)邏輯K 中。而本文通過(guò)證明論的方法給出F 通過(guò)翻譯τ 嵌入到模態(tài)邏輯K 的新證明。

注4.山崎和佐野（[23]）定義了哥德?tīng)枿C麥金西–塔斯基翻譯的一個(gè)變種翻譯τ′，由于他們給出的是是加標(biāo)的矢列演算，因此與τ 的不同之處除對(duì)原子命題的翻譯(pτ′:=p∧□p)外，還引入了對(duì)加標(biāo)公式x:A 的翻譯：(x:A)τ′:=x:Aτ′，以及對(duì)關(guān)系原子公式xRy 的翻譯：(xRy)τ′:= xRy。然后他們證明F 的G3-型加標(biāo)矢列演算LG3F 可以通過(guò)翻譯τ′嵌入到模態(tài)邏輯K 的G3-型加標(biāo)矢列演算LG3K 中。而本文的證明使用的是不加標(biāo)的矢列演算。

為證明(???)，只需證明更一般的形式：?G3FΓ ??當(dāng)且僅當(dāng)?G3KΓτ??τ，其中Γ 和?為有窮的LF-公式多重集。

引理5.1.令Γ 和?為有窮的LF-公式多重集。如果?G3FΓ ??，那么?G3KΓτ??τ。

證明.施歸納于G3F 中Γ ??的證明高度h。

如果h=0。那么Γ ??是公理，則顯然有?G3KΓτ??τ。

如果h > 0?？紤]最后一步運(yùn)用的規(guī)則是(→) 的情況。令Γ ≡?！?{Ci→Di}i∈n以及?≡A→B,?′，那么有：

然后取m=n，可得(??)。

現(xiàn)在證明(???)。施歸納于m。當(dāng)m=0 時(shí)，由(?)直接可得。

假設(shè)m=k′時(shí)有：

其中k′={1,...,k′}。而其可以劃分為兩部分：

其中k′′={1,...,k,k+1}。因此有：

引理5.2.令Π 為有窮的原子公式集，p ∈Prop，Γ 為有窮的L□-公式集且Γ ∩(Prop ∪{⊥})=?，則如果?G3KΠ,Γ ?p，那么?G3KΠ ?p。

證明.施歸納于證明的高度易得。

引理5.3.令Π 為有窮的原子公式集，Θ1和Θ2為有窮的L□-公式集且Θi∩Prop=?(i ∈{1,2})，則如果?G3KΠ,Θ1?Θ2，那么?G3KΘ1?Θ2。

證明.施歸納于證明的高度易得。

引理5.4.令Γ 和?為有窮的LF-公式多重集，Π 和Σ 為有窮的原子公式多重集。如果?G3KΓτ,Π ??τ,Σ，那么?G3FΓ,Π ??,Σ。

證明.施歸納于G3K 中Γτ,Π ??τ,Σ 的證明高度h.

如果h=0。那么Γτ,Π ??τ,Σ 在G3K 中是公理，因此Γ,Π ??,Σ 在G3F也是公理。

如果h>0。注意到Π,Σ 是LF中的有窮的原子公式多重集，而Γτ和?τ中的公式的最外層聯(lián)結(jié)詞一定不是蘊(yùn)涵符號(hào)→。因此考慮如下情況：

(i)最后運(yùn)用的規(guī)則是(L∧),(R∧),(L∨)或(R∨)，

(ii)最后運(yùn)用的規(guī)則是(K□)。

情況(i)，考慮最后運(yùn)用的是(R∧)，其余情況類似。令?τ≡Aτ∧Bτ,?′τ，那么有

由歸納假設(shè)知，?G3FΓ,Π ?A,Σ 以及?G3FΓ,Π ?B,Σ，運(yùn)用規(guī)則R∧可得?G3FΓ,Π ?A,Σ。

情況(ii)。由于最后運(yùn)用的規(guī)則是(K□)，則主公式一定是模態(tài)前束公式。令Γτ≡?！洇?□Π′,以及?τ≡□A,?′τ，其中Π′為有窮的原子公式多重集，則有

若A ≡p，則根據(jù)引理5.2 有?G3KΠ′?p，由歸納假設(shè)得?G3FΠ′?p，運(yùn)用(W)得?G3FΓ′,Π′,{Ci→Di}i∈n,Π ?p,?′,Σ。

基于引理5.1和引理5.4，有如下定理：

定理5.5.令Γ 和?為有窮的LF-公式多重集。那么?G3FΓ ??當(dāng)且僅當(dāng)?G3KΓτ??τ。

上述定理的一個(gè)運(yùn)用就是可以用來(lái)證明切割規(guī)則(Cut)在G3F 中的可容許性。

定理5.6.規(guī)則(Cut)在G3F 中是可容許的。

證明.假設(shè)?G3FΓ ??,A 以及?G3FA,Γ ??，根據(jù)定理5.5 可得?G3KΓτ??τ,Aτ和?G3KAτ,Γτ??τ。又因?yàn)榍懈钜?guī)則(Cut)在G3K 中是可容許的，因此有?G3kΓτ??τ。因此，?G3FΓ ??。

6 討論

本文建立的這種G3-矢列演算可以擴(kuò)展到弱邏輯F 的一些擴(kuò)張上，比如克羅西（[6]）建立的邏輯FD、FR 以及FT 上。這三個(gè)邏輯希爾伯特式公理系統(tǒng)分別是在HF 的基礎(chǔ)上增加如下公理D′、T′以及4′得到：

與之對(duì)應(yīng)的G3-型矢列演算G3D′和G3T′分別是在G3F 的基礎(chǔ)上增加如下規(guī)則(→d)，(→t)得到：

而將G3F 中的規(guī)則(→)修改為如下規(guī)則(→4)并保持公理和其他規(guī)則不變，就可以得到邏輯FT 的矢列演算G34′：

克羅西（[6]）運(yùn)用模型論的方法證明了FD、FR 以及FT 可以通過(guò)翻譯?分別嵌入到模態(tài)邏輯D、T 以及K4 中。本文則運(yùn)用證明論的方法證明FD、FR 以及FT可以通過(guò)哥德?tīng)枿C麥金西–塔斯基翻譯分別嵌入到模態(tài)邏輯D、T 以及K4 中。

為此，先給出模態(tài)邏輯D、T 以及K4 的G3-型矢列演算G3D、G3T 和G34。G3D、G3T 分別在G3K 的基礎(chǔ)上增加如下規(guī)則(D□)和(L□)得到：

將G3K 中的規(guī)則(K□)修改為如下的規(guī)則(4□)就可以得到矢列演算G34：

矢列演算G3D、G3T 和G34 同樣具有良好的證明論性質(zhì)，即弱化、收縮和規(guī)則(Cut) 都是可容許的。（[16,25]）用G3[D′T′4′]表示一個(gè)矢列演算X ∈{G3D′,G3T′,G34′}，G3[DT4]類似。與第5 節(jié)中的證明類似，可以得到：

定理6.1.?G3[D′T′4′]Γ ??當(dāng)且僅當(dāng)?G3[DT4]Γτ??τ。

運(yùn)用定理6.1，可以得到：

定理6.2.規(guī)則(Cut)在G3[D′T′4′]中是可容許的。

7 結(jié)語(yǔ)

本文建立起弱邏輯F 的矢列演算G3F，并且證明結(jié)構(gòu)規(guī)則（弱化、收縮和切割規(guī)則）在該演算中是可容許的。事實(shí)上，本文給出了G3F 中切割規(guī)則可容許性的一個(gè)純語(yǔ)法的證明。同時(shí)，也證明了矢列演算G3F 與希爾伯特式公理系統(tǒng)HF 是等價(jià)的。此外，本文運(yùn)用證明論的方法給出一個(gè)通過(guò)哥德?tīng)枿C麥金西–塔斯基翻譯將弱邏輯F 嵌入到模態(tài)邏輯K 的新證明，并給出了F 的一些擴(kuò)張的G3-型矢列演算，探討了它們與模態(tài)邏輯之間的關(guān)系，即建立起它們到模態(tài)邏輯的嵌入定理。

在將來(lái)的工作中，我們考慮將本文的方法擴(kuò)展到其他嚴(yán)格蘊(yùn)涵邏輯，以此建立起這些邏輯的無(wú)切割規(guī)則的G3-型矢列演算。另外，切割消去定理的一個(gè)應(yīng)用就是給出克雷格內(nèi)插性質(zhì)（Craig Interpolation Property，簡(jiǎn)稱CIP）甚至比其更強(qiáng)的林登內(nèi)插性質(zhì)（Lyndon Interpolation Property，簡(jiǎn)稱LIP）的構(gòu)造性證明。艾博利安和艾利扎德（[1]）根據(jù)阿蓋伊和阿德希爾（[2]）證明BPL 具有CIP 的方法，給出與GF 等價(jià)的一個(gè)變種矢列演算GFs，在該演算中矢列的后件至多含有一個(gè)公式，從而構(gòu)造性的方法證明了F 具有LIP。然而，這類方法都是借助擴(kuò)張的語(yǔ)言，即引入受限的實(shí)質(zhì)蘊(yùn)涵，來(lái)刻畫嚴(yán)格蘊(yùn)涵，從而實(shí)現(xiàn)目的。但是本文建立的矢列演算不引入額外的語(yǔ)言，因此，能否根據(jù)本文的這類演算，運(yùn)用證明論的方法給出F 以及其他嚴(yán)格蘊(yùn)涵邏輯的內(nèi)插性質(zhì)（如果有的話）的構(gòu)造性證明也是一項(xiàng)有意義的工作。