林哲

中山大學哲學系 中山大學邏輯與認知研究所linzhe8@mail.sysu.edu.cn

梁飛?

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

1 引言

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

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

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

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

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

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

令ALM的語言遞歸定義為：

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

定理3任意極小否定剩余半群都能被擴張成一個極小否定剩余半群群胚。

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

下面證明·和→滿足如下三個條件：

1.a·b=b·a；

2.?a=a→⊥；

3.a·b≤c當且僅當b≤a→c。

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

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

令系統(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?⊥。因為A?B?B?A，根據(jù)(Cut)A?B?⊥以及LRes′1可得B?A→⊥。

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

定理5對于任何ALM簡單序列A?B，ALM?A?B當且僅當ALM+?A?B。

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

3 根岑序列演算與判定性

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

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

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

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

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

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

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

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

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

1.至少R1或R2是公理；

2.R1或R2沒有引入切割公式；

3.R1和R2同時引入切割公式。

1.假設(shè)R1或R2是公理?？紤]下面的情況：

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

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

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

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

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

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

將上面的推導樹改寫成如下推導樹

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

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

將上面的推導樹改寫成如下推導樹：

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

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

定理7LM+是可判定的。

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

定理8LM是可判定的。

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

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

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

定理9ALM?α?β當且僅當LM?α?β。

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

定理10弱LM是可判定的。

在弱LM中可證α?β蘊含?β?α，但不可證α???α。這里記弱LM為LM?

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

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

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

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

L的德摩根擴張是指在L上額外添加一個德摩根否定算子：即滿足α?β蘊含?β?α和α???α.L的德摩根擴張邏輯可以簡單的由LM添加公理??α?α得到。這里將L的德摩根擴張記為LDM。

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

定義4

·k(p)=p；

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

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

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

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

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

定理11LDM是可判定的。