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

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

m
(5) E ϕ → E ϕ (m<n) (4)E B m ϕ 与 E ϕ 的定义
n
n
B
B
B
m
n
m
m
(6) EC ϕ → E C ϕ (m<n) (5)公理模式
B
B
B
B
n
m
(7) C ϕ → E C ϕ (m<n) (2)(6)假言三段论
m
B
B
B
m
n
n
(8) CC ϕ → E C m B ) ϕ (m<n) (7)N C
(
B
B
B
(9) CC ϕ → B n ( m B E C m B ) ϕ (C ϕ → B m C C B m ) ϕ→ Ax8
n
n
B
B
(10) C ϕ → C C ϕ (m<n) (8)(9)MP
m
m
n
B
B
B
(11) C ϕ → ϕ (1)命题逻辑规则
m
B
m
n
(12) CC ϕ → ) ϕ (11)N C
(
B
B
n
(13) CC ϕ → B m ) ϕ (C C ϕ → B n B m → C B n ) ϕ Ax6
(
B
n
m
n
(14) CC ϕ → C ϕ (12)(13)MP
B
B
B
n
(15) C ϕ → C ϕ (m<n) (10)(14)假言三段论
m
B
B
t
t
据此,容易证明如下两个公式也是 S5 C 系统的内定理.
m
n
m
• “ C ϕ → C C ϕ ,m<n”,读作“如果群体 B 在 m 时形成公共知识ϕ并且 m 早于 n,那么群体 B 在 n 时形成
B
B
B
公共知识‘群体 B 在 m 时形成公共知识ϕ’”;
m
• “ C ϕ¬ m → C ¬ n C ϕ ,m<n”,读作“如果群体 B 在 m 时没有形成公共知识ϕ并且 m 早于 n,那么群体 B 在
B B B
n 时形成公共知识‘群体 B 在 m 时没有形成公共知识ϕ’”.
这说明随着时间的流逝,公共知识总是可以得到保留,并且群体总可以形成关于之前所有时刻认知状态(是
否形成公共知识)的公共知识.
t
定义 1.3(模型). 给定一个可数的常原子命题集 P,一个有穷主体集 A,自然数集 N 的一个有穷子集 T.S5 C t
系统合式公式的模型 M 是一个三元组〈W,R,V〉,其中,
• W 为可能世界的集合;
• R 是一个函数:A×T→℘(W×W).任意 R(a,t)满足以下两个条件.
(1) 等价关系(自返、传递和对称);
(2) 单调递减:对任意 m,n∈T,a∈A,如果 m<n,那么 R(a,m)⊇R(a,n);
• V 是一个赋值函数:P→℘(W).
要求 R 是单调递减函数,是为了使每个主体的不可区分世界有序对的集合随着时间的延伸只可能收缩而
不可能扩大,直观上是指随着时间的流逝,每个主体的不可区分世界越来越少.
定义 1.4(自返传递闭包). 令 R (, )Bt = ∪ R ( , )a t .(w,u)∈R E (B,t)表示群体 B 在 t 时刻从 w 经 1 步之后可以
E aB
∈
到达 u.如果存在一个序列 w 0 ,w 1 ,w 2 ,…,w n ,使得 w 0 =w,w n =s,并且对任意 0≤k<n 都有(w k ,w k+1 )∈R E (B,t),那么(w,s)∈
n
(R E (B,t)) ,这表示群体 B 在 t 时刻从 w 经 n 步之后可以到达 s.
R C (B,t)是 R E (B,t)的自返传递闭包,即一个满足下列 3 个条件的最小集合.
(1) R E (B,t)⊆R C (B,t);
(2) 对任意 w,u,v∈W,若(w,u)∈R C (B,t)并且(u,v)∈R C (B,t),则(w,v)∈R C (B,t);
(3) 对任意 w∈W,(w,w)∈R C (B,t).
定义 1.5(语义). 给定模型 M=〈W,R,V〉,公式ϕ在点模型(M,w)上是真的记为 M,wBϕ.本文将公式ϕ在满足等价
且单调递减框架类上的所有点模型上都是真的记为Bϕ.对 M,wBϕ的定义如下.
• M,wBp 当且仅当 w∈V(p);
• M,wB¬ϕ当且仅当 M,wHϕ;
• M,wBϕ∧ψ当且仅当 M,wBϕ并且 M,wBψ;
t
• Mw K ϕ 当且仅当对所有 v∈W,若(w,v)∈R(a,t),则 M,vBϕ;
, B
a