賈青
中國社會(huì)科學(xué)院 哲學(xué)研究所 邏輯研究室v100jq@163.com
從20世紀(jì)60年代開始,不同相干邏輯系統(tǒng)的代數(shù)語義相繼出現(xiàn),但是這些代數(shù)語義大都是為某一或某些相干邏輯系統(tǒng)構(gòu)建的,因此具有較強(qiáng)的特設(shè)性,也很難將其推廣或者應(yīng)用到其他相干邏輯系統(tǒng)的語義構(gòu)造上去。Meyer和Routley([1])所定義的阿克曼廣群(Ackermann groupoid)則初步改善了這一狀況。由于阿克曼廣群給出了相干邏輯的基本正系統(tǒng)(Basic positive system)B+以及B+的一系列擴(kuò)充的語義解釋,所以其成為一個(gè)較有普遍性的代數(shù)語義。Meyer和Routley([1])還探討了阿克曼廣群與相干邏輯關(guān)系語義之間的對(duì)應(yīng)關(guān)系。本文中,我們將這種討論擴(kuò)展到阿克曼廣群、關(guān)系語義(relational semantics)以及推理語義這三者之間的對(duì)應(yīng)關(guān)系,從而說明對(duì)于B+以及其一系列擴(kuò)充而言,這三種語義解釋是等價(jià)的。
相干邏輯系統(tǒng)B+由Routley和Meyer([2])給出。B+的語言記作LB+,其中包括命題常項(xiàng)?,二元連接詞→、∧、∨,命題變項(xiàng)p、q、...以及輔助符號(hào)左括號(hào)“(”和右括號(hào)“)”。
LB+有以下類型的公式:變項(xiàng)、常項(xiàng)、A∧B、A∨B和A→B。
系統(tǒng)B+的公理模式和推導(dǎo)規(guī)則如下:
如果保持B+的公理模式(A1–A9)和規(guī)則(R1–R5)不變,那么B+可以通過增加下列的任意公理模式而得到擴(kuò)充1需要注意的是,通過將B+中的規(guī)則轉(zhuǎn)變?yōu)槎ɡ?,我們就能得到比B+更強(qiáng)的相干邏輯系統(tǒng)。:
由此可以得到下列相干邏輯中的正系統(tǒng):
如果剔除掉LB+中的常項(xiàng)?以及相關(guān)公理模式和規(guī)則,那么就能在此基礎(chǔ)上擴(kuò)充得到一系列不含常項(xiàng)?的相干邏輯正系統(tǒng)(如R+等)。
對(duì)于系統(tǒng)B+,我們使用V(LB+)表示LB+的變項(xiàng)集,C(LB+)表示LB+的常項(xiàng)集,F(xiàn)(LB+)表示LB+的公式集,Th(B+)表示LB+的定理集;如果將B+的上述任意擴(kuò)充系統(tǒng)記為L+,那么LL+、V(LL+)、C(LL+)、F(LL+)、Th(L+)就分別表示L+的語言以及LL+的變項(xiàng)集、常項(xiàng)集、公式集和定理集。
Meyer和Routley([1])中指出阿克曼廣群是最基礎(chǔ)的相干代數(shù)(結(jié)構(gòu))。這一代數(shù)結(jié)構(gòu)可被定義如下:
定義 2.1結(jié)構(gòu) G=〈G,≤,?,→,1〉2二元運(yùn)算?可被解釋為命題一致性(propositional consistency)且被嚴(yán)格定義如下:對(duì)于G中任意的元素a、是一個(gè)阿克曼廣群,當(dāng)且僅當(dāng)下面的條件被滿足:
(1)G是一個(gè)非空集合,≤是G上的二元偏序關(guān)系,即≤是自反、傳遞且反對(duì)稱的;?是G上的二元運(yùn)算,且對(duì)于G中的任意元素a,b,c,如果a≤b,那么a?c≤b?c且c?a≤c?b;
(2)對(duì)于G中任意的元素a,1?a=a;
(3)是G上的二元運(yùn)算,且G相對(duì)于是左剩余的(left-residuated),即對(duì)于G中的任意元素a,b,c,a?b≤c,當(dāng)且僅當(dāng)c;
引入阿克曼廣群的目的是為了對(duì)純蘊(yùn)涵的相干邏輯系統(tǒng)進(jìn)行刻畫。類似地,如果阿克曼廣群被引入的目的是對(duì)那些相干邏輯正系統(tǒng)進(jìn)行一般性的刻畫或者說明,那么就要使用正的阿克曼廣群。這一代數(shù)結(jié)構(gòu)可被定義如下:
定義 2.2結(jié)構(gòu)是一個(gè)正的阿克曼廣群,當(dāng)且僅當(dāng)下面的條件被滿足:
(1)定義2.1中的條件(1)被加強(qiáng)如下:
〈G,≤〉是一個(gè)分配格(distributive lattice),即〈G,≤〉是一個(gè)格(lattice)且對(duì)于G中的任意元素是格序的(lattice-ordered),即對(duì)于S中任意的元素a,b,c,b,a?b=d f?,其中?是G上的一元運(yùn)算。
(2)定義2.1中的條件(2)–(3)被滿足。
相對(duì)于任意阿克曼廣群G和任意相干邏輯正系統(tǒng)L,一個(gè)解釋I是一個(gè)定義在L中所有公式上的函數(shù),且對(duì)于L中的任意公式A,B,滿足下面的條件:3條件(4)和(5)是相對(duì)于正的阿克曼廣群給出的。
對(duì)于正系統(tǒng)L中的任意公式A,A在相對(duì)于任意阿克曼廣群G的解釋I下為真,當(dāng)且僅當(dāng)1≤I(A),否則,A在I下為假。A在G上是有效的,當(dāng)且僅當(dāng)A在相對(duì)于G的所有解釋下都為真。
Routley和Meyer([2])中將相干邏輯關(guān)系語義中的正模型結(jié)構(gòu)(positivemodel structure)定義如下:
定義2.3一個(gè)正模型結(jié)構(gòu)是一個(gè)三元組〈0,K,R〉,其中K是一個(gè)集合,0∈K且R是一個(gè)K上的三元組使得下面的定義和假設(shè)都成立:
對(duì)于K中任意的元素a,b,c,d而言:
(1)a<b=dfR0ab;
(2)R2abcd=df?x(Rabx∧Rxcd);
(3)R0aa;a<b并且b<c?a<c;
(4)R20abc?Rabc。
定義2.4令〈0,K,R〉為一個(gè)正模型結(jié)構(gòu),v是該結(jié)構(gòu)上的一個(gè)從V(LL+)×K到{0,1}函數(shù)且滿足下面的條件:a<b并且v(p,a)=1?v(p,b)=1。
另外,v可擴(kuò)充為滿足下面條件的結(jié)構(gòu)〈0,K,R〉上的解釋I:
對(duì)于K中任意的元素a,b,c:
(1)I(p,a)=v(p,a);
(2)I(A∧B,a)=1當(dāng)且僅當(dāng)I(A,a)=1并且I(B,a)=1;
(3)I(A∨B,a)=1當(dāng)且僅當(dāng)I(A,a)=1或者I(B,a)=1;
(4)I(A→B,a)=1當(dāng)且僅當(dāng):如果I(A,b)=1且Rabc,那么I(B,c)=1;
(5)I(?,a)=1當(dāng)且僅當(dāng)0<a。
對(duì)于任意公式A,如果I(A,0)=1,那么稱A在解釋I上被驗(yàn)證(verified)。相對(duì)于某一正模型結(jié)構(gòu),如果A在該結(jié)構(gòu)上的任意解釋下都為真,那么稱A在該正模型結(jié)構(gòu)上是有效的。
相干邏輯推理語義由周北海([3,4])給出,其初衷是為相干邏輯關(guān)系語義,特別是正模型結(jié)構(gòu)中的三元關(guān)系R給出一個(gè)符合直觀的解釋。
推理語義提出R表示的是推理規(guī)則集、前提集以及結(jié)論集三者之間的關(guān)系。任何一個(gè)推理都由前提、結(jié)論和規(guī)則這三部分構(gòu)成,如果令A(yù)→B為一個(gè)規(guī)則、A為一前提,那么經(jīng)由該規(guī)則,就能從前提A得到結(jié)論B。如果令Z表示某一非空子集,r表示邏輯規(guī)則集,R表示前提集、結(jié)論集和規(guī)則集之間的三元關(guān)系,那么推理語義中的框架就可被表示為三元組〈Z,R,r〉。
記號(hào)說明:
設(shè)a,b是任意的公式集,[ab]df={B|A→B∈a且A∈b}。
定義2.5三元組〈Z,R,r〉是一個(gè)推理語義框架,當(dāng)且僅當(dāng),
(1)Z??(F(LL+));
(2)r∈Z,稱為邏輯規(guī)則集;
(3)對(duì)Z中任意的元素a,b,c而言,Rabc,當(dāng)且僅當(dāng),[ab]?c;
(4)對(duì)Z中任意的元素a而言,[ra]=a。
定義2.6令〈Z,R,r〉是一個(gè)推理語義框架,I是該框架上的解釋,則
對(duì)于Z中任意的元素a,b,c
(1)I(p,a)=1,當(dāng)且僅當(dāng),p∈a;
(2)I(A∧B,a)=1,當(dāng)且僅當(dāng),I(A,a)=1且I(B,a)=1;
(3)I(A∨B,a)=1,當(dāng)且僅當(dāng),I(A,a)=1或I(B,a)=1;
(4)I(A→B,a)=1,當(dāng)且僅當(dāng),如果Rabc且I(A,b)=1,那么I(B,c)=1;
(5)I(?,a)=1當(dāng)且僅當(dāng)[rr]?a。
對(duì)于意公式A,A在推理語義框架〈Z,R,r〉上是有效的,當(dāng)且僅當(dāng)A∈r。
定義3.1令三元組〈0,K,R〉為相干邏輯關(guān)系語義中的一個(gè)正模型結(jié)構(gòu)。K的子集J被稱為是一擊(strike),如果對(duì)于任意K中的元素a,b,若a∈J且a<b,則b∈J。
所有擊構(gòu)成的集合可稱為S(K),由S(K)可構(gòu)建六元組〈S(K),?,→,∧,∨,1〉。
定義 3.2六元組中,如果對(duì)于S(K)中的任意元素J1,J2,下面的條件被滿足,那么該六元組就是一個(gè)正阿克曼廣群:
(1)J1?J2={c∈K且存在屬于J1的元素a和屬于J2的元素b滿足Rabc}
(3)J1J2=J1∩J2
(4)J1J2=J1∪J2
(5)1={a:a∈K且0<a}
Meyer和Routley指出了關(guān)系語義中的正模型結(jié)構(gòu)與代數(shù)語義中的正阿克曼廣群之間的對(duì)應(yīng)關(guān)系([1]),即相對(duì)于某一關(guān)系語義的正模型結(jié)構(gòu)〈0,K,R〉而言,每一正的阿克曼廣群都能被表示為S(K)的一個(gè)子廣群(sub-groupoid);另外,給定一個(gè)正的阿克曼廣群G,一個(gè)關(guān)系語義的正模型結(jié)構(gòu)〈K,R,0〉也能被自然地構(gòu)建出來。因此,如果能給出關(guān)系語義中正模型結(jié)構(gòu)與推理語義框架之間的對(duì)應(yīng)關(guān)系,那么就能得到阿克曼廣群與推理語義框架之間的對(duì)應(yīng)關(guān)系,以便于看清相干邏輯三種語義的框架之間的對(duì)應(yīng)關(guān)系。
定理3.1如果三元組〈Z,R,r〉是一個(gè)推理語義框架,那么〈Z,R,r〉是一個(gè)正模型結(jié)構(gòu)。
證明:令〈Z,R,r〉是一個(gè)滿足定義定義2.5要求的推理語義框架。由定義2.3和定義2.5可得,如果能夠證明R滿足定義2.3中的定義和預(yù)設(shè),那么〈Z,R,r〉就是一個(gè)正模型結(jié)構(gòu)。
現(xiàn)規(guī)定,對(duì)于Z中任意的元素a,b,c,d而言
因此,R滿足定義2.3中的定義。
對(duì)于預(yù)設(shè)(3):
由定義2.5中的條件(4)可得[ra]?a,因此再由定義2.5中條件(3)可得Rraa。
由定義2.5中的條件(4)可得對(duì)于Z中任意的元素a,a?[ra],由全稱消去規(guī)則可得,b?[rb],進(jìn)而可得[ra]?b?[ra]?[rb]。由[ra]?b?[ra]?[rb]可得[ra]?b?([rb]?c?[ra]?c),由定義2.5中的條件(3)可得Rrab?(Rrbc?Rrac),即Rrab并且Rrbc?Rrac。由定義a<b=dfRrab可得,a<b并且b<c?a<c。
對(duì)于預(yù)設(shè)(4):
由定義2.5中的條件4可得[ra]?a,又因?yàn)閇ab]?[ab]為真,所以[ra]?a?[ab]?[ab],即?x([ra]?x?[ab]?[xb])。由存在消去規(guī)則可得,[ra]?x?[ab]?[xb],進(jìn)而可得[ra]?x?([xb]?c?[ab]?c),即[ra]?x∧[xb]?c?[ab]?c。由定義2.5中條件(3)可得Rrax∧Rxbc?Rabc,由存在添加規(guī)則可得?x(Rrax∧Rxbc?Rabc),再由定義R2abcd=df?x(Rabx∧Rxcd)可得R2rabc?Rabc。因此可得,結(jié)論成立。
周北海、賈青([5])中將任意的關(guān)系語義正模型以及其公式化模型(formulistic model)定義如下:
定義3.3令M=〈K,R,0,I〉是任意的關(guān)系語義(正)模型,其中F=〈K,R,0〉是關(guān)系語義中的正模型結(jié)構(gòu),I為解釋函數(shù)。s(M)=〈s(K),s(R),s(0),s(I)〉是M的公式化模型,如果
(1)對(duì)于任意α∈K,s(α)={A|I(A,α)=1};
(2)s(K)={s(α)|α∈K};
(3)對(duì)任意的a,b,c∈s(K),s(R)abc,當(dāng)且僅當(dāng),[ab]?c;
(4)s(I)是推理語義的賦值映射I。
其中,s(M)中的部分〈s(K),s(R),s(0)〉稱為〈K,R,0〉的公式化框架。
定理3.2令F=〈K,R,0〉為相干邏輯關(guān)系語義中的任意正模型結(jié)構(gòu)且其公式化框架為s(F)=〈s(K),s(R),s=(0)〉。如果A→A∈s(0),那么s(F)就是一推理語義框架。
證明:由定義2.5和定義3.3可得,如果s(F)滿足定義2.5中的條件(4),那么s(F)就是一推理語義框架。
現(xiàn)求證對(duì)s(K)中任意的元素a而言,[s(0)a]=a。
(1)求[s(0)a?a]。設(shè)a是s(K)中的任意元素。由定義3.3,存在α∈K,a=s(α)。由于F是一個(gè)關(guān)系語義中的正模型結(jié)構(gòu),所以有R0αα。進(jìn)而可得對(duì)任意的公式A,B,如果I(A→B,0)=1且I(A,α)=1,那么I(B,α)=1,由此可得,如果A→B∈s(0)且A∈s(α),則B∈(α)。這就是[s(0)a]?a。
(2)求a?[s(0)a],即對(duì)任意的c,[s(0)a]?c?a?c。現(xiàn)假設(shè)[s(0)a]?c,求對(duì)于任意公式A,如果A∈a,那么A∈c。由記號(hào)說明可得,[s(0)a]?c,即對(duì)于任意的B,C,如果C→B∈s(0)且C∈a,那么B∈c。由全稱消去規(guī)則可得,如果A∈A∈s(0)且A∈a,那么A∈c。因此a?c成立。
因此可得,結(jié)論成立。
由于對(duì)B+以及其上文中的一系列擴(kuò)充而言,A→A都是其系統(tǒng)中的公理,因此在這一情況下,定理3.2可被修改為:如果F=〈K,R,0〉為相干邏輯關(guān)系語義中的任意正模型結(jié)構(gòu)且F的公式化框架為s(F)=〈s(K),s(R),s(0)〉,那么s(F)就是一推理語義框架。下面的各種結(jié)論中,如不特別說明,也都是相對(duì)于B+以及其上文中的一系列擴(kuò)充而言的。
定義3.4設(shè)F,F(xiàn)′是任意的兩個(gè)框架。F與F′是等價(jià)的,如果對(duì)于任意公式A,A在F上有效,當(dāng)且僅當(dāng),A在F′上有效。
定理3.3如果令M=〈K,R,0,I〉是任意的關(guān)系語義模型,s(M)=〈s(K),s(R),s(0),s(I)〉是M的公式化模型,A是任意的公式,那么對(duì)任意的a∈s(K),I(A,a)=1,當(dāng)且僅當(dāng),A∈a。
證明:對(duì)于變項(xiàng),由定義2.6(1),命題成立。
對(duì)于常項(xiàng),假定?∈a,那么存在α∈K使得I(?,α)=1。由定義2.4(5)可得,0<α,即R00α成立,所以s(R)s(0)s(0)s(α)成立,即[rr]?s(α),所以可得I(?,a)=1。
假設(shè)?/∈a,那么存在α∈K使得I(?,α)=0。由定義2.4(5)可得,0<α不成立,即R00α不成立,所以[rr]??(α),進(jìn)而可得I(?,a)=0。
在A是一合取式、析取式或者蘊(yùn)涵式的情況下,證明參考[5]。
定理3.4如果令F=〈K,R,0〉為相干邏輯關(guān)系語義中的任意正模型結(jié)構(gòu)且其公式化框架為s(F)=〈s(K),s(R),s(0)〉,那么F與s(F)是等價(jià)的。
證明:按照定義3.4的要求,求證對(duì)于任意的公式A,A在F上有效,當(dāng)且僅當(dāng),A在s(F)上有效。從左到右:
對(duì)A中連接詞的數(shù)量施歸納。
如果A中連接詞數(shù)量為0,那么A為一變項(xiàng)或者常項(xiàng)。
假設(shè)結(jié)論不成立,即①A在F上有效且②A在s(F)上不是有效的,那么由①和推理語義中的有效性定義可得A/∈r,即存在一個(gè)解釋函數(shù)I以及s(K)中的元素s(α),使得I(A,s(α)=0,因此A/∈s(α)。由②可得對(duì)于K中任意的α,I(A,α)=1。再由公式化模型的定義可得A∈s(α),與A/∈s(α)矛盾,所以在這種情況下,假設(shè)不成立,A在s(F)上有效。
假定A中的連接詞數(shù)量為n時(shí)結(jié)論成立,即如果A在F上有效,那么A在s(F)上有效?,F(xiàn)求A中的連接詞數(shù)量為n+1時(shí)結(jié)論也成立。
(1)如果A中新增的連接詞為∧,那么令A(yù)=B∧C。
由關(guān)系語義中的有效性定義可得,對(duì)于F上的任意解釋I,I(B∧C,0)=1,當(dāng)且僅當(dāng)I(B,0)=1且I(C,0)=1再由歸納假設(shè)可得如果B在F上有效,那么B在s(F)上有效,而且如果C在F上有效,那么C在s(F)上有效。因此,如果B在F上有效且C在F上有效,那么B在s(F)上有效且C在s(F)上有效。再由關(guān)系語義中的有效性定義以及推理語義中的有效性定義可得如果B∧C在F上有效,那么B∧C在s(F)上有效,即如果A在F上有效,那么A在s(F)上有效。
(2)如果A中新增的連接詞為∨,那么令A(yù)=B∨C。
證明方法類似(1)。
(3)如果A中新增的連接詞為→,那么令A(yù)=B→C。
由關(guān)系語義中的有效性定義可得,對(duì)于F上的任意模型M,I(B→C,0)=1當(dāng)且僅當(dāng)對(duì)任意的b,c∈K,如果R0bc且I(B,b)=1那么I(C,c)=1。由歸納假設(shè)可得,對(duì)任意的s(b),s(c)∈s(K),如果s(R)s(0)s(b)s(c)且I(B,s(b))=1那么I(C,s(c))=1。由定義3.2可得,I(B→C,s(0))=1。假設(shè)B→C在s(F)上不是有效的,那么存在s(b),s(c)∈s(K),使得s(R)s(0)s(b)s(c)且I(B,s(b))=1且I(C,s(c))=0,這與歸納假設(shè)所得結(jié)論矛盾,因此假設(shè)不成立,B→C在s(F)是有效的,即A在s(F)是有效的。
從右到左:
由于證明方法同樣是對(duì)A中連接詞的數(shù)量施加歸納,所以具體證明在此不作贅述。
由于相對(duì)于某一關(guān)系語義的正模型結(jié)構(gòu)〈0,K,R〉而言,每一正的阿克曼廣群都能被表示為S(K)的一個(gè)子廣群(sub-groupoid),而每一推理語義框架都是一個(gè)正模型結(jié)構(gòu)(定理3.1),所以相對(duì)于某一推理語義的框架〈Z,R,r〉而言,每一正的阿克曼廣群也都能被表示為S(Z)的一個(gè)子廣群;另一方面,由于給定一個(gè)正的阿克曼廣群G,一個(gè)關(guān)系語義的正模型結(jié)構(gòu)〈K,R,0〉就能被自然地構(gòu)建出來,即將K視為G的素濾子(prime filters)4給定任一正阿克曼廣群〉,F(xiàn)是G的素濾子,當(dāng)且僅當(dāng)F是G的真濾子,〈G,≤〉構(gòu)成格且對(duì)于G中任意的元素a,b,如果,那么a∈F或者b∈F。的集合,而這一正模型結(jié)構(gòu)的公式化框架就是一個(gè)推理語義框架(定理3.2),而且該推理語義框架等價(jià)與由正阿克曼廣群所構(gòu)造出的正模型結(jié)構(gòu)。
由此,我們就能較為清楚地整理出相干邏輯正系統(tǒng)的代數(shù)語義(正阿克曼廣群)、關(guān)系語義(正模型結(jié)構(gòu))以及推理語義(推理語義框架)之間的對(duì)應(yīng)關(guān)系。
令A(yù)表示任意公式,A是B+中的定理,當(dāng)且僅當(dāng)A在所有的正阿克曼廣群中是有效的([1]),當(dāng)且僅當(dāng)A在所有的正模型結(jié)構(gòu)上是有效的([1,2])。
Meyer和Routley([1])進(jìn)一步給出了公理B1–B12在代數(shù)語義中以及關(guān)系語義中所分別對(duì)應(yīng)的語義假設(shè)。本節(jié)中,我們則將給出公理B1–B12在推理語義中所分別對(duì)應(yīng)的語義假設(shè)。
系統(tǒng)B+以及公理B1-B12在代數(shù)語義、關(guān)系語義以及推理語義中所分別對(duì)應(yīng)的條件或者假設(shè)如表1。
需要注意的是,表1中“?”是一個(gè)元語言符號(hào),表示推出關(guān)系。
由表1可見,系統(tǒng)B+所對(duì)應(yīng)的代數(shù)語義、關(guān)系語義以及推理語義中的結(jié)構(gòu)分別是正阿克曼廣群、正模型結(jié)構(gòu)以及推理語義框架。公理B1–B12在三種語義中所對(duì)應(yīng)的假設(shè)則分別如表中所述。
對(duì)于B+的任意擴(kuò)充系統(tǒng)L+(即在B+的基礎(chǔ)上添加B1–B12中任意公理模式后所得到的系統(tǒng)),一個(gè)正阿克曼廣群對(duì)L+而言是適合的(fitting),假如新增公理所對(duì)應(yīng)的代數(shù)語義假設(shè)在這一廣群上是成立的;一個(gè)正模型結(jié)構(gòu)對(duì)L+而言是適合的,假如新增公理所對(duì)應(yīng)的關(guān)系語義假設(shè)在這一結(jié)構(gòu)上是成立的。對(duì)于任意公式A,A是L+中的定理,當(dāng)且僅當(dāng)A在所有適合L+的正阿克曼廣群上是有效的([1]),當(dāng)且僅當(dāng)A在所有適合L+的正模型結(jié)構(gòu)上是有效的([1])。
表1
定義4.1三元組〈Z,R,r〉是B+的推理語義框架,當(dāng)且僅當(dāng),
(1)〈Z,R,r〉是一個(gè)推理語義框架;
(2)Th(B+)?r。
定理4.1對(duì)于任意公式A,A是B+中的定理,當(dāng)且僅當(dāng)A在B+的推理語義框架上是有效的。
證明:由定理3.1、定理3.2以及定理3.4可得,B+的正模型結(jié)構(gòu)與推理語義框架是等價(jià)的,又由于定理4.1中的結(jié)論在B+的正模型結(jié)構(gòu)上是成立的,所以該結(jié)論在B+的推理語義框架上也成立。
對(duì)于B+的任意擴(kuò)充系統(tǒng)L+,一個(gè)推理語義框架對(duì)L+而言是適合的,假如新增公理所對(duì)應(yīng)的推理語義假設(shè)在這一框架上是成立的。下面將證明;A是L+中的定理,當(dāng)且僅當(dāng)A在所有適合L+的推理語義框架上是有效的。
定義4.2三元組〈Z,R,r〉是L+的推理語義框架,當(dāng)且僅當(dāng),
(1)〈Z,R,r〉是一個(gè)推理語義框架;
(2)Th(L+)?r;
(3)〈Z,R,r〉對(duì)L+而言是適合的。
定理4.2令L+是一個(gè)在B+的基礎(chǔ)上添加B1–B12中任意公理得到相干邏輯正系統(tǒng),那么對(duì)于任意公式A,A是L+中的定理,當(dāng)且僅當(dāng)A在對(duì)L+合適的推理語義框架上是有效的。
證明:由定理4.1可得,如果能夠證明公理B1-B12各自所對(duì)應(yīng)的關(guān)系語義假設(shè)成立,當(dāng)且僅當(dāng)其所對(duì)應(yīng)的推理語義假設(shè)成立,那么結(jié)論成立。
對(duì)于B1,B4和B7。參見[5]。
對(duì)于B2。從右到左:假設(shè)[a[ab]]?[ab],則[ab]?c?[a[ab]]?c。因?yàn)閇ab]?[ab]總成立,所以可得[ab]?c?[a[ab]]?c∧[ab]?[ab],即Rabc??x(Rabx∧Raxc),進(jìn)而可得Rabc?R2a(ab)c成立。
從左到右:求[a[ab]]?[ab],即求[ab]?c?[a[ab]]?c。假設(shè)[ab]?c,如果對(duì)于任意的公式A,B,A→B∈a且A∈[ab],那么B∈c,則結(jié)論成立。設(shè)存在α,β,γ∈K,a=s(α),b=s(β)且c=s(γ)。由于s(R)s(α)s(β)s(γ)?s(R)2s(α)(s(α)s(β))s(γ)成立,所以由 [ab]?c可得s(R)s(α)s(β)s(γ) 也成立,進(jìn)而可得s(R)2s(α)(s(α)s(β))s(γ),即存在s(K)中的元素x,[s(α)x]?s(γ)∧[s(α)s(β)]?x,也就是[ax]?c∧[ab]?x成立。因?yàn)锳∈[ab]所以A∈x。由于[ax]?c成立且A→B∈a,A∈x,所以可得B∈c。
對(duì)于 B3。從右到左:假設(shè)[b[ac]]?[[ab]c],則 [[ab]c]?d?[b[ac]]?d,即R[ab]cd?Rb[ac]d。又因?yàn)镽ab[ab]和Rac[ac]總成立,所以可得R[ab]cd∧Rab[ab]?Rb[ac]d∧Rac[ac],即R2abcd?R2b(ac)d成立。
從左到右:求[b[ac]]?[[ab]c],即求[[ab]c]?d?[b[ac]]?d。假設(shè)[[ab]c]?d,如果對(duì)于任意的公式A,B,A→B∈b且A∈[ac],那么B∈d,則結(jié)論成立。由A∈[ac]可得,對(duì)于任意的公式C,C→A∈a且C∈c。由于(C→A)→((A→B)→(C→B))是B3公理,再由A→B∈b和s(R)s(0)aa可得,(A→B)→(C→B)∈a,因此C→B∈[ab],再由C∈c可得B∈[[ab]c]。由于[[ab]c]?d,所以B∈d。
對(duì)于 B5。從右到左:假設(shè) [[ab]b]?[ab],則 [ab]?c?[[ab]b]?c,即Rabc?R[ab]bc。又因?yàn)镽ab[ab]總成立,所以Rabc?R[ab]bc∧Rab[ab],即Rabc?R2abbc成立。
從左到右:求[[ab]b]?[ab],即求[ab]?c?[[ab]b]?c。假設(shè)[ab]?c,如果對(duì)于任意的公式A,B,A→B∈[ab]且A∈b,那么B∈c,則結(jié)論成立。設(shè)存在α,β,γ∈K,a=s(α),b=s(β)且c=s(γ)。由于s(R)s(α)s(β)s(γ)?s(R)2s(α)s(β)s(β)s(γ)成立,所以由[ab]?c可得s(R)s(α)s(β)s(γ)也成立,進(jìn)而可得s(R)2s(α)s(β)s(β)s(γ),即存在s(K)中的元素x,[s(α)s(β)]?x∧[xs(β)]?s(γ),也就是[ab]?x∧[xb]?c成立。因?yàn)锳→B∈[ab],所以A→B∈x。由于[xb]?c成立,且A→B∈x,A∈b,所以可得B∈c。
對(duì)于B6。從右到左:假設(shè)[ar]?a,則由定義2.5可得Rara成立。
從左到右:求[as(0)]?a。假設(shè)a是s(K)中的任意元素,由定義3.3,存在α∈K,a=s(α)。由于〈K,R,0〉是一個(gè)關(guān)系語義中的正模型結(jié)構(gòu),所以有Ra0a。進(jìn)而可得對(duì)任意的公式A,B,如果I(A→B,α)=1且I(A,0)=1,那么I(B,a)=1。由此可得如果A→B∈s(a)且A∈s(0),則B∈s(a),即[as(0)]?a。
對(duì)于B8。從右到左:假設(shè)[rr]?a,則由定義2.5可得Rrra成立。
從左到右:求[s(0)s(0)]?a。假設(shè)a是s(K)中的任意元素,由定義3.3,存在α∈K,a=s(α)。由于〈K,R,0〉是一個(gè)關(guān)系語義中的正模型結(jié)構(gòu),所以有R00α。進(jìn)而可得對(duì)任意的公式A,B,如果I(A→B,0)=1且I(A,0)=1,那么I(B,α)=1。由此可得如果A→B∈s(0)且A∈s(0),則B∈s(a),即[s(0)s(0)]?a。
對(duì)于B9。從右到左:假設(shè)[ra]?[ab],則[ab]?c?[ra]?c,由定義2.5可得Rabc?Rrac成立。
從左到右:求 [ra]?[ab],即求 [ab]?c?[ra]?c。假設(shè) [ab]?c,如果可得 [ra]?c,則結(jié)論成立。設(shè)存在α,β∈K,a=s(α),b=s(β)。由于s(R)s(α)s(β)s(γ)?s(R)s(0)s(α)s(γ)成立,所以由[ab]?c可得,s(R)s(0)s(α)s(γ)成立。
對(duì)于B10。從右到左:假設(shè)[[ac][bc]]?[[ab]c],則[[ab]c]?d?[[ac][bc]]?d。進(jìn)而可得R[ab]cd?R2[ac][bc]d。又因?yàn)镽ab[ab]、Rac[ac]和Rbc[bc]都總是成立的,所以R[ab]cd∧R[ab]cd?Rac[ac]∧R2[ac][bc]d∧Rbc[bc]成立,即R2abcd??x(R2acxd∧Rbcx)成立。
從左到右:求[[ac][bc]]?[[ab]c],即求[[ab]c]?d?[[ac][bc]]?d。假設(shè)[[ab]c]?d,如果對(duì)于任意的公式A,B,A→B∈[ac]且A∈[bc],那么B∈d,則結(jié)論成立。由A→B∈[ac]可得,C→(A→B)∈a且C∈c。由于(C→(A→B))→((C→A)→(C→B))是B10公理,再由s(R)s(0)aa可得,(C→A)→(C→B)∈a。由A∈[bc]可得C→A∈b且C∈c。由(C→A)→(C→B)∈a和C→A∈b可得(C→B)∈[ab],再由C∈c可得B∈[[ab]c]。因?yàn)閇[ab]c]?d,所以B∈d。
對(duì)于B11。從右到左:假設(shè)[[ac]b]?[[ab]c],則[[ab]c]?d?[[ac]b]?d,即R[ab]cd?R[ac]bd。又因?yàn)镽ab[ab]和Rac[ac],所以可得R[ab]cd∧Rab[ab]?R[ac]bd∧Rac[ac],即R2abcd?R2acbd成立。
從左到右:求[[ac]b]?[[ab]c],即求[[ab]c]?d?[[ac]b]?d。假設(shè)[[ab]c]?d,如果對(duì)于任意的公式A,B,A→B∈[ac]且A∈b,那么B∈d,則結(jié)論成立。由A→B∈[ac]可得C→(A→B)∈a且C∈c。由于(C→(A→B))→(A→(C→B))是B11公理,再由s(R)s(0)aa可得,A→(C→B)∈a,又因?yàn)锳∈b,所以C→B∈[ab]。因?yàn)镃∈c,所以B∈[[ab]c],進(jìn)而可得B∈d。
對(duì)于B12。假設(shè)[ra]或者[rb]?[ab],則[ab]?c?[ra]?c或者[rb]?c。再由定義2.5可得Rabc?Rrac或者Rrbc成立。
從左到右:求[ra]或者[rb]?[ab],即求[ab]?c?[ra]?c或者[rb]?c。假設(shè)存在α,β,γ∈K,使得a=s(α),b=s(β)且c=s(γ)。由于s(R)s(α)s(β)s(γ)?s(R)s(0)s(α)s(γ)或者s(R)s(0)s(β)s(γ)成立,故由 [ab]?c得s(R)s(0)s(α)s(γ)或者s(R)s(0)s(β)s(γ)成立,即[ra]?c或者[rb]?c成立。
由上一節(jié)中的結(jié)論可知,對(duì)于任意公式A,A是B+中的定理,當(dāng)且僅當(dāng)A在所有的正阿克曼廣群中是有效的,當(dāng)且僅當(dāng)A在所有的正模型結(jié)構(gòu)上是有效的,當(dāng)且僅當(dāng)A在所有的推理語義框架上是有效的;而A是L+中的定理,當(dāng)且僅當(dāng)A在所有適合L+的正阿克曼廣群上是有效的,當(dāng)且僅當(dāng)A在所有適合L+的正模型結(jié)構(gòu)上是有效的,當(dāng)且僅當(dāng)A在L+的推理語義框架上是有效的。
代數(shù)語義、關(guān)系語義以及推理語義從不同的角度出發(fā),分別給出了一系列相干邏輯正系統(tǒng)的語義解釋以及可靠性和完全性的結(jié)果。雖然從技術(shù)結(jié)果的角度看,三者不相伯仲,但是從直觀性的角度看,推理語義顯然是更為直觀且易于理解的。推理語義將正模型結(jié)構(gòu)中的三元關(guān)系R解釋成推理中規(guī)則、前提和結(jié)論之間的關(guān)系,即推理中通過規(guī)則,由前提得到結(jié)論的這一關(guān)系。因此其解釋方式不但直觀明了,而且也符合相干邏輯創(chuàng)立之初,要給出推理合適的形式化刻畫的這一目標(biāo)。