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

3792 Journal of Software 软件学报 Vol.31, No.12, December 2020

0
0
若Φ中有形如 K ϕ 的公式, R * ( ,0) {( , ) |{a = ΓΔ K ϕ | K ϕ Γ∈ a 0 } {K ϕ= 0 a | K ϕ Δ∈ 0 a }} .
a
a
*
*
k
② 若Φ中无形如 K ϕ 的公式,R (a,k)=R (a,k−1);
a
k
k
若Φ中有形如 K ϕ 的公式, R * (, ) {( , ) |{ak = ΓΔ K ϕ | K ϕ Γ∈ a k } {K ϕ= a k | K ϕ Δ∈ a k }}.
a
a
c
c
c
c
*
*
R 是 R 上的一个限制函数:A×T→℘(W ×W ),即 R (a,t)={(Γ,Δ)∈R (a,t)|(a,t)∈A×T}.
c
c
(3) V (p)={Γ∈W |p∈Γ}.
c
之所以如上定义 R ,是因为存在一些如“ K p¬ 1 ∧ K p ”这样的公式,其闭包中不含 K ϕ 和 K ϕ 的形式,但在
3
1
3
a b a b
c
t
t
c
典范模型中仍然需要定义出 R (a,3)和 R (b,1),否则,其典范模型不可能是 S5 C 系统的模型.对此问题的第 2 种解
t
t
决方法是:将定义 1.3 中 S5 C 系统的模型修改为四元组〈W,f,R,V〉,其中,f 是一个函数,A→℘(T).即,为每个主体指
派一些时间点,这样在定义典范模型时,可以相应地将一些无意义的(a,t)二元组删除.这两种补救方法都可以在
t
t
技术上实现定义出的典范模型是 S5 C 系统模型的目标,因此二者效果是相同的.本文出于对克里普克模型三元
组〈W,R,V〉的敬意,采纳第 1 种解决方法.
引理 2.2. 令Φ是某公式的闭包,则Φ的每个一致子集都是Φ中某个极大一致集的子集.
证明:令Δ⊆Φ是一致集并且|Φ|=n,令ϕ k 是Φ中第 k 个公式.考虑如下公式集的序列.
① Γ 0 =Δ;
② 若Γ k ∪{ϕ k+1 }是一致集,则Γ k+1 =Γ k ∪{ϕ k+1 };
若Γ k ∪{ϕ k+1 }不是一致集,则Γ k+1 =Γ k .
显然,Δ⊆Γ n ,我们需要证明Γ n 是Φ中的极大一致集.首先,对 k 进行归纳可知,每个Γ k 都是一致集,所以Γ n 是一
致集.另外,任取公式ϕ k ∈Φ,假设ϕ k ∉Γ n .所以,Γ k−1 ∪{ϕ k }是不一致的,那么Γ n ∪{ϕ k }也是不一致的.由于ϕ k ∈Φ是任取
的,所以不存在Γ′⊆Φ,使得Γ⊂Γ′且Γ′是一致的.即,Γ n 也是Φ中的极大集.
定义 2.4(路径). 令Φ是某公式的闭包,Γ是Φ中的某个极大一致集.
一个从Γ开始的“B(t)-路径”是指Φ中的某些极大一致集的序列Γ 0 ,…,Γ n .这个序列满足:对任意 k(0≤k<n),都
c
存在 a∈B,使得(Γ k ,Γ k+1 )∈R (a,t)且Γ 0 =Γ.一个“ϕ-路径”是Φ中的某些极大一致集的序列Γ 0 ,…,Γ n .这个序列满足:对
任意 k(0≤k<n),都有ϕ∈Γ k .路径Γ 0 ,…,Γ n 的长度是 n.若路径Γ 0 ,…,Γ n 既是 B(t)-路径又是ϕ-路径,则称其为“B(t)-ϕ-
路径”.
c
c
c
c
引理 2.3. 令Φ是某公式的闭包,M =〈W ,R ,V 〉是Φ的典范模型,Γ与Δ是Φ中的极大一致集.则如下几点成立:
(1) Φ中的Γ是演绎封闭的(对任意ϕ∈Φ,若AΓ→ϕ,则ϕ∈Γ);
(2) 若¬ϕ∈Φ,则ϕ∈Γ当且仅当¬ϕ∉Γ;
(3) 若(ϕ∧ψ)∈Φ,则(ϕ∧ψ)∈Γ当且仅当(ϕ∈Γ且ψ∈Γ);
(4) 若 Γ K Δ ∧〈 a t 〉 是一致的,则(Γ,Δ)∈R (a,t);
c
(5) 若 K ψ Φ∈ ,则{K ϕ | K ϕ t Γ ∈ } ψ ├ 当且仅当{K ϕ | K ϕ t Γ ∈ } K ψ├ t ;
t
t
t
a a a a a a
(6) A∨{Γ|Γ是Φ中的极大一致集};
c
t
(7) 若 K t a ϕ Φ∈ ,则(Γ,Δ)∈R (a,t)当且仅当{K ϕ | K ϕ a t Γ ∈ } Δ⊆ ;
a
(8) 若 C t B ϕ Φ∈ ,则 C t B ϕ Γ∈ 当且仅当始于Γ的每个 B(t)-路径都是ϕ-路径.
证明:可以参考文献[18],仅在原有 S5C 系统认知算子上增加时间参数,证明方法相同. □
c
c
c
c
c
引理 2.4(真值引理). 令Φ是某公式的闭包,令 M =〈W ,R ,V 〉是关于Φ的典范模型.则对任意ϕ∈Φ,任意Γ∈W ,
c
M ,ΓBϕ当且仅当ϕ∈Γ.
证明:对公式ϕ∈Φ的结构进行归纳证明.
c
(1) 假设ϕ是一个命题变元 p.由典范模型的定义可知,p∈Γ当且仅当Γ∈V (p).根据语义定义可知,p∈Γ当且
c
仅当 M ,ΓBp;
c
c
(2) 假设对任意极大一致集Γ和任意公式ϕ,ψ∈Φ,都成立 M ,ΓBϕ当且仅当ϕ∈Γ,成立 M ,ΓBψ当且仅当
ψ∈Γ.现在考虑公式ϕ∈Φ的其他结构形式.