基于n值關系語義的命題模態邏輯系統研究

周張泉,楊成彪,劉 軍

(1.陸軍工程大學 指揮控制工程學院,江蘇 南京 210000;2.東南大學 計算機科學與工程學院,江蘇 南京 210000;3.南京審計大學金審學院 信息科學與工程學院,江蘇 南京 210000)

0 引 言

模態邏輯作為形式化的邏輯語言工具被廣泛應用于計算機科學諸多理論和應用中[1],比如軟硬件的可靠性模型檢測[2-3]、計算復雜性理論[4-5]、數據庫理論[6]、知識表示與推理[7]、量子計算[8]等。近年來,模態邏輯越來越多地被研究如何結合神經方式以提升學習模型的可解釋性及邏輯推理能力[9-10]。通過引入模態詞,模態邏輯具有部分二階邏輯的表達能力,同時能夠保持形式上的簡潔性以及較低的計算復雜度[1,11]。研究者基于不同的模態詞,發展除了不同的模態邏輯系統,如動態邏輯[12-13]、時序邏輯[14]等。經典的模態邏輯仍舊屬于二值邏輯,這使得其在一些常見的應用場景中存在局限性,比如針對知識圖譜中分級概念(graded concepts)的推理[15-16](如概念“深紅色的花”)、多Agent協同任務[17]等。這些場景要求邏輯語言能夠描述對象某一性質的程度(如“深紅色”中“深”的程度),或者Agent進行某項決策或行動的可能性。為使得模態邏輯具備上述能力,可建立多值邏輯系統,從而對模態公式的分級程度或可能性進行推理和計算。另外,多值邏輯系統也能更直觀地映射到神經方式下的學習模型[18]。

在建立多值邏輯系統方面已有不少研究。早期研究者通過人為指派的方式確定邏輯公式的真值程度[19](又稱為真度),然而給全體命題指派真度可行性較低。為解決此問題,諸多研究將全體命題映射為模糊集進行處理,從而提出模糊邏輯的概念[20](fuzzy logic)。模糊邏輯建立了較完整的多值邏輯研究框架,通過將語義模型映射到多值系統以實現多值語義。但該方法容易導致公式真度的弱化,比如重言式和矛盾式的真假是顯而易見的,但基于該方法需要做更多假設或處理才能保證。國內學者在邏輯公式真度的建模上也進行了深入的研究[21-25],通過全體命題的真值下界確定命題真度,并將數值計算引入到真度的賦值計算中,建立了計量邏輯學的概念。此種方法更多地考察命題真度的賦值方法,以及如何誘導出復雜公式的真度,但并未從邏輯層面深入探索推理過程在多值語義下是否保持相應的性質,即原有公理系統及推理規則在多值語義下的正確性和完備性。另外,不少工作引入ukasiewicz代數系統以建立多值邏輯系統[20,26-27]。ukasiewicz代數系統具有取值有限性的特點且可以進行任意的n值擴張,相較于復雜代數系統下的計量邏輯在建模難易性與計算效率上具有優勢。該方法也被用于建立多值模態邏輯[28-29]。具體而言,給出模態公式在語義模型狀態上的真度,同時針對狀態間的關系也進行了多值化處理。然而,該方法易導致計算效率較低,且公式的可滿足性及有效性并不清晰。在實際應用中,狀態間的關系往往是明確的,比如知識圖譜中對象或事件的關系、Agent系統中的狀態轉移關系等。這意味著狀態間的可能性及程度信息可以通過公式進行傳遞,而不需要針對狀態間的關系另作多值化處理。這進一步使得公式的可滿足性及有效性也能得到更清晰的定義。

1 預備知識

(1)x→Lny=min(1,1-x+y);

(2)x∨Lny=max(x,y);

(3)x∧Lny=min(x,y);

(4)～x=1-x。

稱Ln及定義在其上的運算為n值ukasiewicz代數系統。

定義1:設P={p0,p1,…}為可數的命題變元集合,對于n值命題邏輯語言Pn,公式φ歸納定義如下:

其中,p∈P,a∈Ln。定義真度賦值函數V:Pn→Ln如下:

(1)V(p)=c(c∈Ln);

(3)V(φ)=～V(φ);

(4)V(φ∨ψ)=V(φ)∨LnV(ψ);

(5)V(φ∧ψ)=V(φ)∧LnV(ψ);

(6)V(φ→ψ)=V(φ)→LnV(ψ)。

進一步,包含邏輯符號?的公式所誘導的真度賦值函數為V(φ?ψ)=V((φ→ψ)∧(ψ→φ))。

給定Pn的公式集Γ及某公式φ,如果對于任意的ψ∈Γ且V(ψ)=1,有V(φ)=1,則稱φ是Γ的Ln-后承。針對上述n值命題邏輯語言Pn,可進一步找到一組正確且完備的公理。

定義2:n值命題邏輯公理系統Hn由如下公理組成:

(P1)φ→(ψ→φ);

(P2)(φ→ψ)→((ψ→χ)→(φ→χ));

(P4)((φ→ψ)→ψ)→((ψ→φ)→φ);

上述公理系統中,公理(P1)～公理(P4)是經典命題邏輯公理,(P5)則包含由Ln系統的數值構成的邏輯公式。給定Pn的公式集Γ及某公式φ,現有公式φ可以通過公式集Γ、上述公理、分離規則以及一致替換規則推導出,則將該推導關系記作Γ├Hnφ。上述公理系統Hn的正確性和完備性由以下定理保證。

定理1:給定Pn(n≥2)的公式集Γ及某公式φ,φ是Γ的Ln-后承,當且僅當Γ├Hnφ。

文獻[20]給出了該定理的證明?？梢则炞C,n=2是二值邏輯的情況。

2 n值命題模態邏輯

2.1 n值關系語義

基于上一節介紹的n值ukasiewicz代數系統及其在命題邏輯的擴展,給出n值命題模態邏輯的語法。

定義3:設Q={p0,p1,…}為可數的命題變元集合,對于n值命題模態邏輯語言Qn,模態公式φ歸納定義如下:

其中,p∈Q,a∈Ln。

下面基于系統Ln給出n值命題模態邏輯語言Qn的關系語義。不同于文獻[28-29],這里針對公式在狀態上進行n值化處理,同時保持狀態間關系的確定性。

定義4:令F=(S,R)為Qn的框架,其中S≠?為狀態集合,R?S×S為狀態間的二元關系;令M=(F,V)為Qn的模型,其中V:Qn×S→Ln是模態公式在狀態上的真度賦值函數,定義如下:

(1)V(p,u)=c;

(3)V(φ,u)=～V(φ,u);

(4)V(φ∨ψ,u)=V(φ,u)∨LnV(ψ,u);

(5)V(φ∧ψ,u)=V(φ,u)∧LnV(ψ,u);

(6)V(φ→ψ,u)=V(φ,u)→LnV(ψ,u);

(7)V(□φ,u)=∧Ln{V(φ,v)|?v∈S且(u,v)∈R}。

上述式子中,u,v∈S,c,a∈Ln。

根據上述定義,可以進一步導出公式◇φ的真度賦值函數,即:

V(◇φ,u)=∨Ln{V(φ,v)|?v∈S且(u,v)∈R}

參考文獻[30],下面給出Qn的模態公式在模型M上的可滿足性定義。

定義5:給定Qn的模型M=(F,V),其中F=(S,R)為Qn的框架,對于模態公式φ,若對于任意狀態u∈S,均有V(φ,u)=1,則稱φ在M上是有效的,記為VM(φ)=1。若存在某個狀態u∈S,有V(φ,u)>0,稱φ在模型M的狀態u下是可滿足的。

可以驗證,φ在模型M的某個狀態u下是可滿足的,當且僅當φ在模型M上不是有效的。對于上述可滿足性的定義,若限制V(φ,u)=1,實際上n值命題模態邏輯就轉化為了經典的命題模態邏輯。

類似于n值命題邏輯,定義Qn下的Ln-后承如下:給定Qn的模型M、公式集Γ及某公式φ,如果對于任意的ψ∈Γ且VM(ψ)=1,有VM(φ)=1,則稱φ是Γ的Ln-后承。

2.2 公理系統

在經典命題模態邏輯中,K系統為最基本的模態邏輯系統[1],其對框架上的狀態關系R沒有限制。該系統基本構成包括:經典命題邏輯公理、公理K、分離規則MP、必然化規則N以及一致替換規則:

公理K:□(φ1→φ2)→(□φ1→□φ2)

一致替換規則即將上述公理及規則中的公式一致替換為任意其它形式的公式。

以K系統為基礎,增加公理及規則可得到其他經典的模態邏輯公理系統。具體而言,在K系統之上增加公理T可得T系統,同時框架上的關系R滿足自反性;在T系統之上增加公理4可得系統S4,同時框架上的關系R滿足自反性和傳遞性;在S4上增加公理5可得系統S5,同時框架上的關系R滿足自反性和歐性[1]。

公理T:□φ→φ

公理4:□φ→□□φ

公理5: ◇φ→□◇φ

定義6:n值命題模態邏輯系統Kn由n值命題邏輯公理(P1)～公理(P5)、公理K、分離規則MP、必然化規則N、一致替換規則、公理A1以及公理A2組成;系統Tn包含Kn,另外包含公理T;系統S4n包含Tn,另外包含公理4;系統S5n包含S4n,另外包含公理5。

下文利用符號Λn指代某個n值命題模態邏輯系統,其中Λ∈{K,T,S4,S5}。在n值關系語義下,n值命題模態邏輯系統Λn的正確性及完備性尚不明確,下文對此進行探討。

3 正確性的證明

定理2:針對n值模態邏輯系統Λn,任給Qn的模型M、公式集Γ,對于任意的φ,若Γ├Λnφ,那么有φ是Γ的Ln-后承。

證明:按照如下步驟進行,首先分別證明公理K、公理T、公理4、公理5、公理A1和公理A2的有效性,其次分別證明推導規則MP及規則N的正確性。一致替換規則的正確性由前述推導規則及公理的正確性易證。另外經典n值命題邏輯公理的有效證明性可參考文獻[20],在此略過。

(1)公理K的有效性。給定任意n值模型M及公式φ,對于任意的狀態u∈S,往證結論V(□(φ1→φ2)→(□φ1→□φ2),u)=1。為證此結論,首先假設V(□(φ1→φ2),u)=c成立,欲使V(□(φ1→φ2)→(□φ1→□φ2),u)=1,根據→Ln定義,需證V(□φ1→□φ2,u)≥c。進一步假設V(□φ1,u)=d,欲使V(□φ1→□φ2,u)≥c成立,只需證V(□φ2,u)≥c+d-1。展開V(□φ2,u)如下:

V(□φ2,u)=∧Ln{V(φ2,v)|?v∈S且(u,v)∈R}

設存在狀態w∈S且(u,w)∈R,使得w=argmin?t∈S且(u,t)∈RV(φ2,t)成立,于是有V(□φ2,u)=V(φ2,w)。由于V(□(φ1→φ2),u)=c,且(u,w)∈R,有V(φ1→φ2,w)≥V(□(φ1→φ2),u)=c。又由假設V(□φ1,u)=d,有V(φ1,w)≥V(□φ1,u)=d。V(φ1→φ2,w)展開如下:

V(φ1→φ2,w)=V(φ1,w)→LnV(φ2,w)=min(1,1-V(φ1,w)+V(φ2,w))≥c

要使上式成立,即使1-V(φ1,w)+V(φ2,w)≥c,由V(□φ2,u)=V(φ2,w)有1-V(φ1,w)+V(□φ2,u)≥c,進一步有V(□φ2,u)≥c+V(φ1,w)-1,由V(φ1,w)≥d有V(□φ2,u)≥c+d-1。因此得證。

(2)公理T的有效性。給定任意n值模型M及公式φ,對于任意u∈S,往證V(□φ→φ,u)=1。進一步假設V(□φ,u)=c,欲使V(□φ→φ,u)=1,需證V(φ,u)≥c。展開V(□φ,u)如下:

V(□φ,u)=∧Ln{V(φ,v)|?v∈S且(u,v)∈R}

由于系統Tn需關系R滿足自反性,則(u,u)∈R,進一步有V(φ,u)≥V(□φ,u)=c。因此得證。

(3)公理4的有效性。給定任意n值模型M及公式φ,對于任意u∈S,往證V(□φ→□□φ,u)=1。進一步假設V(□φ,u)=c,欲使V(□φ→□□φ,u)=1,需證V(□□φ,u)≥c。任給w∈S,使得(u,w)∈R2,欲使V(□□φ,u)≥c,根據V(□□φ,u)的展開式及w的任意性,只需證V(φ,w)≥c。

展開V(□φ,u)如下:

V(□φ,u)=∧Ln{V(φ,v)|?v∈S且(u,v)∈R}

由(u,w)∈R2以及系統S4n中關系R的傳遞性有(u,w)∈R,因此根據上式有結論V(φ,w)≥V(□φ,u)=c成立。因此得證。

(4)公理5的有效性。給定任意n值模型M及公式φ,對于任意u∈S,往證V(◇φ→□◇φ,u)=1。進一步假設V(◇φ,u)=c,欲使V(◇φ→□◇φ,u)=1,需證V(□◇φ,u)≥c。任給v∈S,使得(u,v)∈R,欲使V(□◇φ,u)≥c,只需證V(◇φ,v)≥c。

展開V(◇φ,u)如下:

V(◇φ,u)=∨Ln{V(φ,w)|?w∈S且(u,w)∈R}=c

因此,存在w∈S且(u,w)∈R,使得V(φ,w)=c。由于系統S5n中關系R具有歐性,有(v,w)∈R,進一步根據V(◇φ,v)的展開式有V(◇φ,v)≥V(φ,w)=c。因此得證。

∧Ln{min(1,1-a+V(φ,v))|?v∈S

且(u,v)∈R}=c

欲使上式結論成立,有?v∈S且(u,v)∈R,需有1-a+V(φ,v)≥c,即V(φ,v)≥a+c-1。因此得證。

min(1,1-a+V(□φ,u))=c

欲使上式成立,需1-a+V(□φ,u)=c,即V(□φ,u)=a+c-1。展開V(□φ,u)有,欲使V(□φ,u)=a+c-1成立,有?v∈S且(u,v)∈R,V(φ,v)≥a+c-1成立。因此得證。

下面證明規則的正確性。

(7)分離規則MP的正確性。給定任意n值模型M及公式φ,根據歸納假設有VM(φ)=1,VM(φ→ψ)=1,往證VM(ψ)=1。由VM(φ)=1和VM(φ→ψ)=1有,對于任意狀態u∈S,V(φ,u)=V(φ→ψ,u)=1。V(φ→ψ,u)可展開如下:

V(φ→ψ,u)=V(φ,u)→LnV(ψ,u)=min(1,1-V(φ,u)+V(ψ,u))=min(1,V(ψ,u))=1

由于V(ψ,u)≤1,要使上式成立,則有V(ψ,u)=1,由于u的任意性,即有VM(ψ)=1。因此得證。

(8)推導規則N的正確性。給定任意n值模型M及公式φ,根據歸納假設有VM(φ)=1,往證VM(□φ)=1。由VM(φ)=1有,對于任意u∈S,V(φ,u)=1。展開V(□φ,u)如下:

V(□φ,u)=∧Ln{V(φ,v)|?v∈S且(u,v)∈R}

設存在狀態w∈S且(u,w)∈R,并且使得w=argmin?v∈S且(u,v)∈RV(φ,v),由上式有V(□φ,u)=V(φ,w)。由于u具有任意性,有V(φ,w)=1,進一步有V(□φ,u),因而VM(□φ)=1得證。

證畢。

4 完備性的證明

定義7(極大一致集):任給n值命題模態公式集Ω,Ω是一致的,且不存在任何Ω'?Ω,使得Ω'是一致的,則稱Ω是極大一致集。

下文用MΛn代表公理系統Λn上所有極大一致集構成的集合。進一步,根據極大一致集的定義,有如下引理。

引理1:任給邏輯系統Λn的極大一致集Ω,對任意n值命題模態公式φ,ψ有:

(3)φ→ψ∈Ω當且僅當φ?Ω或ψ∈Ω;

(4)φ∧ψ∈Ω當且僅當φ∈Ω且ψ∈Ω;

(5)φ∨ψ∈Ω當且僅當φ∈Ω或ψ∈Ω。

證明 分別針對上述5條結論證明:

證畢。

針對公理系統Λn的典范模型MΛn基于Λn上極大一致集的集合MΛn進行構建。具體定義如下:

定義8(典范模型):對于公理系統Λn,構建模型MΛn=(SΛn,RΛn,VΛn),其中:

(1)SΛn=MΛn;

(2)對于任意的u,w∈SΛn,(u,w)∈RΛn當且僅當,對任意的公式φ∈Qn,若□φ∈u則φ∈w;同時RΛn滿足對應系統Λ對關系的要求;

(3)對于所有的命題變元p,VΛn(p,u)=1當且僅當p∈u;

(4)對于任意公式φ,VΛn(φ,u)滿足定義4。稱模型MΛn為Λn的典范模型。

顯然,根據定義4,上述模型MΛn是一個n值命題模態邏輯模型。進一步,由上述定義(2)易得如下推論。

推論1:模型MΛn=(SΛn,RΛn,VΛn)是系統Λn的典范模型,對于任意的u,w∈SΛn,若(u,w)∈RΛn,那么對任意的公式φ∈Qn,當φ∈w時,□φ∈u成立。

在進入完備性證明前,還需證明如下真值引理。

引理2(真值引理):令MΛn=(SΛn,RΛn,VΛn)為邏輯系統Λn的典范模型,對任意u∈SΛn及任意n值模態邏輯公式φ,有VΛn(φ,u)=1當且僅當φ∈u。

證明:施歸納于φ的語法構造。

基礎步:當φ為命題變元時,由定義8(3)易證。

(1)φ:=ψ,此時有VΛn(φ,u)=1當且僅當VΛn(ψ,u)=～VΛn(φ,u)=0。根據歸納假設,VΛn(ψ,u)≠1當且僅當ψ?u。根據引理1(2),ψ?u當且僅當ψ∈u,即φ∈u。

(2)φ:=ψ∨χ,此時有VΛn(φ,u)=1當且僅當VΛn(ψ∨χ,u)=1,即VΛn(ψ,u)=1或VΛn(χ,u)=1。根據歸納假設,VΛn(ψ,u)=1或VΛn(χ,u)=1,當且僅當ψ∈u或χ∈u,當且僅當(根據引理1(5))ψ∨χ∈u,即φ∈u。

(3)φ:=ψ∧χ,此時有VΛn(φ,u)=1當且僅當VΛn(ψ∧χ,u)=1,即VΛn(ψ,u)=1且VΛn(χ,u)=1。根據歸納假設,VΛn(ψ,u)=1且VΛn(χ,u)=1,當且僅當ψ∈u且χ∈u,當且僅當(根據引理1(4))ψ∧χ∈u,即φ∈u。

(4)φ:=ψ→χ,此時有VΛn(φ,u)=1當且僅當VΛn(ψ→χ,u)=1。展開VΛn(ψ→χ,u)如下:

VΛn(ψ→χ,u)=VΛn(ψ,u)→LnVΛn(ψ,χ)=

min(1,1-VΛn(ψ,u)+VΛn(χ,u))=1

欲使上式成立,需VΛn(χ,u)≥VΛn(ψ,u)。(i)假設VΛn(ψ,u)=1,有VΛn(χ,u)=1,根據歸納假設χ∈u;(ii)假設VΛn(ψ,u)<1,那么VΛn(χ,u)只需滿足VΛn(χ,u)≥VΛn(ψ,u)即可。由于VΛn(ψ,u)<1,即VΛn(ψ,u)≠1,根據歸納假設,ψ?u。因此,VΛn(ψ→χ,u)=1,當且僅當(i)或(ii)成立,當且僅當ψ?u或χ∈u,當且僅當(根據引理1(3))ψ→χ∈u,即φ∈u。

(5)φ:=□ψ,(?)若VΛn(φ,u)=1,即VΛn(□ψ,u)=1。展開VΛn(□ψ,u)如下:

VΛn(□ψ,u)=∧Ln{VΛn(ψ,v)|?v∈SΛn且(u,v)∈RΛn}

由于VΛn(□ψ,u)=1,因此?v∈SΛ且(u,v)∈RΛn,有VΛn(ψ,v)=1,根據歸納假設ψ∈v。根據推論5.1,有□ψ∈u,即φ∈u。

(?)若φ∈u,即□ψ∈u,任給v∈SΛn使得(u,v)∈RΛn,根據定義8(2)有ψ∈v,根據歸納假設,VΛn(ψ,v)=1。展開VΛn(□ψ,u)如下:

VΛn(□ψ,u)=∧Ln{VΛn(ψ,v)|?v∈SΛn且(u,v)∈RΛn}

由VΛn(ψ,v)=1及v任意性,有VΛn(□ψ,u)=1。

證畢。

下面可進一步完成完備性的證明。

所尋找的模型為Λn的典范模型MΛn=(SΛn,RΛn,VΛn)。令Γ'為Λn的極大一致集,且Γ'?Γ,有Γ'∈SΛn。

(1)對于任意的ψ∈Γ,有ψ∈Γ',根據引理2進一步有VΛn(ψ,Γ')=1。

綜合(1)和(2)可證上述逆否命題。

證畢。

5 結束語