Page 125 - 《软件学报》2020年第12期

张玉志 等:面向完美回忆的时态认知逻辑 3791

t
• Mw E ϕ 当且仅当对所有 v∈W,若(w,v)∈R E (B,t),则 M,vBϕ;
, B
B
• Mw C ϕB t B 当且仅当对所有 v∈W,若(w,v)∈R C (B,t),则 M,vBϕ.
,
命题 1.3(可靠性). 对任意公式ϕ,若Aϕ,则Bϕ.
t
t
t
t
容易证明 S5 C 系统的推演规则保持有效性,只需证明 S5 C 系统的公理是有效的.本文仅证明 Ax5 是有效
m
n
的( B K ϕ → K ϕ ,m<n),其他公理的有效性证明见文献[18].
a
a
证明:给定模型 M=〈W,R,V〉,假设存在 w∈W,使得:
n
m
,
Mw H K ϕ → K ϕ ,m<n (1)
a
a
根据语义定义可得:
m
Mw K ϕ (2)
, B
a
并且
n
,
Mw ¬B K ϕ ,m<n (3)
a
由公式(3),根据语义定义可知,存在 u∈W,使得:
(w,u)∈R(a,n)并且 M,uB¬ϕ (4)
由于 R 单调递减并且 m<n,所以 R(a,m)⊇R(a,n),所以(w,u)∈R(a,m).再由公式(2),根据语义定义可知:
M,uBϕ (5)
m
n
得出矛盾,所以假设不成立.所以 B K ϕ → K ϕ ,m<n.证毕. □
a a
2 完全性证明
可靠性是指系统中所有可证公式经过语义解释后都是真的,它是所有逻辑系统都必须具备的基本性质(因
为人们无法容忍一门理论能够推出虚假结论).与此不同,完全性是指所有在语义上为真的公式都是该系统的可
证公式,它是部分逻辑系统才具有的一种美好性质.一个逻辑系统同时具有可靠性和完全性,意味着语义为真的
t
t
公式构成的集合与系统中的可证公式集完全相同.S5 C 系统具有完全性,但其证明需要构造较为特殊的典范模
型.本节证明主要参考了 S5C 系统完全性的证明 [18] .
定义 2.1. 任给公式ϕ,ϕ的闭包 cl(ϕ)是指一个满足如下条件的最小集合.
(1) ϕ∈cl(ϕ);
(2) 若ψ∈cl(ϕ),则ψ的子公式集 Sub(ψ)⊆cl(ϕ);
(3) 若ψ∈cl(ϕ)且ψ不是形如¬χ的公式,则¬ψ∈cl(ϕ);
t
t
(4) 若 C ψ ∈ cl ()ϕ ,则{K C ψ | a ∈ B } ⊆ cl ( )ϕ ;
t
a
B
B
m
m
(5) 若 K ψ ,K χ a n cl ( )ϕ ∈ ,且 m<n,则 K K ψ ,K ¬ a n K ψ a m cl ( )ϕ ∈ .
n
a
a
a
引理 2.1. 对任意公式ϕ,cl(ϕ)总是有穷集.
利用结构归纳法容易证明.
定义 2.2. 令Φ是某公式的闭包,称Γ是Φ中的极大一致集当且仅当:
(1) Γ⊆Φ;
(2) Γ是一致的:ΓG⊥,即:不存在一个有穷子集{ϕ 1 ,...,ϕ n }⊆Γ,使得A¬(ϕ 1 ∧...∧ϕ n );
(3) Γ在Φ中是极大的:不存在Γ′⊆Φ,使得Γ⊂Γ′且Γ′G⊥.
显然,Φ中的每个极大一致集Γ都是有穷的.令Γ=∧ ϕ∈Γ ϕ.
定义 2.3. 令Φ是某公式的闭包,A 是Φ中出现主体的集合,T 是Φ中出现时间点的集合,a∈A,t∈T.Φ的典范模
c
c
c
c
型 M =〈W ,R ,V 〉定义如下.
c
(1) W ={Γ|Γ是Φ中的极大一致集};
*
c
c
*
*
*
*
(2) R 是一个函数:A×T →℘(W ×W ),其中,T ={0,1,…,n}⊇T.设 0<k≤n,对 R (a,t )归纳定义如下:
0
c
*
c
① 若Φ中无形如 K ϕ 的公式,R (a,0)=W ×W ;
a