第1 章计数模态语言
本章是计数模态语言的简要引论。1.1 节首先讨论研究动机。然后在1.2 节正式引入计数模态语言及其关系语义学。1.3 节引入一些基本模型构造方法并证明相应的保持结果，第2 章会使用这些结果。1.4 节集中考虑一种特殊的计数模态语言，即分次模态语言，主要目的是对目前已有的模型论方面的结果进行概述。
1.1 模态逻辑的语义视角
自20 世纪60 年代以来，逻辑学家们认识到，在关系语义学中解释的模态算子，只不过是没有明确约束个体变元的“局部”量词。“局部”这个词的意思是，作为量词的模态词算子仅以所有可及状态为量化域。因此，从语义角度看，基本模态逻辑与一阶逻辑FOL 并非如此不同，因为两者都能用来谈论关系结构的性质。另一方面，一阶逻辑与模态逻辑也存在重要差异，就表达力而言，前者要远远强于后者。在模型层次上，模态逻辑是FO2 的一个片段，这里FO2 是一阶逻辑带两变元的片段。更确切地说，根据范本特姆J. van Benthem刻画定理，模态逻辑是一阶逻辑或FO2，因为模态逻辑可以嵌入FO2的互模拟不变片段。然而，模态逻辑有一些非常好的逻辑性质和计算性质，比如可判定性和低程度的计算复杂性，而一阶逻辑不具有这些性质。因此，如果我们想获得表达力更强的模态语言，但是又保持基本模态逻辑的优良性质，一种方法就是通过增加新模态词对基本模态逻辑进行扩张，这些新模态词在基本模态逻辑中是不能定义的。逻辑学家们一直在探索这个研究方向。
本书采取的研究思路如下：从与语义视角相反的角度看，任给量词Q，都可以抽象出一元模态词.Q，它是关系结构上的一个局部量词。这条从量词到模态词的道路也可以在斐尼的论文Fine, 1972a中找到，该文引入了数字量词的模态对应算子。一个带数字量词的一阶公式的形式是.nxαx，它在一个一阶模型中是真的当且仅当至少存在n 个个体满足αxTarski, 1941。显然这些量词在带等词的一阶逻辑中是可定义的，但是在不带等词的纯一阶逻辑中是不可定义的。一阶公式.nxαx的模态对应公式可以写作.nα，它在一个关系模型中状态w 上是真的当且仅当w 至少有n 个可及状态满足α。
更一般地，由于有限多个无限多个和可数多个不可数多个这样的概念常常在数学中使用，它们在一阶逻辑中是不可定义的，因此可以引入新的量词来丰富一阶逻辑，从而使这些概念得以表达。莫斯托夫斯基Mostowski, 1957提出的广义量词理论，开启了通向一阶逻辑扩张的模型论之门。任给无限基数κ，新语言FOLQκ从FOL 增加新量词Qκ得到。如下解释形如Qκxαx的新公式：
M Qκxαx当且仅当存在κ个元素b 属于M 使得M αx[b]。令αx1, ..., xnM = {a1, ..., an : M αx1, ..., xn[a1, ..., an]}。那么M Qκx αx 当且仅当| αx1, ..., xnM | ≥κ。例如，在语言FOLQ0中，可以表达“存在可数多个”这个概念。在这些基数逻辑中，一个重要结果是“存在不可数多个”这个量词的逻辑可以使用一束相当简单的公式来公理化，这些公理是凯斯勒Keisler, 1970给出的。对这些基数量词来说，通过推广斐尼Fine, 1972a的方法，也可以抽象出对应的基数模态词。
现在正式引入基数模态词。令M = W, R, V是关系模型，w ∈W 并且w ↑ = {v ∈W : Rwv}。对任何公式φ，令φM 是φ在M 中的真集。对每个自然数n 0，定义模态词.n 如下：
M, w .nφ当且仅当| w ↑∩φM | ≥ n。公式.nφ的意义是至少存在n 个后继状态使φ真。同样，可以把数字模态词推广到任意基数模态词。对每个基数κ，定义模态词.κ如下：
M, w .κφ当且仅当| w ↑∩φM | ≥ κ。考虑在基本模态逻辑基础上增加基数模态词的扩张。在有限基数的情况下，增加所有.nn 0 而获得的扩张仍然是带等词一阶逻辑的片段。然而，在无限基数的情况下，所获得的模态语言比一阶逻辑的表达能力更强。本书所要研究的主要内容就是有限基数的模态逻辑。在1.4 节，笔者将概述目前文献中所得到的关于分次模态逻辑的模型论结果。下面首先以形式的方式定义计数模态语言、关系语义以及相关的句法和语义概念。
1.2 计数模态语言
基数可用于计算一阶结构中具有特定性质的个体的数目，在关系结构中，它们也可以用来计算具有特定性质的可及状态的数目。本节以形式的方式定义计数模态语言及其关系语义学，还包括一些有用的基本概念。
定义1.1 给定有限的或无限的基数κ 0，计数模态语言MLκ, ω由
模态相似型τκ = {.λ : λ κ}和命题字母集Φ组成。所有MLκ, ω公式的集合Formκ, ω由如下归纳规则给出：
φ ::= p | ⊥ | φ1 →φ2| .λφ,
其中p ∈Φ并且.λ∈τκ。其他联结词，.，∧和∨如命题逻辑中定义。定义对偶算子λφ:= ..λ.φ以及缩写.!λφ:= .λφ∧..+φ，其中λ+是大于λ 的最小基数，即λ 的后继基数。在一些地方也使用无穷的基λ数模态语言MLκ, ∞，它允许对任意公式集合取和析取。
下面定义一些句法概念。对任何计数模态公式φ，定义varφ = {p : p 是在φ中出现的命题字母}。也可以写φp1, ..., pn，如果varφ . {p1, ..., pn}。称φ为无变元MLκ, ω公式，如果varφ = .。还可以令Sfφ = {ψ : ψ是φ的子公式}。子公式的概念容易归纳定义。此外，还定义两个句法概念。
定义1.2 所有MLκ, ω公式φ的模态度mdφ递归定义如下：
1 mdp = md⊥ = 0。
2 mdφ1 →φ2 = max{mdφ1, mdφ2}。
3 md.λφ = mdφ + 1。
定义1.3 任何MLκ, ω公式φ的等级定义为gdφ = max{λ : .λψ∈Sfφ}。
下面定义计数模态语言的关系语义。研究的本体是所有只带一个二元关系的关系结构框架组成的类。用Frm 表示所有框架组成的类。所有MLκ, ω公式都如1.1 节说明的那样在关系结构中进行解释。引入MLκ, ω的关系语义的代数形式。令F = W, R是框架。前面已经引入记号w ↑，它代表F 中状态w 的所有R 后继状态的集合，有时也记为Rw。还可以定义
w ↓ = {v ∈W : Rvw},
即w 的所有前驱状态的集合。这两种运算可扩张到状态集。对集合X .W，如下定义：
X ↑ = {w ∈W : X ∩w ↑≠.} 和X ↓ = {w ∈W : X ∩w ↓≠.}。
此外，在幂集.W上可以定义补运算.X := W \ X。还可以定义模态运算
.λ.X = {w ∈W : | w ↑∩X | ≥ λ}。
同样，算子.λ.的对偶算子定义为[λ]X := ..λ..X。与句法复合算子.!一样，可以引入记号.λ.!X := .λ.X ∩..λ+.X。这些运算在下面定义模型中公式的意义真集时起作用。
定义1.4 令M = W, R, V是模型。所有MLκ, ω公式φ在M 中的真集φM 递归定义如下：
pM = Vp, ⊥M = ., φ1 →φ2M = .φ1M ∪φ2M, .λφM = .λ.φM。
计算可得，λφM = [λ]φM 和.!λφM = .λ.!φM。
满足关系可以定义为：M, w φ当且仅当w ∈φM。称φ在M 中可满足，如果M 中存在状态w 使得M, w φ。对于M 中任何状态子集X，写M, X φ，如果对所有x ∈X 都有M, x φ。称φ在M 中是全局真的记为M φ，如果φM = W。称φ在点框架F, w中有效记为F, w φ，如果对F 中每个赋值V 都有F, V, w φ。称φ在框架F 中有效记为F φ，如果对F 中每个状态w 都有F, w φ。
例1.1 这里给出计数模态语言的一些例子。
1 计数模态语言ML1, ω只含模态词.0 和0。根据真之定义，容易验证公式.0φ逻辑等值于，而公式0φ逻辑等值于⊥。因此，ML1, ω这个语言等价于古典命题演算的语言。
2 很容易看到，基本模态算子.和分别可以定义为.1 和1。因此，基本模态语言恰恰等价于计数模态语言ML2, ω。
3 如果κ = ω，则得到语言MLω, ω，它的模态相似型是所有模态词
.nn ∈ω的集合。这恰好就是斐尼Fine, 1972a所引入的分次模态语言。另外，还要定义一些关于句法和语义之间相互联系的概念。在任何计数模态语言MLκ, ω中，给定框架类K，它的逻辑定义为LogK = {φ : φ是MLκ, ω公式并且对所有F ∈K 都有F φ}。反之，给定任何MLκ, ω公式集Σ，它定义这样一个框架类
FrmΣ = {F : 对所有φ∈Σ都有F φ}。由此，对每个计数模态语言MLκ, ω，存在下面两种运算：
1 Log . : .Frm →.Formκ, ω。
2 Frm . : .Formκ, ω →.Frm 。
容易验证如下关于这两种运算的事实。
事实1.1 令Σ和Γ是MLκ, ω公式集，并且K，C 是框架类。
1 如果Σ.Γ，那么FrmΓ .FrmΣ。
2 如果K .C，那么LogC .LogK。
3 Σ.LogFrmΣ并且K .FrmLogK。
4 LogFrmΣ = Σ当且仅当Σ = LogK对某个框架类K。
5 FrmLogK = K 当且仅当K = FrmΣ对某个公式集Σ。
称MLκ, ω公式集Σ定义框架类K，如果K = FrmΣ。称Σ定义模型类C，如果C = {M : 对所有φ∈Σ都有M φ}。同样的概念可扩展到点结构。称一个结构类在MLκ, ω中可定义，如果存在MLκ, ω公式集定义它。
1.3 构造模型和框架的基本方法
逻辑学家并非孤立地研究结构，而是要研究结构之间的相互联系，即如何从旧结构构造新结构。本节定义一些模型构造的方法或运算，在这些运算下，计数模态语言的公式的真是不变的，而且公式的有效性是保持的，这些运算包括：不相交并、生成子结构、树型展开、超积、计数有界态射和计数互模拟。
定义1.5 令{Mi = Wi, Ri, Vi : i ∈ I} 不相交的模型族，并且{Fi = Wi, Ri : i ∈I}是不相交的框架族。模型Mii ∈ I的不相交并定义为模型.I Mi =W, R, V，其中①W = ∪ i ∈I Wi ；②R = ∪ i ∈I Ri ；③Vp= ∪ i ∈I Vip对每个命题字母p。框架Fii ∈ I的不相交并定义为.I Fi = W, R。
不相交并使原来的结构在新的结构中成为“孤岛”，因此不改变后继状态的数目。这个事实蕴涵如下关于计数模态公式的不变性和保持结果。
命题1.1 令.I Mi 是模型Mii ∈ I的不相交并，而.I Fi 是框架Fi i ∈ I的不相交并。对每个MLκ, ω公式φ以及模型Mi 或框架Fi 中的状态w，
1 对所有i ∈I：.I Mi, w φ当且仅当Mi, w φ。
2 对所有i ∈I：.I Fi, w φ当且仅当Fi, w φ。
3 .I Mi φ当且仅当对所有i ∈I 都有Mi φ。
4 .I Fi φ当且仅当对所有i ∈I 都有Fi φ。证明 容易对φ归纳证明1，其他几项通过类似于基本模态逻辑的论证得到Blackburn et al., 2001。■
定义1.6 令M = W, R, V 和M′ = W ′, R ′, V ′是模型，而F = W, R 和F′ = W ′, R ′是框架。模型M 称为M′的子模型记为M .M′，如果
1 W .W ′。
2 R = R ′∩ W ×W。
3 对每个命题字母p，Vp = V ′p ∩W。
模型M 称为M′的生成子模型记为M M′，如果M .M′并且对每个状态w ∈W 都有R ′wu 蕴涵u ∈W。
任给非空子集X .W ′，M 称为M′从X 生成的子模型，如果M .M′并且W = ∪i ωWi .W ′，其中W0 = X 并且Wn+1 = Wn↑。称M 是M′的点生成子模型，如果存在状态w ∈W ′使得M 是M′从{w}生成的子模型。对框架来说，去掉赋值条件便可定义如上概念。
与不相交并一样，生成过程也不改变当前状态所有可及状态的数目，因为生成封闭条件保留原来结构中所有可及状态。由此可得如下不变性和保持结果。
命题1.2 令M M′并且F F′。对每个MLκ, ω公式φ以及模型M 或框架F 中的状态w，
1 M, w φ当且仅当M′, w φ。
2 如果M′φ，那么M φ。
3 F, w φ当且仅当F′, w φ。
4 如果F′φ，那么F φ。证明 对φ归纳证明1，其他各项容易得出。■下面引入树型展开。令F = W, R是框架并且w ∈W。定义SeqF, w为F
中从w 出发的所有非空有限状态序列。定义函数last : SeqF, w →W 使得对每个序列s = w0, ..., wn ∈ SeqF, w，lasts = wn，即序列s 的最后一个分量。一个框架F 或模型M 称为有根的，如果存在一个状态w 使得其他每个状态都是可以从w 在有限步之内可及的。
定义1.7 令M = W, R, V 是有根模型，F =W, R是有根框架，w ∈W 是根状态。定义M 从状态w 的树型展开是模型unrM[w] = W *, R *, V *，其中
1 W * = SeqF, w。
2 R * = {s, su : u ∈W & lastsRu}。
3 V *p = {s : lasts ∈ Vp}。框架F 从w 的树型展开定义为unrF[w] = W *, R *。显而易见，树型展开不会改变可及状态的数目，因为没有任何状态会在展开
过程中被切除。因此，也有如下关于树型展开的不变性和保持结果。命题1.3 令unrM[w]和unrF[w]是从w 的树型展开结构。对每个MLκ, ω 公式φ和序列s ∈SeqF, w，
1 unrM[w], s φ当且仅当M, lasts φ。
2 M φ当且仅当unrM[w] φ。
3 如果unrF[w], s φ，那么F, lasts φ。
4 如果unrF[w] φ，那么F φ。
|
購物車/收銀台(
0
) | 在線留言板
| 付款方式
| 運費計算
| 聯絡我們
| 幫助中心 |
加入書簽
HOME
新書上架
