1977年, 图灵奖获得者Pnueli开创性地把时态逻辑引入计算机科学, 引发了对系统的动态行为推理的基本模式转变^[1], 使得时态逻辑成为反应式系统和并发式系统时进行规格说明和验证的工具, 在芯片、硬件的设计上被广泛运用.我国唐稚松院士将时态逻辑形式化理论与软件技术结合起来, 提出了第1个可执行时态逻辑语言XYZ/E^[2].该语言将状态转换的控制机制引入到逻辑系统之中.这一成果是软件工程领域中发展可执行时态逻辑的先驱.段振华教授开发的时态逻辑程序设计语言在并发系统、实时系统、混合系统 (形式验证)、互联网计算及嵌入式系统中都有重要应用^[3].随着计算机科学的进一步发展, 时态逻辑在软件工程、人工智能、模型检测、信息安全等方面也得到了广泛的应用.

极小时态逻辑Kt是一种比较简单的时态逻辑^[4].Kt的语言是在经典命题逻辑语言的基础上加入时态算子G, H构成, 它们的对偶算子分别定义为F $\phi $:=¬G¬ $\phi $和P $\phi $:=¬H¬ $\phi $.公式G $\phi $读作“ $\phi $将来总是真的”, H $\phi $读作“ $\phi $过去总是真的”, F $\phi $读作“ $\phi $将来可能真”, P $\phi $读作“ $\phi $过去可能真”.极小时态逻辑的语言的框架是一个关系框架 (W, R_F, R_P), 其中:W是非空集, 称为框架的域, R_F和R_P是W上的二元关系且对任意w, v∈W, wR_Fv当且仅当vR_Pw.关系R_F和R_P分别用来解释时态算子G和H, wR_Fv表示v是w的未来点, vR_Pw表示w是v的过去点.

Lemmon在1966年提出了极小非正规模态逻辑C2^[5], 它是在极小正规模态逻辑K中去掉正规性得到的, 即把系统K中概括规则替换为单调规则 (概括规则:从$\phi $推出□ $\phi $; 单调规则:从$\phi $→Ψ推出□ $\phi $→□Ψ).它是关系语义学 (克里普克语义学) 下极小的非正规模态逻辑.在C2中, □"不是定理, 即真不是必然的.雷蒙用正则模型 (W, N, R, V) 来解释C2, 其中, N⊆W中的点称为正规点, N之外的点称为非正规点; R⊆W²是W上的二元关系, 用来解释模态算子□.正则模型是非正规模态逻辑的模型, 它与通常的克里普克模型区别在于:正则模型中可以存在非正规点, 在非正规的点上, 矛盾是可能的.在文献[6]中, 我们将C2时态化处理, 得到极小非正规时态逻辑C2t, 它是Kt的子逻辑.该文还构造了C2t的带标矢列式系统.

可定义性是模型论的一个核心问题^[7], 它研究模型类或模型的性质在一个逻辑语言中可定义或可表达的问题.在研究时态逻辑的可定义性问题中, 互模拟的概念起着重要作用.互模拟概念也是理论计算机科学的一个重要概念, 在计算机科学中有广泛的应用, 例如在并发系统的研究中, 可以用来证明进程之间的等价性^[8].经典模态逻辑的互模拟概念是由荷兰逻辑学家van Benthem提出来的^[9].关于模态逻辑的互模拟有许多研究成果. Perkov研究了经典克里普克框架类在基本命题模态语言下的存在可定义性 (existential definability)^[10]; Kurtonina和De Rijke研究了带U, S算子的时态逻辑的互模拟^[11], 其中, U($\phi $, Ψ) 读作“直到$\phi $, Ψ为真”, S($\phi $, Ψ) 读作“自从$\phi $之后, Ψ为真”.Venema研究了经典模态逻辑的模型类可定义性的刻画问题^[12].这些工作主要研究经典的克里普克模型或框架的可定义性问题.本文的主要工作是研究正则模型的互模拟及其在时态语言下的可定义性.首先定义正则模型的不相交并、生成子模型、C2t-互模拟、时态饱和以及时态可定义性等概念, 然后证明一个正则模型类是时态可定义的当且仅当它在不相交并、满C2t-互模拟像、C2t-超滤扩张下封闭, 并且它的补类在C2t-超滤扩张下封闭.

1 语言和语义

时态逻辑的语言${\cal L}$_t由可数命题变元集Prop、命题常量⊥、命题联接词→、时态算子G和H组成.${\cal L}$_t公式由如下规则递归定义:

$\phi :: = p| \bot |(\phi \to \phi )|G\phi |H\phi ,{\rm{其中,}}p \in {Pr}op$

其他联结词定义如下:

$\begin{array}{l} \neg \phi : = \phi \to \bot ,\top: = \bot \to \bot ,\phi \vee \psi : = \neg \phi \to \psi ,\phi \wedge \psi : = \neg \left( {\neg \varphi \vee \neg \psi } \right),\varphi \leftrightarrow \psi :\\ = \left( {\phi \to \psi } \right) \wedge \left( {\psi \to \phi } \right),F\phi : = \neg G\neg \phi ,P\phi : = \neg H\neg \phi . \end{array}$

定义1.一个正则框架是$\mathfrak{F}$=(W, N, R_F, R_P), 其中:W是一个非空集合; N是W的子集; R_F和R_P是集合W上满足下面条件的二元关系:对任意w, v∈N, wR_Fv当且仅当vR_Pw.一个正则模型是$\mathfrak{M}$=(W, N, R_F, R_P, V), 其中, (W, N, R_F, R_P) 是正则框架框, V:Prop→$\mathcal{P}$(W) 是从Prop到W的幂集上的赋值函数.

定义2.一个公式$\phi $在正则模型$\mathfrak{M}$中点w上真 (记号$\mathfrak{M}$, w╞ $\phi $) 递归定义如下.

● $\mathfrak{M}$, w╞p当且仅当w∈V(p), 其中p∈Prop;

● $\mathfrak{M}$, w$\nVdash$⊥;

● $\mathfrak{M}$, w╞ $\phi $→Ψ当且仅当$\mathfrak{M}$, w $\nvDash \phi $或者$\mathfrak{M}$, w╞Ψ;

● $\mathfrak{M}$, w╞G $\phi $当且仅当w∈N并且$\forall $v∈W(wR_Fv⇒ $\mathfrak{M}$, v╞ $\phi $);

● $\mathfrak{M}$, w╞H $\phi $当且仅当w∈N并且$\forall $v∈W(wR_Pv⇒ $\mathfrak{M}$, v╞ $\phi $).

由定义2可得:

● $\mathfrak{M}$, w╞F $\phi $当且仅当w∉N或者∃v∈W(wR_Fv并且$\mathfrak{M}$, w╞ $\phi $);

● $\mathfrak{M}$, w╞P $\phi $当且仅当w∉N或者∃v∈W(wR_Pv并且$\mathfrak{M}$, w╞ $\phi $).

令V($\phi $)={w∈W| $\mathfrak{M}$, w╞ $\phi $}表示使得$\phi $为真的所有点的集合.称$\phi $在正则模型$\mathfrak{M}$上是全局真的 (记为$\mathfrak{M}$╞ $\phi $), 如果对任意w∈W, $\mathfrak{M}$, w╞ $\phi $.称公式集Σ在w上可满足 (记为$\mathfrak{M}$, w╞Σ), 如果对任意Ψ∈Σ, $\mathfrak{M}$, w╞Ψ.称Σ在一个正则模型类$\mathbb{K}$上可满足, 如果存在$\mathfrak{M}$'∈ $\mathbb{K}$, 使得Σ在$\mathfrak{M}$'某点上可满足.

2 C2t-互模拟

本节定义正则模型类上的C2t-互模拟概念, 证明时态公式在C2t-互模拟下保持不变.不相交并、生成子模型等正则模型类上运算都是C2t-互模拟的特殊情况.

定义3(时态等价).令$\mathfrak{M}$=(W, N, R_F, R_P, V) 和${\mathfrak{M}}'=({W}',{N}',{{{R}'}_{F}},{{{R}'}_{P}},{V}')$是两个正则模型, w和w'分别是$\mathfrak{M}$和$\mathfrak{M}$'上的点.w上的理论Th(w) 是在该点上为真的所有公式的集合, 即Th(w)={ $\phi $| $\mathfrak{M}$, w╞ $\phi $}.称w和w'时态等价 (记为w $\leftrightsquigarrow$w'), 如果Th(w)=Th(w'). $\mathfrak{M}$的理论Th($\mathfrak{M}$) 是在$\mathfrak{M}$所有点上都是真的公式构成的集合, 即Th($\mathfrak{M}$)={f| $\mathfrak{M}$╞ f}.称$\mathfrak{M}$和M'时态等价 (记为$\mathfrak{M} \leftrightsquigarrow \mathfrak{M}$'), 如果Th($\mathfrak{M}$)=Th($\mathfrak{M}$').

定义4.令$\mathfrak{M}$=(W, N, R_F, R_P, V) 和${\mathfrak{M}}'=({W}',{N}',{{{R}'}_{F}},{{{R}'}_{P}},{V}')$是正则模型.一个非空二元关系Z⊆W×W'称为$\mathfrak{M}$和$\mathfrak{M}$'之间的一个C2t-互模拟 (记为Z: $\mathfrak{M} \leftrightsquigarrow \mathfrak{M}$'), 如果下列条件成立:对任意w, v∈W和w', v'∈W', 如果wZw', 那么,

(1) 对任意p∈Prop, $\mathfrak{M}$, w╞p当且仅当$\mathfrak{M}$', w'╞p;

(2) w∈N当且仅当w'∈N';

(3) 如果wR_Fv, 那么存在点v'∈W'满足${w}'{{{R}'}_{F}}{v}'$并且vZv';

(4) 如果wR_Pv, 那么存在点v'∈W'满足${w}'{{{R}'}_{P}}{v}'$并且vZv';

(5) 如果${w}'{{{R}'}_{F}}{v}'$, 那么存在点v∈W满足wR_Fv并且vZv';

(6) 如果${w}'{{{R}'}_{P}}{v}'$, 那么存在点v∈W满足wR_Pv并且vZv'.

如果Z是$\mathfrak{M}$和$\mathfrak{M}$'之间的一个C2t-互模拟并且wZw', 那么称w和w'是C2t-互模拟的, 记为Z: $\mathfrak{M}$, w $\rightleftharpoons \mathfrak{M}$', w',有时简记为w $\rightleftharpoons $w'.称Z: $\mathfrak{M} \rightleftharpoons \mathfrak{M}$'是$\mathfrak{M}$和$\mathfrak{M}$'之间的一个满C2t-互模拟, 如果对任意w'∈W', 存在w∈W满足wZw'.这时称$\mathfrak{M}$'是$\mathfrak{M}$在满C2t-互模拟Z下的像.

定义5.称一个公式集Δ定义一个正则模型类$\mathbb{K}$, 如果对任意正则模型$\mathfrak{M}$, $\mathfrak{M}$∈ $\mathbb{K}$当且仅当$\mathfrak{M}$╞Δ.称一个正则模型类是时态可定义的, 如果存在一个公式集定义该正则模型类.

下面命题表明C2t-互模拟的两个点是时态等价的.

命题1.对任意正则模型$\mathfrak{M}$=(W, N, R_F, R_P, V) 和$\mathfrak{M}' = (W',N',{R'_F},{R'_P},V')$, 任意w∈W和w'∈W', 如果w $\rightleftharpoons $w', 那么w $\leftrightsquigarrow$w'.

证明:假设w $\rightleftharpoons $w', 那么存在C2t-互模拟关系Z: $\mathfrak{M}$, w=$\mathfrak{M}$', w'.只需证对任意公式$\phi $, $\mathfrak{M}$, w╞ $\phi $当且仅当$\mathfrak{M}$', w'╞ $\phi $.对公式$\phi $进行归纳. $\phi $是原子公式或者⊥时, 根据C2t-互模拟定义直接可得. $\phi $=$\phi $₀→f₁时易证. $\phi $=GΨ时, 设$\mathfrak{M}$, w╞GΨ, 则w∈N并且$\forall $v∈W(wR_Fv⇒ $\mathfrak{M}$, v╞Ψ).由于wZw', 所以w'∈N'.设v'∈W'并且${w}'{{{R}'}_{F}}{v}'$, 所以存在v∈W, 满足wR_Fv并且vZv'.所以$\mathfrak{M}$, v╞Ψ.由归纳假可得, $\mathfrak{M}$', v'╞Ψ.因此$\forall {v}'\in {W}'({w}'{{{R}'}_{F}}{v}'\Rightarrow {\mathfrak{M}}',{v}'\vDash \psi )$.即$\mathfrak{M}$', w'╞GΨ.反方向证明类似.f=HΨ时的证明和$\phi $=Gy类似.

命题2.正则模型的时态可定义类在满C2t-互模拟下是封闭的.

证明:设公式集Σ定义一个正则模型类$\mathbb{K}$, $\mathfrak{M}$和$\mathfrak{M}$'是任意正则模型并且$\mathfrak{M}$∈ $\mathbb{K}$.再设Z: $\mathfrak{M} \rightleftharpoons \mathfrak{M}$'是$\mathfrak{M}$和$\mathfrak{M}$'之间的满C2t-互模拟.下面证明$\mathfrak{M}$'∈ $\mathbb{K}$.设任意$\phi $∈Δ并且任意w'∈W'.由于Z: $\mathfrak{M} \rightleftharpoons \mathfrak{M}$'是满C2t-互模拟, 所以∃w∈W满足wZw'.又因$\mathfrak{M}$∈ $\mathbb{K}$, 所以$\mathfrak{M}$╞D.所以$\mathfrak{M}$╞ $\phi $.所以$\mathfrak{M}$, w╞ $\phi $.根据命题1, 有$\mathfrak{M}$', w'╞ $\phi $.根据$\phi $和w'的任意性, 可得$\mathfrak{M}$'╞Δ.所以$\mathfrak{M}$'∈ $\mathbb{K}$.

对任意一族正则模型, 称它们是互不相交的, 如果它们的域两两之间没有共同的元素.显然, 如果它们的域不是互不相交的, 那么总是可以取与它们同构的模型, 使得它们的域彼此之间互不相交.

定义6.令{ $\mathfrak{M}$_i|i∈I}是一族正则模型, 其中, ${{\mathfrak{M}}_{i}}=({{W}_{i}},{{N}_{i}},R_{F}^{i},R_{P}^{i},{{V}_{i}})$, i∈I.不妨设{ $\mathfrak{M}$_i|i∈I}是互不相交的.它们的不相交并是${{\uplus }_{i\in I}}{{\mathfrak{M}}_{i}}=(W,N,{{R}_{F}},{{R}_{P}},V)$, 其中,

(1) $W=\bigcup\nolimits_{i\in I}{{{W}_{i}}}$;

(2) $N=\bigcup\nolimits_{i\in I}{{{N}_{i}}}$;

(3) ${{R}_{F}}=\bigcup\nolimits_{i\in I}{R_{F}^{i}}$;

(4) ${{R}_{P}}=\bigcup\nolimits_{i\in I}{R_{P}^{i}}$;

(5) $V(p)=\bigcup\nolimits_{i\in I}{{{V}_{i}}(p)}$, 其中, p∈Prop.

命题3.任意一族正则模型的不相交并是正则模型.

证明:根据不相交的定义易证.

命题4.正则模型的时态可定义类对不相交并封闭.

证明:设正则模型类$\mathbb{K}$是由公式集Σ定义并且{ $\mathfrak{M}$_j|j∈I}⊆ $\mathbb{K}$.下面证明${{\uplus }_{j\in I}}{{\mathfrak{M}}_{j}}\in \mathbb{K}.$设任意$\phi $∈Δ并且任意$w\in \bigcup\nolimits_{j\in I}{{{W}_{j}}}.$那么∃i∈I, w∈W_i.容易验证, 关系{ < v, v > |v∈W_i}是$\mathfrak{M}$_i和${{\uplus }_{j\in I}}{{\mathfrak{M}}_{j}}$之间的C2t-互模拟.因为$\mathfrak{M}$_i∈ $\mathbb{K}$, 所以$\mathfrak{M}$_i╞Δ.因此$\mathfrak{M}$_i, w╞ $\phi $.所以${{\uplus }_{j\in I}}{{\mathfrak{M}}_{j}},w\vDash \phi .$所以$\forall \phi $∈Δ, $\forall w\in \bigcup\nolimits_{j\in I}{{{W}_{j}}},{{\uplus }_{j\in I}}{{\mathfrak{M}}_{j}},w\vDash \phi ,$即${{\uplus }_{j\in I}}{{\mathfrak{M}}_{j}}\vDash \Delta .$所以${{\uplus }_{j\in I}}{{\mathfrak{M}}_{j}}\in \mathbb{K}.$

定义7.对任意正则模型$\mathfrak{M}$=(W, N, R_F, R_P, V) 和${\mathfrak{M}}'=({W}',{N}',{{{R}'}_{F}},{{{R}'}_{P}},{V}')$, 称$\mathfrak{M}$'是$\mathfrak{M}$的子模型, 如果W'⊆W, N'=N∩W', ${{{R}'}_{F}}={{R}_{F}}\cap ({W}'\times {W}'),{{{R}'}_{P}}={{R}_{P}}\cap ({W}'\times {W}')$, V'(p)=V(p)∩W', 其中, p∈Prop.称$\mathfrak{M}$'是$\mathfrak{M}$的生成子模型, 如果$\mathfrak{M}$'是$\mathfrak{M}$的子模型, 并且满足下面的封闭条件:如果w∈W'并且w(R_F∪R_P)v, 那么v∈W'.其中, R_F∪R_P表示关系R_F和R_P的并, 即对任意w, v∈W, w(R_F∪R_P)v当且仅当wR_Fv或者wR_Pv.

递归定义集合W上的二元关系 (R_F∪R_P)ⁿ如下.

(1) w(R_F∪R_P)⁰v当且仅当w=v;

(2) w(R_F∪R_P)ⁿ⁺¹v当且仅当∃w'∈W满足w(R_F∪R_P)w'并且w'(R_F∪R_P)ⁿv.

给定W中的一点w, 存在最小的包含w的生成子模型, 该生成子模型记为$\mathfrak{M}$_w.易知, $\mathfrak{M}$_w的域是w通过关系 (R_F∪R_P) 在有穷步内到达的所有点构成的集合.下面给出$\mathfrak{M}$_w的定义: ${{\mathfrak{M}}_{w}}=({{W}_{w}},{{N}_{w}},R_{F}^{w},R_{P}^{w},{{V}_{w}})$, 其中,

(1) W_w={v∈W|w(R_F∪R_P)ⁿv, n∈N};

(2) N_w=N∩W_w;

(3) $R_{F}^{w}={{R}_{F}}\cap ({{W}_{w}}\times {{W}_{w}})$;

(4) $R_{P}^{w}={{R}_{P}}\cap ({{W}_{w}}\times {{W}_{w}})$;

(5) V_w=V(p)∩W_w, 其中, p∈Prop.

其中, N表示自然数集合.

命题5.对任意正则模型$\mathfrak{M}$和$\mathfrak{M}$中任意点w.

(1) $\mathfrak{M}$和$\mathfrak{M}$_w之间存在一个满C2t-互模拟;

(2) ${{\uplus }_{v\in W}}{{\mathfrak{M}}_{v}}$和$\mathfrak{M}$之间存在一个满C2t-互模拟.

证明:

(1) 容易验证, 关系{ < v, v > |v∈W_w}是$\mathfrak{M}$和$\mathfrak{M}$_w之间的一个满C2t-互模拟;

(2) 容易验证, 关系$\{ v,{v}' |v\in {{\uplus }_{w\in W}}{{\mathfrak{M}}_{w}},{v}'\in \mathfrak{M}$并且v'和v是相同的点的副本}是${{\uplus }_{w\in W}}{{\mathfrak{M}}_{w}}$和$\mathfrak{M}$之间的一个满C2t-互模拟.

由命题5可得如下推论:

推论1.如果是$\mathbb{K}$是任意时态可定义的正则模型类, 那么对任意正则模型$\mathfrak{M}$, $\mathfrak{M}$∈ $\mathbb{K}$当且仅当对任意点w∈ $\mathfrak{M}$, $\mathfrak{M}$_w∈ $\mathbb{K}$.

证明:假设公式集Σ定义$\mathbb{K}$.下面证从左到右方向:设$\mathfrak{M}$∈ $\mathbb{K}$.那么$\mathfrak{M}$╞Δ.设w∈W.再设$\phi $∈Δ, v∈W_w.那么v∈W.因此$\mathfrak{M}$, v╞ $\phi $.根据命题5(1) 的证明, { < u, u > |u∈W_w}是$\mathfrak{M}$和$\mathfrak{M}$_w之间的满C2t-互模拟, 所以$\mathfrak{M}$_w, v╞ $\phi $.所以$\forall \phi $∈Δ, $\forall $v∈W_w, $\mathfrak{M}$_w, v╞ $\phi $.所以$\mathfrak{M}$_w╞Δ.因此$\mathfrak{M}$_w∈ $\mathbb{K}$.所以$\forall $w∈W, $\mathfrak{M}$_w∈ $\mathbb{K}$.从右到左方向:设$\forall $w∈W, $\mathfrak{M}$_w∈ $\mathbb{K}$, 因此$\forall $w∈W, M_w╞Δ.所以${{\uplus }_{w\in W}}{{\mathfrak{M}}_{w}}\vDash \Delta $.再设w∈W并且$\phi $∈Δ, 那么${{\uplus }_{w\in W}}{{\mathfrak{M}}_{w}}\vDash \phi $.根据命题5(2), ${{\uplus }_{w\in W}}{{\mathfrak{M}}_{w}}$和$\mathfrak{M}$存在满C2t-互模拟, 所以$\mathfrak{M}$, w╞ $\phi $.所以$\forall $w∈W, $\forall \phi $∈Δ, $\mathfrak{M}$, w╞ $\phi $, 即$\mathfrak{M}$╞Δ.所以$\mathfrak{M}$∈ $\mathbb{K}$.

3 时态饱和

在模态逻辑中, 互模拟蕴涵模态等价, 但是反过来不必然成立.在饱和模型类上, 两个模态等价的模型是互模拟的^[13].在正则时态逻辑中, 也可以定义时态饱和的正则模型类, 可以证明正则模型类的时态等价蕴涵C2t-互模拟.

令Σ是一个公式集, $\mathfrak{M}$=(W, N, R_F, R_P, V) 是正则模型, 并且A⊆W.称Σ在A上可满足, 如果Σ在A中某点上可满足; 称Σ在A上有穷可满足, 如果Σ的任意有穷子集在A上可满足.

定义8.称一个正则模型$\mathfrak{M}$=(W, N, R_F, R_P, V) 是时态饱和的, 如果下面的条件成立:对任意w∈W, 任意公式集Σ:

(1) 如果w ∉N, 那么R_F[w]=R_P[w]=∅;

(2) 如果Σ在R_F[w]上有穷可满足, 那么Σ在R_F[w]上可满足;

(3) 如果Σ在R_P[w]上有穷可满足, 那么Σ在R_P[w]上可满足.

其中, 表示空集, R_F[w]={v∈W|wR_Fv}, R_P[w]={v∈W|wR_Pv}.

命题6.令$\mathfrak{M}$和$\mathfrak{M}$'是时态饱和的正则模型, 并且w和w'分别是$\mathfrak{M}$和$\mathfrak{M}$'上的点.那么w $\rightleftharpoons $w'当且仅当w $\leftrightsquigarrow$w'.

证明:

●从左到右方向是显然的.

●从右到左方向:

设w $\leftrightsquigarrow$w'.下面证明时态等价关系$\leftrightsquigarrow$是C2t-互模拟关系.只需验证$\leftrightsquigarrow$是满足C2t-互模拟的4个条件.第1个和第2个条件显然成立.第3个条件验证如下:假设w $\leftrightsquigarrow$w'并且wR_Fv.根据时态饱和的定义, 可得w∈N.所以w'∈N'.令Σ={ $\phi $| $\mathfrak{M}$, v ╞ $\phi $}.为了证明v和w'的某个后继点时态等价, 只需证Σ在${{{R}'}_{F}}[{w}']$上可满足.根据时态饱和的定义, 只需证Σ在${{{R}'}_{F}}[{w}']$中有穷可满足.假设Σ₀是Σ的任意有穷子集, 显然$\mathfrak{M}$, w╞FΨ, 其中, Ψ=$\wedge $Σ₀.由于w $\leftrightsquigarrow$w', 所以$\mathfrak{M}$', w'╞FΨ.又因w∈N', 所以∃v'∈ $\mathfrak{M}$', 使得${w}'{{{R}'}_{F}}{v}'$并且$\mathfrak{M}$', v'╞Ψ.所以Σ₀在${{{R}'}_{F}}[{w}']$上可满足.因此, Σ在${{{R}'}_{F}}[{w}']$上有穷可满足, 所以Σ在${{{R}'}_{F}}[{w}']$上可满足.对关系R_P验证与R_F类似.第4个条件的验证与第3条类似.

4 C2t-超滤扩张

在模态逻辑中, 一个模型的超滤扩张是模态饱和的^[12].在时态逻辑中, 本节定义正则模型的C2t-超滤扩张, 并且证明任何正则模型的C2t-超滤扩张是时态饱和的.

对任意集合W, 集合族u⊆$\mathcal{P}$(W) 称为W上的超滤子, 如果满足下面的条件:

(1) 如果A, B∈u, 那么A $\cap $B∈u;

(2) 如果A∈u并且A⊆B⊆W, 那么B∈u;

(3) 对任意A⊆W, A∈u当且仅当A^c∉u.

其中, $\mathcal{P}$(W)={A|A⊆W}是W的幂集, A^c表示A相对于W的补集.

对任意集族E⊆$\mathcal{P}$(W), 称E具有有穷交性质, 如果E中任意有穷个集合的交集非空, 即如果A_i∈E, i∈n, 那么,

$\bigcap\nolimits_{i\in n}{{{A}_{i}}}\not{=}\varnothing .$

事实1.对任意w∈W, 容易验证 $\pi $_w={A⊆W|w∈A}是W上的超滤子, 并且称 $\pi $_w是由w生成的主超滤子.对任意集族E⊆P(W), 如果E具有有穷交性质, 那么E可以扩张为一个超滤子, 即存在W上的一个超滤子u, 使得E⊆u.

事实2. 如果E⊆$\mathcal{P}$(W) 是W上的任意超滤子, 那么,

(1) 对任意A, B∈$\mathcal{P}$(W), 有A∪B∈u当且仅当A∈u或B∈u.

(2) W∈u.

(3) ∅∉u.

(4) 如果u包含一个有穷集, 那么u是W中的某个元素生成的主超滤子.因此当W是有穷集时, 其上的超滤子恰好有|W|个.

关于事实1、事实2的证明可参考文献[14].

定义9.对任意正则框架$\mathfrak{F}$=(W, N, R_F, R_P), 在W幂集上定义4个运算如下:

●F(X):={w∈W|w∉N或者∃v∈W(wR_Fv并且v∈X)};

●G(X):={w∈W|w∈N并且$\forall $v∈W(wR_Fv⇒v∈X)};

●P(X):={w∈W|w∉N或者∃v∈W(wR_Pv并且v∈X)};

●H(X):={w∈W|w∈N并且$\forall $v∈W(wR_Pv⇒v∈X)}.

命题7.对任意正则框架$\mathfrak{F}$=(W, N, R_F, R_P), 任意X, Y⊆W, 有:

(1) G(X)=(F(X^c))^c;

(2) H(X)=(P(X^c))^c;

(3) F(X)=(G(X^c))^c;

(4) P(X)=(H(X^c))^c;

(5) G(X $\cap $Y)=G(X) $\cap $G(Y) 并且H(X $\cap $Y)=H(X) $\cap $H(Y);

(6) 如果X⊆Y, 那么G(X)⊆G(Y) 并且H(X)⊆H(Y).

证明:根据F, G, P, H的定义易证.

定义10(C2t-超滤扩张).对任意正则框架$\mathfrak{F}$=(W, N, R_F, R_P), 结构$\mathfrak{u}\mathfrak{e}\mathfrak{F}=(Uf(W),{{N}^{ue}},R_{F}^{ue},R_{P}^{ue})$称为$\mathfrak{F}$的C2t-超滤扩张, 其中,

(1) Uf(W):={u|u是W上的超滤子};

(2) N^ue:={u∈Uf(W)|N∈u};

(3) u₀∈N^ue时, ${{u}_{0}}R_{F}^{ue}{{u}_{1}}$当且仅当{A|G(A)∈u₀}⊆u₁;

(4) u₀ $\notin $N^ue时, $R_{F}^{ue}[{{u}_{0}}]=\varnothing $;

(5) u₀∈N^ue时, ${{u}_{0}}R_{P}^{ue}{{u}_{1}}$当且仅当{A|H(A)∈u₀}⊆u₁;

(6) u₀ $\notin $N^ue时, $R_{P}^{ue}[{{u}_{0}}]=\varnothing $.

命题8.对任意u₀, u₁∈Uf(W):

(1) 如果u₀∈N^ue, 那么${{u}_{0}}R_{F}^{ue}{{u}_{1}}$当且仅当{F(A)|A∈u₁}⊆u₀;

(2) 如果u₀∈N^ue, 那么${{u}_{0}}R_{P}^{ue}{{u}_{1}}$当且仅当{P(A)|A∈u₁}⊆u₀;

(3) 如果G(A)∈u₀, 那么u₀∈N^ue并且对任意v∈Uf(W), ${{u}_{0}}R_{F}^{ue}v$蕴涵A∈v;

(4) 如果H(A)∈u₀, 那么u₀∈N^ue并且对任意v∈Uf(W), ${{u}_{0}}R_{P}^{ue}v$蕴涵A∈v.

证明:

(1) 设u₀∈N^ue, 再设${{u}_{0}}R_{F}^{ue}{{u}_{1}}$并且A∈u₁.由超滤子定义可知, A^c∉u₁.由${{u}_{0}}R_{F}^{ue}{{u}_{1}}$定义可知, G(A^c) $\in $u₀.所以 (G(A^c))^c∈u₀.因此F(A)∈u₀.反过来, 设{F(A)|A∈u₁}⊆u₀并且G(A)∈u₀.由命题7(1) 可得, (F(A^c))^c∈u₀.所以F(A^c)∉u₀.所以A^c∉u₁.因此A∈u₁.所以${{u}_{0}}R_{F}^{ue}{{u}_{1}}$.

(2) 证明与 (1) 类似.

(3) 设G(A)∈u₀.因为G(A)={w∈W|w∈N并且$\forall $v∈W(wR_Fv⇒v∈A)}, 所以G(A)⊆N.所以N∈u₀.因此u₀∈N^ue.再设${{u}_{0}}R_{F}^{ue}v$, 那么{B|G(B)∈u₀}⊆v.因为G(A)∈u₀, 所以A∈v.

(4) 证明与 (3) 类似.

命题9.对任意集合A⊆W, 任意超滤子u₀∈Uf(W):

(1) 如果F(A)∈u₀, 那么u₀∉N^ue或者存在u₁∈Uf(W) 使得${{u}_{0}}R_{F}^{ue}{{u}_{1}}$并且A∈u₁;

(2) 如果P(A)∈u₀, 那么u₀∉N^ue或者存在u₁∈Uf(W) 使得${{u}_{0}}R_{P}^{ue}{{u}_{1}}$并且A∈u₁.

证明:设F(A)∈u₀并且u₀∉N^ue.下面构造超滤子u₁使得${{u}_{0}}R_{F}^{ue}{{u}_{1}}$并且A∈u₁.

令${{{u}'}_{1}}=\{A\}\cup \{B|GB\in {{u}_{0}}\}$.下面证明${{{u}'}_{1}}$具有有穷交性质.假设${{{u}'}_{1}}$不具有穷交性质, 那么存在自然数n, 使得A $\cap $B₁ $\cap $… $\cap $B_n=∅, 其中B_i∈{B|GB∈u₀}, i≤n.所以B₁ $\cap $… $\cap $B_n⊆A^c.因此G(B₁ $\cap $… $\cap $B_n)⊆G(A^c).所以G(B₁) $\cap $… $\cap $G(B_n)⊆ G(A^c).因为G(B_i)∈u₀, i≤n.所以G(B₁) $\cap $… $\cap $G(B_n)∈u₀.所以G(A^c)∈u₀.因此 (G(A^c))^c∉u₀.根据命题7(3), F(A)∉u₀, 这与假设矛盾.所以${{{u}'}_{1}}$具有有穷交性质.因此${{{u}'}_{1}}$可以扩张为一个超滤子u₁.由u₁的构造可知, ${{u}_{0}}R_{F}^{ue}{{u}_{1}}$并且A∈u₁.

(2) 的证明与 (1) 类似.

命题10.对任意正则框架$\mathfrak{F}$=(W, N, R_F, R_P), 它的C2t-超滤扩张$\mathfrak{u}\mathfrak{e}\mathfrak{F}=(Uf(W),{{N}^{ue}},R_{F}^{ue},R_{P}^{ue})$是正则框架.

证明:设u₀, u₁∈N^ue, 再设${{u}_{0}}R_{F}^{ue}{{u}_{1}}$并且H(A)∈u₁.由命题8(1) 可得, F(H(A))∈u₀.容易验证N^c∪(F(H(A)))^c∪A=W∈ u₀.由于u₀是超滤子并且F(H(A))∈u₀, N∈u₀.根据事实2, A∈u₀.因此${{u}_{1}}R_{P}^{ue}{{u}_{0}}$.反过来, 设${{u}_{1}}R_{P}^{ue}{{u}_{0}}$并且A∈u₁.容易验证N^c∪A^c H(F(A))=W∈u₁.由于u₁是超滤子并且N∈u₁, A∈u₁.根据事实2, H(F(A))∈u₁.所以F(A)∈u₀.因此${{u}_{0}}R_{F}^{ue}{{u}_{1}}$.

定义11.对任意正则模型$\mathfrak{M}$=($\mathfrak{F}$, V), $\mathfrak{ueM}$=(ueF, V^ue) 称为$\mathfrak{M}$的C2t-超滤扩张, 其中V^ue定义为

${V^{ue}}(p) = \{ u \in Uf(W)|V(p) \in u\} ,{\rm{ 对任意}}p \in Prop.$

显然, 任意正则模型的C2t-超滤扩张是正则模型.

命题11.对任意正则模型$\mathfrak{M}$=($\mathfrak{F}$, V), 任意公式$\phi $以及W上超滤子u, 有:

V($\phi $)∈u当且仅当$\mathfrak{ueM}$, u╞ $\phi $.

证明:对公式$\phi $进行归纳. $\phi $是原子命题或者⊥时, 根据C2t-超滤扩张定义易得. $\phi $=$\phi $₀→ $\phi $₁时易证. $\phi $=GΨ时, 从左到右方向:设V(GΨ)∈u.那么G(V(Ψ))∈u.所以u∈N^ue并且对任意超滤子v, 如果$uR_{F}^{ue}v$, 那么V(Ψ)∈v.再设v是任意超滤子并且$uR_{F}^{ue}v$, 那么V(Ψ)∈v.根据归纳假设, $\mathfrak{ueM}$, v╞Ψ, 所以$\forall v(uR_{F}^{ue}v\Rightarrow \mathfrak{u}\mathfrak{e}\mathfrak{M},v\vDash \psi )$, 即$\mathfrak{ueM}$, u╞GΨ.从右到左方向:设$\mathfrak{ueM}$, u╞GΨ, 那么u∈N^ue并且$\forall v(uR_{F}^{ue}v\Rightarrow \mathfrak{u}\mathfrak{e}\mathfrak{M},v\vDash \psi )$.再设G(V(Ψ))∉u.所以 (G(V(Ψ)))^c∈u.因此F((V(Ψ))^c)∈u.由于u∈N^ue, 所以存在超滤子v, 使得$uR_{F}^{ue}v$并且 (V(Ψ))^c∈v.所以$\mathfrak{ueM}$, v╞Ψ.根据归纳假设可得, V(y)∈v.这与 (V(Ψ))^c∈v矛盾.所以G(V(Ψ))∈u, 即V(GΨ)∈u.f=HΨ时, 证明与上面类似.

命题12.对任意正则模型$\mathfrak{M}$和其中任意点w, 有w $\leftrightsquigarrow$ $\pi $_w.

证明:只需证对任意w∈W和任意$\phi $, $\mathfrak{M}$, w╞ $\phi $当且仅当$\mathfrak{ueM}$, $\pi $_w╞ $\phi $.从左到右方向:假设$\mathfrak{M}$, w╞ $\phi $.那么w∈V(f), 所以V($\phi $)∈ $\pi $_w.根据命题11, 有$\mathfrak{ueM}$, p_w╞ $\phi $.从右到左方向:假设$\mathfrak{ueM}$, $\pi $_w╞ $\phi $.那么V($\phi $)∈ $\pi $_w.根据命题11, 有w∈V($\phi $), 所以$\mathfrak{M}$, w╞ $\phi $.

命题13.对任意公式$\phi $和任意正则模型$\mathfrak{M}$, $\mathfrak{M}$╞ $\phi $当且仅当$\mathfrak{ueM}$╞ $\phi $.

证明:从左到右方向:设$\mathfrak{M}$╞ $\phi $.那么V($\phi $)=W.因为W属于W上任意超滤子, 再根据命题11, 对任意u∈Uf(W), $\mathfrak{ueM}$, u╞ $\phi $, 所以$\mathfrak{ueM}$╞ $\phi $.从右到左方向:设$\mathfrak{M} \vDash \phi $.那么∃w∈W, $\mathfrak{M}$, w $\vDash \phi $.根据命题12, $\mathfrak{ueM}$, p_w $\vDash \phi $.所以$\mathfrak{ueM} \vDash \phi $.

命题14.正则模型的时态可定义类和它的补类在C2t-超滤扩张下封闭.

证明:从命题13显然可得.

命题15.对任意正则模型$\mathfrak{M}$, $\mathfrak{ueM}$是时态饱和的.

证明:令$\mathfrak{M}$=(W, N, R_F, R_P, V) 是任意正则模型.下面验证$\mathfrak{u}\mathfrak{e}\mathfrak{M}=(Uf(W),{{N}^{ue}},R_{F}^{ue},R_{P}^{ue},{{V}^{ue}})$满足时态饱和的3个条件.

饱和条件1:根据C2t-超滤扩张的定义显然可得.

饱和条件2:设Σ是任意公式集, u是W上任意超滤子, 再设Σ在$R_{F}^{ue}[u]$上有穷可满足, 那么对Σ的任意有穷子集Σ₀, 存在点v∈Uf(W), 使得$uR_{F}^{ue}v$并且$\mathfrak{ueM}$, v╞Σ₀.因为Σ总是存在有穷子集的, 所以u在关系$R_{F}^{ue}$下存在后继点.

根据C2t-超滤扩张的定义, 有u∈N^ue.因为如果u $\notin $N^ue, 那么u不存在后继点.

令B={V($\phi $)| $\phi $∈Σ}∪{A|G(A)∈u}.下面证B有有穷交性质.

设$\phi $₁, …, φ_n∈Σ, 因为$\phi $₁ … $\wedge $φ_n在$R_{F}^{ue}[u]$可满足, 所以V($\phi $₁) $\cap $… $\cap $V(f_n)=V($\phi $₁ $\wedge $… $\wedge $φ_n)≠∅;并且对任意G(A₁), …, G(A_m)∈u, A₁ $\cap $… $\cap $A_m $\ne $∅.因为假设不然, G(A₁ $\cap $… $\cap $A_m)=G(∅).根据命题7(5), G(A₁) $\cap $… $\cap $G(A_m)=G(∅).所以G(∅)∈u.因为u在关系$R_{F}^{ue}$下存在后继点, 不妨记其中一个后继点为u'.根据命题8(3), 有∅∈u'.但这是不可能的.

所以, 要证B有有穷交性质, 只需证V($\phi $₁) $\cap $… $\cap $V(f_n) $\cap $A₁ $\cap $… $\cap $A_m $\ne $∅.因为{ $\phi $₁, …, φ_n}在$R_{F}^{ue}[u]$上可满足, 所以存在v∈Uf(W), 满足$uR_{F}^{ue}v$并且$\mathfrak{ueM}$, v╞($\phi $₁ $\wedge $… $\wedge $φ_n).根据命题11, V($\phi $₁ $\wedge $… $\wedge $φ_n)∈v; 又因G(A₁), …, G(A_m)∈u并且 $uR_F^{ue}v$, 根据命题8(3), 所以A₁, …, A_m∈v.所以V($\phi $₁) $\cap $… $\rightleftharpoons $V(f_n) $\rightleftharpoons $A₁ $\rightleftharpoons $… $\cap $A_m∅.所以B可以扩张为一个超滤子v.根据B的构造, 显然有$uR_{F}^{ue}v$并且$\mathfrak{ueM}$, v╞Σ.所以Σ在$R_{F}^{ue}[u]$可满足.

饱和条件3:与饱和条件2的验证类似.

命题16.令$\mathfrak{M}$和$\mathfrak{N}$是两个正则模型, w和v分别是$\mathfrak{M}$和$\mathfrak{N}$中的点, 那么w和v时态等价当且仅当它们相应的主超滤子是C2t-互模拟的, 即:

$\mathfrak{M},w\leftrightsquigarrow \mathfrak{n},v\text{当且仅当}\mathfrak{u}\mathfrak{e}\mathfrak{M},{{\pi }_{w}}\rightleftharpoons \mathfrak{u}\mathfrak{e}\mathfrak{n},{{\pi }_{w}}$

证明:根据命题12, $\mathfrak{M}$, w $\leftrightsquigarrow \mathfrak{N}$, v当且仅当$\mathfrak{ueM}$, $\pi $_w $\leftrightsquigarrow \mathfrak{ueN}$, $\pi $_v.根据命题6和命题15, $\mathfrak{ueM}$, p_w $\leftrightsquigarrow \mathfrak{ueN}$, $\pi $_v当且仅当$\mathfrak{ueM}$, $\pi $_w $\rightleftharpoons \mathfrak{ueN}$, $\pi $_v.

5 时态可定义性

本节运用前面定义的正则模型类上的运算, 证明一个正则模型类在时态语言中的可定义性的刻画定理.

引理1.对任意正则模型${\mathfrak{M}}'=({W}',{N}',{{{R}'}_{F}},{{{R}'}_{P}},{V}')$和$\mathfrak{M}$=(W, N, R_F, R_P, V), 如果$\mathfrak{M}$是由点w生成的, 即$\mathfrak{M}$=$\mathfrak{M}$_w, 并且Z: $\mathfrak{M}$', w' $\rightleftharpoons $M_w, w, 那么Z是满C2t-互模拟.

证明:设$\mathfrak{M}$=M_w并且Z: $\mathfrak{M}$', w' $\rightleftharpoons $M_w, w.再设v∈ $\mathfrak{M}$_w.那么存在自然数n, 使得w(R_F∪R_P)ⁿv.下面证明$\mathfrak{M}$'中存在某点和v, 有C2t-互模拟关系.对n进行归纳.n=0, 那么w=v.显然, 根据假设, w'和w有C2t-互模拟关系.假设w(R_F∪R_P)ⁿ⁺¹v.那么存在w₀∈ $\mathfrak{M}$_w, 使得w(R_F∪R_P)ⁿw₀并且w₀(R_F∪R_P)ⁿv.根据归纳假设, 存在${{{w}'}_{0}}\in {\mathfrak{M}}'$, 使得${{{w}'}_{0}}\leftrightharpoons {{w}_{0}}$.又因为w₀(R_F∪R_P)ⁿv, 所以w₀R_Fv或者w₀R_Pv.分两种情况讨论:第1种情况, w₀R_Fv, 那么根据C2t-互模拟的定义, 存在v'∈ $\mathfrak{M}$', 使得${{{w}'}_{0}}{{{R}'}_{F}}{v}'$并且v' $\rightleftharpoons $v; 第2种情况, w₀R_Pv, 同理, 存在v"∈ $\mathfrak{M}$', 使得${{{w}'}_{0}}{{{R}'}_{F}}{v}''$并且v" $\rightleftharpoons $v.因此, 在两种情况下, v和$\mathfrak{M}$'中的点都存在C2t-互模拟关系, 所以Z是一个满C2t-互模拟.

定理1.正则模型类是时态可定义的当且仅当它在不相交并、满C2t-互模拟以及C2t-超滤扩张下封闭, 并且它的补类也在C2t-超滤扩张下封闭.

证明:

●从左到右方向:由命题2、命题4、命题14可得.

●从右到左方向:

设正则模型类$\mathbb{K}$在不相交并、满C2t-互模拟像、C2t-超滤扩张下封闭, 并且$\mathbb{K}$的补类在C2t-超滤扩张下封闭.定义${{\mathit{\boldsymbol{ \boldsymbol{\varTheta} }} }_{\mathbb{K}}}=\{\phi |\mathbb{K}\vDash \phi \}.$下面证明${{\mathit{\boldsymbol{ \boldsymbol{\varTheta} }} }_{\mathbb{K}}}$定义$\mathbb{K}$, 即对任意正则模型$\mathfrak{M}$, $\mathfrak{M}\vDash {{\mathit{\boldsymbol{ \boldsymbol{\varTheta} }} }_{\mathbb{K}}}$当且仅当$\mathfrak{M}$∈ $\mathbb{K}$.

($\Leftarrow $) 直接根据定义可得.

(⇒) 假设$\mathfrak{M}\vDash {{\mathit{\boldsymbol{ \boldsymbol{\varTheta} }} }_{\mathbb{K}}}\text{,}$下面分情况考虑:

第1种情况: $\mathfrak{M}$是时态饱和的并且$\mathfrak{M}$是点生成模型.不妨设$\mathfrak{M}$=$\mathfrak{M}$_w, 其中, w是$\mathfrak{M}$的点.令Σ={σ| $\mathfrak{M}$, w╞σ}.下面证$\mathbb{K}$中存在一个时态饱和模型满足Σ.

易证:对任意公式σ∈Σ, 存在正则模型N_σ∈ $\mathbb{K}$满足σ.因为假设不然, 那么存在公式σ₀∈Σ, $\mathbb{K}$所有模型都不满足σ₀.所以, ¬σ₀在$\mathbb{K}$中所有模型上都是全局真的.所以$\neg {{\sigma }_{0}}\in {{\mathit{\boldsymbol{ \boldsymbol{\varTheta} }} }_{\mathbb{K}}}\text{.}$根据假设, $\mathfrak{M}$, w $\vDash $σ₀.这与σ₀∈Σ矛盾.

定义$\mathfrak{N}={{\uplus }_{\sigma \in \Sigma }}{{\mathfrak{N}}_{\sigma }}=({W}',{N}',{{{R}'}_{F}},{{{R}'}_{P}},{V}')$.因为对任意σ∈Σ, N_σ∈ $\mathbb{K}$并且$\mathbb{K}$在不相交并下封闭, 所以N∈ $\mathbb{K}$.

令U(σ)={v∈W'|N, v╞σ}.定义集合E⊆P(W') 为E={U(s)|σ∈Σ}.容易验证, E不包含空集并且在集合交运算下封闭.所以, E有有穷交性质.所以存在W'上超滤子v', 满足E⊆v'.所以对任意σ∈Σ, U(s)∈v'.根据命题11, $\mathfrak{ueN}$, v'╞Σ.根据命题15, $\mathfrak{ueN}$是时态饱和的.又因N∈ $\mathbb{K}$并且$\mathbb{K}$在C2t-超滤扩张下封闭, 所以$\mathfrak{ueN}$∈ $\mathbb{K}$.

因此, $\mathbb{K}$中存在一个时态饱和模型 (也就是$\mathfrak{ueN}$), 使得Σ在该饱和模型上可满足 (即在点v'可满足).所以, w(在$\mathfrak{M}$中) 和v'(在$\mathfrak{ueN}$中) 是时态等价的.由于$\mathfrak{M}$和$\mathfrak{ueN}$是时态饱和的, 根据命题6, 存在C2t-互模拟Z: $\mathfrak{ueN}$, v' $\rightleftharpoons \mathfrak{M}$, w.由于$\mathfrak{M}$=$\mathfrak{M}$_w是由点w生成的, 根据引理1可得, Z是一个满C2t-互模拟.又因为$\mathbb{K}$在满C2t-互模拟下封闭, 所以$\mathfrak{M}$∈ $\mathbb{K}$.

第2种情况: $\mathfrak{M}$是时态饱和的.为了叙述方便, 令$\mathfrak{M}$=(W, N, R_F, R_P, V).那么对任意w₀∈W, ${{\mathfrak{M}}_{{{w}_{0}}}}\models $${\mathit{\boldsymbol{ \boldsymbol{\varTheta} }} }_{\mathbb{K}}$容易验证:对任意w₀∈W, ${{\mathfrak{M}}_{{{w}_{0}}}}$是时态饱和的.根据第1种情况的证明可得:对任意w₀∈W, ${{\mathfrak{M}}_{{{w}_{0}}}}\in \mathbb{K}\text{.}$由于$\mathbb{K}$在不相交并下封闭, 所以${{\uplus }_{{{w}_{0}}\in W}}{{\mathfrak{M}}_{{{w}_{0}}}}\in \mathbb{K}\text{.}$根据命题5(2), ${{\uplus }_{{{w}_{0}}\in W}}{{\mathfrak{M}}_{{{w}_{0}}}}$与$\mathfrak{M}$之间存在满C2t-互模拟.又因为$\mathbb{K}$在满C2t-互模拟下封闭, 所以$\mathfrak{M}$∈ $\mathbb{K}$.

第3种情况: $\mathfrak{M}$是任意正则模型.根据命题13, $\mathfrak{u}\mathfrak{e}\mathfrak{M}\vDash {{\mathit{\boldsymbol{ \boldsymbol{\varTheta} }} }_{\mathbb{K}}}$.因为$\mathfrak{ueM}$是时态饱和的, 所以根据第2种情况的证明可得, $\mathfrak{ueM}$∈ $\mathbb{K}$.又因为$\mathbb{K}$及其补类在C2t-超滤扩张下封闭, 所以$\mathfrak{M}$∈ $\mathbb{K}$.

6 结论

本文证明了正则模型类在时态语言中可定义性的刻画定理.它是对克里普克模型类在模态语言中的可定义性刻画定理的推广.每个时态公式都定义一个正则模型类, 但是并非每个正则模型类都能在时态语言中定义.例如, 所有有穷的正则模型类在时态语言中不可定义, 因为这个模型类对不相交并不是封闭的.本文证明的定理对于时态逻辑在计算机科学中的应用具有潜在的价值, 运用这个定理, 可以检验给定的正则模型类或正则模型性质是否能够在时态语言中表达.