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

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

t
t
为 S5 C 系统.
t
t
1 S5 C 系统及其可靠性证明
定义 1.1(形式语言). 令 P={p,q,...}表示一个可数的常原子命题集;A 表示一个有穷主体集,B⊆A,a∈A;T 是自
t
t
然数集 N(表明我们理解的时间是离散并且有起点)的一个有穷子集,T⊂N,t,m,n∈T.S5 C 系统的合式公式递归定
义如下:
t
ϕ :: p= | ϕϕ¬ | → ϕ | K ϕ | C ϕ .
t
a
B
t
t
K ϕ 读作主体 a 在时刻 t 知道ϕ; C ϕ 读作公式ϕ在 t 时刻是群体 B 的公共知识.定义其他合式公式.
B
a
• ϕ∧ψ=¬(ϕ→¬ψ);ϕ∨ψ=¬ϕ→ψ;ϕ↔ψ=(ϕ→ψ)∧(ψ→ϕ);
t
t
• E ϕ = ∧ aB K ϕ ,读作 B 中所有主体在时刻 t 都知道ϕ;
B ∈ a
• 〈 K ϕ〉 t = ¬ K ¬ t ϕ ,读作主体 a 在时刻 t 认为ϕ是可能的.
a a
t
t
定义 1.2. S5 C 系统是一个如下形式的希尔伯特式公理系统.
Ax0:所有经典命题逻辑重言式特例
Ax1: K t a (ϕ → ψ ) → (K ϕ t a → K ψ t a ) 个体知识分配公理
Ax2: K ϕ → ϕ 知识公理
t
a
t
t
t
Ax3: K ϕ → KK ϕ 正内省公理
a
a
a
t
Ax4: K ϕ¬ a t → K ¬ a t K ϕ 负内省公理
a
Ax5: K ϕ → K ϕ (m<n) 个体记忆公理
m
n
a
a
Ax6: C B t (ϕ → ψ ) → (C ϕ t B → C ψ t B ) 公共知识分配公理
t
Ax7: C ϕ → B t (ϕ E C t B ) ϕ ∧ 固定点公理
B
Ax8: C B t (ϕ → E t B ) ϕ (ϕ → C t B ) ϕ→ 归纳公理
MP:从ϕ和ϕ→ψ推出ψ;
t
N K :从ϕ推出 K ϕ ;
a
t
N C :从ϕ推出 C ϕ .
B
Ax5 刻画个体完美回忆,读作“如果主体 a 在时刻 m 知道ϕ并且 m 早于 n,那么主体 a 在时刻 n 知道ϕ”.其余
公理模式及推理规则都是在 S5C 系统中的 K,C 算子上加入时间点 t 作为上标而已,例如,Ax4 表示主体的负内
省是在当前时间点完成的.
t
命题 1.1(导出规则). Aϕ→ψ,则 K ϕ →├ t a K ψ .
a
证明:
(1) ϕ→ψ 假设
(2) K t (ϕ → ψ ) (1) N K
a
(3) K t (ϕ → ψ ) → (K ϕ t → K ψ t ) Ax1
a a a
t
t
(4) K ϕ → K ψ (2),(3) MP
a a
m
t
t
命题 1.2. 公式“ C ϕ → C ϕ (m<n)”是 S5 C 系统的内定理.
n
B B
证明:
(1) C ϕ → B m (ϕ E C B m ) ϕ ∧ Ax7
m
B
(2) C ϕ → E C ϕ (1)命题逻辑规则
m
m
m
B
B
B
n
(3) K ϕ → K ϕ (m<n) Ax5
m
a
a
n
(4) ∧ aB K ϕ → ∧ ∈ m a a B K ϕ (m<n) (3)命题逻辑规则
∈
a