帶否定算子的蘭貝克演算研究*

林哲

中山大學(xué)哲學(xué)系 中山大學(xué)邏輯與認(rèn)知研究所linzhe8@mail.sysu.edu.cn

梁飛?

山東大學(xué)哲學(xué)與社會(huì)發(fā)展學(xué)院philoliangfei@gmail.com

1 引言

J.Lambek于1958年為自然語(yǔ)言計(jì)算引入了一個(gè)句法演算系統(tǒng)。（[7]）現(xiàn)在這個(gè)系統(tǒng)被統(tǒng)稱為蘭貝克演算。在過(guò)去幾十年間，蘭貝克演算在語(yǔ)言邏輯領(lǐng)域受到了廣泛的重視，并且發(fā)展出許多重要的衍生和擴(kuò)張。W.Buszkowski于1995年在論文[1]中引入帶否定算子的蘭貝克演算作為學(xué)習(xí)范疇語(yǔ)法的核心類型邏輯。Buszkowski在其文章中提出，作為學(xué)習(xí)范疇語(yǔ)法的核心類型邏輯，其否定規(guī)則只需要滿足：

·置換性：假如類型A推出類型B，那么有?B推出?A，和

·雙重否定率：對(duì)任何類型A:??A=A。

有別于這種觀點(diǎn)，在蘭貝克演算的擴(kuò)張研究中，構(gòu)造性否定被廣泛關(guān)注即類型的否定被定義為?A:=A⊥。由于蘭貝克演算一般不具有交換律，因此會(huì)產(chǎn)生兩個(gè)否定。對(duì)這樣的擴(kuò)張的研究可以在文獻(xiàn)[3,6]中找到詳細(xì)的闡述。然而構(gòu)造性否定會(huì)帶來(lái)另外一個(gè)問(wèn)題，即蘭貝克矛盾律α·?α=⊥在邏輯中會(huì)變成有效。這條性質(zhì)缺乏語(yǔ)言邏輯研究的動(dòng)機(jī)，并且還會(huì)破壞一些范疇語(yǔ)法系統(tǒng)所需要的性質(zhì)，因此Buszkowski提出的蘭貝克否定擴(kuò)張更適合作為范疇語(yǔ)法的類型邏輯來(lái)研究。但是這種蘭貝克演算其判定性是未知的，并且缺乏優(yōu)秀的根岑演算系統(tǒng)。這會(huì)對(duì)基于這種類型邏輯范疇語(yǔ)法的進(jìn)一步研究帶來(lái)巨大的不便。

在本文我們選擇了一種極為接近Buszkowski提出的否定，稱為極小否定。極小否定滿足置換性和一半的雙重否定律：任何類型A推出類型??A，并且在極小否定中對(duì)任何??A類型都滿足上述否定的兩個(gè)性質(zhì)。極小否定的概念最早是由A.Kolmogorov（[5]）提出，再由I.Johansson（[4]）的研究發(fā)展得到。Johansson提出了一個(gè)極小邏輯，這一極小邏輯是由直覺主義邏輯刪除Duns Scotus公理A→(?A→B)得到。根據(jù)M.Dunn在其“Dunn’s Kite of Negations”（[2]）的研究，極小否定是一種否定，滿足如下性質(zhì)：A??B當(dāng)且僅當(dāng)B??A。在本文中，我們研究了蘭貝克演算的極小否定擴(kuò)張，并且證明了這種擴(kuò)張具有判定性，同時(shí)提出了一個(gè)滿足切割消除和子公式性質(zhì)的蘭貝克演算極小否定擴(kuò)張的根岑演算系統(tǒng)。最后我們通過(guò)構(gòu)造一個(gè)翻譯，將蘭貝克演算的德摩根擴(kuò)張嵌入到蘭貝克的弱極小否定擴(kuò)張，從而證明蘭貝克演算的德摩根擴(kuò)張的判定性。

2 極小否定蘭貝克演算及其代數(shù)模型

令A(yù)LM的語(yǔ)言遞歸定義為：

ALM的代數(shù)系統(tǒng)由公理

和以下的規(guī)則組成：

如果把ALM的語(yǔ)言限制到不包含?,⊥,?的公式，并且在系統(tǒng)中把公理規(guī)則(⊥)、(?)和(CT)去掉，那么得到的就是經(jīng)典的蘭貝克演算系統(tǒng)L。

定義1剩余半群(G,·,,/,≤)被定義為如下代數(shù)結(jié)構(gòu)：

1.(G,≤)是一個(gè)偏序；

2.(G,·)是一個(gè)半群；

3.·,,/為G上的二元算子并且滿足下面的剩余規(guī)則

在剩余半群的定義中，假如將(G,·)替換成群胚，即(·)，得到的是剩余群胚。如果同時(shí)令·滿足交換律，那么相應(yīng)得到的是交換剩余半群和交換剩余群胚。

定義2極小否定剩余半群(G,·,,/,≤,⊥,?,?)被定義為如下代數(shù)結(jié)構(gòu)：

1.⊥,?分別為G中的極小和極大元；

2.(G,·,,/,≤)是一個(gè)剩余半群；

3.?為G上的一元算子并且滿足下面的極小否定規(guī)則：

定理1L對(duì)剩余半群是有效和完全的。

證明:L有效性證明是顯然的，完全性證明使用林登保姆–塔斯基方法構(gòu)造句法模型可證。證明思路大致如下。首先取一個(gè)剩余半群(M,·,≤)是一個(gè)剩余半群，其中M為公式集。然后我們選擇M所有的下閉包子集的集合C(M)，在C(M)上面定義三個(gè)算子×,,/如下：

顯然代數(shù)(C(M),×,,/)就是一個(gè)剩余半群。在L系統(tǒng)上定義公式集為[A]:={B:?B?A},則[A]為一下閉包集。在所有的[A]組成的集合上如上定義×,,/，得到一個(gè)包含所有公式等價(jià)類的典范模型。因此可以很容易證明L相對(duì)這個(gè)模型是完全的。

下面定理2、定理4證明方法類似，只需要在選取剩余半群時(shí)選取了添加了對(duì)應(yīng)算子?,?及包含其性質(zhì)的代數(shù)結(jié)構(gòu)，其他證明步驟是相同的。

定理2ALM對(duì)極小否定剩余半群是有效和完全的。

定義3極小否定剩余半群群胚(G,·,,/,≤,⊥,?,?,→)被定義為如下代數(shù)結(jié)構(gòu)：

1.(G,·,,/,≤,⊥,?,?)為極小否定剩余半群，其中令?a:=a→⊥；

2.(G,?,→,≤)為交換剩余群胚。

定理3任意極小否定剩余半群都能被擴(kuò)張成一個(gè)極小否定剩余半群群胚。

證明:令G=(G,·,,/,≤,⊥,?,?)為一個(gè)極小否定剩余半群。定義G二元算子?和→如下：

下面證明·和→滿足如下三個(gè)條件：

1.a·b=b·a；

2.?a=a→⊥；

3.a·b≤c當(dāng)且僅當(dāng)b≤a→c。

由定義可以簡(jiǎn)單得到條件1，條件2成立。下面證明條件3成立。假設(shè)c=?時(shí)，那么a·b≤c自然成立；同時(shí)a→c=?，因此b≤a→c。令a·b≤c。因?yàn)閏?=?，所以a·b=⊥。根據(jù)定義有a≤?b，因此b≤?a。又因?yàn)閍→c=?a，所以b≤a→c。反之，假設(shè)b≤a→c。因?yàn)閏?=?，所以a→c=?a。因此b≤?a。根據(jù)定義b·a=⊥，可得a·b=⊥，那么有a·b≤c。因此G是一個(gè)一個(gè)極小否定剩余半群群胚。

令系統(tǒng)ALM+的語(yǔ)言遞歸定義為：

令系統(tǒng)ALM+是由系統(tǒng)ALM去掉規(guī)則(CT)并添加公理A?B?B?A和如下規(guī)則得到：

定義?A:=A→⊥，則規(guī)則(CT)在ALM+是可證的。證明如下：假設(shè)A?B→⊥。由LRes′2可得B?A?⊥。因?yàn)锳?B?B?A，根據(jù)(Cut)A?B?⊥以及LRes′1可得B?A→⊥。

定理4ALM+對(duì)極小否定剩余半群群胚是有效和完全的。

定理5對(duì)于任何ALM簡(jiǎn)單序列A?B，ALM?A?B當(dāng)且僅當(dāng)ALM+?A?B。

證明:從左到右的方向顯然可證。從右到左的方向，這里采用反證法的方式進(jìn)行證明。假設(shè)ALM??A?B。那么根據(jù)定理2，存在一個(gè)極小否定剩余半群G使得G??A?B。根據(jù)定理3，G可擴(kuò)張為一個(gè)極小否定剩余半群群胚G′使得G′??A?B。再根據(jù)定理4，可得ALM+??A?B。

3 根岑序列演算與判定性

本節(jié)將首先討論ALM+的根岑系統(tǒng)LM+，同時(shí)將證明LM+是可判定的，在此基礎(chǔ)上得到LM的判定性和根岑系統(tǒng)。LM+的公式定義與ALM+相同。LM+的公式結(jié)構(gòu)是由公式通過(guò)結(jié)構(gòu)算子(,)和(?)生成。公式串列可以遞歸定義如下：

序列Γ?A是由公式結(jié)構(gòu)Γ、公式A和符號(hào)?組成。任何一個(gè)公式結(jié)構(gòu)Γ代表一個(gè)公式f(Γ)。f(Γ)可以遞歸定義如下：

符號(hào)Γ[?]代表一個(gè)公式結(jié)構(gòu)中存在著一個(gè)位置?。符號(hào)Γ[?]則代表在Γ[?]中的?位置中替代入公式結(jié)構(gòu)?。

LM+的根岑序列系統(tǒng)由公理

和以下的規(guī)則組成：

定理6(切割消除) 任何在LM+下可證的序列都存在一個(gè)LM+中不使用切割規(guī)則的證明。

證明:只需要證明假如(Cut)規(guī)則的兩個(gè)前提都存在LM+下不使用(Cut)的證明，那么(Cut)規(guī)則的結(jié)構(gòu)同樣存在LM+下不使用(Cut)的證明。假設(shè)推導(dǎo)中的某一個(gè)(Cut)如下：

施歸納假設(shè)于(i)切割公式的復(fù)雜度，即切割公式中包含的連接詞數(shù)量。在歸納假設(shè)(i)中我們?cè)偈w納假設(shè)于(ii)(Cut)規(guī)則的度，即切割規(guī)則兩個(gè)前提的證明總長(zhǎng)度。

假設(shè)(Cut)規(guī)則的前提分別由規(guī)則R1和R2得到，下面分三種情況討論：

1.至少R1或R2是公理；

2.R1或R2沒(méi)有引入切割公式；

3.R1和R2同時(shí)引入切割公式。

1.假設(shè)R1或R2是公理。考慮下面的情況：

(a)如果?=B，那么Γ[B]?A等于切割結(jié)論；

(b)如果⊥∈?，⊥∈Γ或A=?，那么Γ[?]?A也是公理；

(c)如果Γ=ε并且B=A，那么??B等于切割結(jié)論；

(d)如果B=?并且Γ[B]?A不是公理，那么對(duì)R1的和R2中包含?的前提使用切割規(guī)則，然后再使用R2，根據(jù)歸納假設(shè)(ii)，結(jié)論成立；

(e)如果B=⊥并且??B不是公理，那么證明方法與情況(d)類似。

2.令R1或R2沒(méi)有引入切割公式B。當(dāng)R1或R2是(Com)或(Ass)時(shí)，證明是顯然的。下面證明當(dāng)R1是(→L)時(shí)結(jié)論成立。其他情況可用類似方法證明。假設(shè)(Cut)規(guī)則的子推導(dǎo)樹如下：

將上面的推導(dǎo)樹改寫成如下推導(dǎo)樹

新的切割規(guī)則的度要小于舊切割規(guī)則的度，因此根據(jù)歸納假設(shè)(ii)結(jié)論得證。

3.R1和R2同時(shí)引入切割公式B。下面證明當(dāng)B等于B1→B2時(shí)結(jié)論成立。其他情況可用類似方法證明。假設(shè)(Cut)規(guī)則的子推導(dǎo)樹如下：

將上面的推導(dǎo)樹改寫成如下推導(dǎo)樹：

新的切割公式的復(fù)雜度要小于舊切割公式的復(fù)雜度，因此根據(jù)歸納假設(shè)，(i)結(jié)論得證。

推論1如果LM+?Γ?A，那么存在一個(gè)LM下Γ?A的證明，使得包含在證明中的公式均為序列Γ?A中出現(xiàn)的公式的子公式。

定理7LM+是可判定的。

證明:根據(jù)定理6，對(duì)任何序列Γ?A，如果其在LM+中可證，那么必然存在LM+中不使用切割規(guī)則的證明。那么以Γ?A為根節(jié)點(diǎn)向上遍歷其在LM+中的推導(dǎo)樹。根據(jù)推論1和LM+的規(guī)則可知，可以出現(xiàn)在推導(dǎo)樹中節(jié)點(diǎn)的不重疊序列的個(gè)數(shù)是有窮的。并且在推導(dǎo)樹中每一個(gè)分支上不會(huì)出現(xiàn)兩個(gè)節(jié)點(diǎn)使得節(jié)點(diǎn)上的序列是相同的。因此可以得到該推導(dǎo)樹的深度，即最長(zhǎng)分支的長(zhǎng)度是有窮的。同時(shí)根據(jù)LM+的規(guī)則可知該推導(dǎo)樹是二叉樹。已知對(duì)任意二叉樹，假如其深度是有窮的，那么該二叉樹的規(guī)模即節(jié)點(diǎn)總數(shù)是有窮的。因此以Γ?A為根節(jié)點(diǎn)向上遍歷其在LM+中的推導(dǎo)樹是有窮的。因?yàn)橐?guī)則的個(gè)數(shù)是有窮的，遍歷序列在LM+中的推導(dǎo)樹這個(gè)過(guò)程是有窮的，因此LM+是可判定的。

定理8LM是可判定的。

證明:由定理5和定理6直接可得。

根據(jù)定理5與推論1可以得到LM+的根岑序列演算LM。LM由公理

和以下的規(guī)則組成：

定理9ALM?α?β當(dāng)且僅當(dāng)LM?α?β。

弱LM指由LM去除(Com)所得到的邏輯。由上面證明可以簡(jiǎn)單得到

定理10弱LM是可判定的。

在弱LM中可證α?β蘊(yùn)含?β?α，但不可證α???α。這里記弱LM為L(zhǎng)M?

引理1如果LM??Γ??α?⊥，那么LM??Γ?α。

由簡(jiǎn)單的施歸納于Γ??α?⊥在LM?中的證明長(zhǎng)度可證。注意?在這里是非結(jié)合算子，如果?是一可結(jié)合算子則該引理不成立。

引理2如果LM??Γ??α，那么LM??Γ?α?⊥。

簡(jiǎn)單由由?α的剩余性質(zhì)可證明。

L的德摩根擴(kuò)張是指在L上額外添加一個(gè)德摩根否定算子：即滿足α?β蘊(yùn)含?β?α和α???α.L的德摩根擴(kuò)張邏輯可以簡(jiǎn)單的由LM添加公理??α?α得到。這里將L的德摩根擴(kuò)張記為L(zhǎng)DM。

定義一個(gè)從LDM公式到LM?公式的遞歸翻譯k:

定義4

·k(p)=p；

·k(?nα)=?mα m=mod(n,2)，并且α不是一個(gè)形為?β的公式；

·k(α?β)=k(α)?k(β)，其中?∈{·,/,}。

k可自然延展為從LDM公式結(jié)構(gòu)到LM?公式結(jié)構(gòu)的翻譯。

引理3如果LDM?Γ?β，那么LM??k(Γ)?k(β)。

對(duì)該引理的證明，只需要證明LDM中的公理和規(guī)則在LM?下都是可證的。由簡(jiǎn)單施歸納于LDM?Γ?β可證。上面兩個(gè)引理保證了LDM否定規(guī)則的k翻譯在LM?下是有效的。

定理11LDM是可判定的。