分次模态语言的模型论 epub 下载 pdf 网盘 2025 mobi 在线 免费

分次模态逻辑是有限基数的模态逻辑。

分次模态语言的模型论给出了分次模态逻辑的余代数语义，研究余代数结构类在分次模态语言中的可定义性问题；证明了几条可定义性定理，使用余代数典范模型证明正规分次模态逻辑模态逻辑的完全性；探讨了余代数语义下分次模态逻辑与弱二阶逻辑的对应理论，以及分次模态公式的分类和几个扩张表达力的语言。此外，在关系语义学下，分次模态语言的模型论还给出了结构类的可定义性定理。

分次模态语言的模型论适合现代逻辑专业、数学专业以及计算机领域的研究人员和高校师生参考阅读。

总序

前言

导论

第1章 计数模态语言

1.1 模态逻辑的语义视角

1.2 计数模态语言

1.3 构造模型和框架的基本方法

1.4 分次模态逻辑

第2章 分次模态语言的关系语义学

2.1 模型和框架构造

2.2 分次超滤扩张与饱和

2.3 模型和框架可定义性

2.4 范本特姆-罗森刻画定理

2.5 GML和FOL(C)之间的框架对应

第3章 分次模态余代数

3.1 分次模态语言的余代数语义

3.2 分次模态代数

3.3 分次模态代数与余代数之间的对偶

3.4 有限余代数和余代数模型的可定义性

3.5 GML的泛余代数

第4章 公理系统和完全性

4.1 分次正规模态逻辑

4.2 典范余代数模型

4.3 一些完全的逻辑

4.4 代数完全性与典范性

4.5 GML的嵌入定理

第5章 余代数对应理论

5.1 弱二阶逻辑与翻译

5.2 无变元公式与统一公式

5.3 分次萨奎斯特对应定理

5.4 非分次萨奎斯特公式

5.5 萨奎斯特完全性定理

第6章 有限模型性质

6.1 过滤模型

6.2 NExt(Kg42)中子余代数逻辑

6.3 Kg43的典范公式

6.4 正规分次模态格NExt(KgAltn)

第7章 公式的分类

7.1 Ω模拟与正存在公式

7.2 点Ω子模型保持

7.3 GML的Chang-Los-Suszko定理

7.4 保序与正公式

7.5 子框架保持

第8章 分次模态逻辑的扩张

8.1 分次全通模态词

8.2 分次异点算子

8.3 无限基数的模态逻辑

8.4 GML的Lindstr?m定理

参考文献

附录A 模型论与泛代数

附录B 基本模态逻辑

附录C 余代数理论

后记

暂无相关内容，正在全力查找中

暂无出版社相关信息，正在全力查找中！

第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 个个体满足α(x)(Tarski, 1941)。显然这些量词在带等词的一阶逻辑中是可定义的，但是在不带等词的纯一阶逻辑中是不可定义的。一阶公式.nxα(x)的模态对应公式可以写作.nα，它在一个关系模型中状态w 上是真的当且仅当w 至少有n 个可及状态满足α。

更一般地，由于有限多个(无限多个)和可数多个(不可数多个)这样的概念常常在数学中使用，它们在一阶逻辑中是不可定义的，因此可以引入新的量词来丰富一阶逻辑，从而使这些概念得以表达。莫斯托夫斯基(Mostowski, 1957)提出的广义量词理论，开启了通向一阶逻辑扩张的模型论之门。任给无限基数κ，新语言FOL(Qκ)从FOL 增加新量词Qκ得到。如下解释形如Qκxα(x)的新公式：

M Qκxα(x)当且仅当存在κ个元素b 属于M 使得M α(x)[b]。令α(x1, ..., xn)M = {(a1, ..., an) : M α(x1, ..., xn)[a1, ..., an]}。那么M Qκx α(x) 当且仅当| α(x1, ..., xn)M | ≥κ。例如，在语言FOL(Q0)中，可以表达“存在可数多个”这个概念。在这些基数逻辑中，一个重要结果是“存在不可数多个”这个量词的逻辑可以使用一束相当简单的公式来公理化，这些公理是凯斯勒(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 | ≥ κ。考虑在基本模态逻辑基础上增加基数模态词的扩张。在有限基数的情况下，增加所有.n(n > 0) 而获得的扩张仍然是带等词一阶逻辑的片段。然而，在无限基数的情况下，所获得的模态语言比一阶逻辑的表达能力更强。本书所要研究的主要内容就是有限基数的模态逻辑。在1.4 节，笔者将概述目前文献中所得到的关于分次模态逻辑的模型论结果。下面首先以形式的方式定义计数模态语言、关系语义以及相关的句法和语义概念。

1.2 计数模态语言

基数可用于计算一阶结构中具有特定性质的个体的数目，在关系结构中，它们也可以用来计算具有特定性质的可及状态的数目。本节以形式的方式定义计数模态语言及其关系语义学，还包括一些有用的基本概念。

定义1.1 给定(有限的或无限的)基数κ > 0，计数模态语言ML(κ, ω)由

模态相似型τκ = {.λ : λ φ ::= p | ⊥ | φ1 →φ2| .λφ,

其中p ∈Φ并且.λ∈τκ。其他联结词，.，∧和∨如命题逻辑中定义。定义对偶算子λφ:= ..λ.φ以及缩写.!λφ:= .λφ∧..+φ，其中λ+是大于λ 的最小基数，即λ 的后继基数。在一些地方也使用无穷的基λ数模态语言ML(κ, ∞)，它允许对任意公式集合取和析取。

下面定义一些句法概念。对任何计数模态公式φ，定义var(φ) = {p : p 是在φ中出现的命题字母}。也可以写φ(p1, ..., pn)，如果var(φ) . {p1, ..., pn}。称φ为无变元ML(κ, ω)公式，如果var(φ) = .。还可以令Sf(φ) = {ψ : ψ是φ的子公式}。子公式的概念容易归纳定义。此外，还定义两个句法概念。

定义1.2 所有ML(κ, ω)公式φ的模态度md(φ)递归定义如下：

(1) md(p) = 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 后继状态的集合，有时也记为R(w)。还可以定义

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 = V(p), ⊥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) 计数模态语言ML(1, ω)只含模态词.0 和0。根据真之定义，容易验证公式.0φ逻辑等值于，而公式0φ逻辑等值于⊥。因此，ML(1, ω)这个语言等价于古典命题演算的语言。

(2) 很容易看到，基本模态算子.和分别可以定义为.1 和1。因此，基本模态语言恰恰等价于计数模态语言ML(2, ω)。

(3) 如果κ = ω，则得到语言ML(ω, ω)，它的模态相似型是所有模态词

.n(n ∈ω)的集合。这恰好就是斐尼(Fine, 1972a)所引入的分次模态语言。另外，还要定义一些关于句法和语义之间相互联系的概念。在任何计数模态语言ML(κ, ω)中，给定框架类K，它的逻辑定义为Log(K) = {φ : φ是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，那么Log(C) .Log(K)。

(3) Σ.Log(Frm(Σ))并且K .Frm(Log(K))。

(4) Log(Frm(Σ)) = Σ当且仅当Σ = Log(K)对某个框架类K。

(5) Frm(Log(K)) = 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}是(不相交的)框架族。模型Mi(i ∈ I)的不相交并定义为模型.I Mi =(W, R, V)，其中①W = ∪ i ∈I Wi ；②R = ∪ i ∈I Ri ；③V(p)= ∪ i ∈I Vi(p)对每个命题字母p。框架Fi(i ∈ I)的不相交并定义为.I Fi = (W, R)。

不相交并使原来的结构在新的结构中成为“孤岛”，因此不改变后继状态的数目。这个事实蕴涵如下关于计数模态公式的不变性和保持结果。

命题1.1 令.I Mi 是模型Mi(i ∈ 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，V(p) = V ′(p) ∩W。

模型M 称为M′的生成子模型(记为M M′)，如果M .M′并且对每个状态w ∈W 都有R ′wu 蕴涵u ∈W。

任给非空子集X .W ′，M 称为M′从X 生成的子模型，如果M .M′并且W = ∪i 与不相交并一样，生成过程也不改变当前状态所有可及状态的数目，因为生成封闭条件保留原来结构中所有可及状态。由此可得如下不变性和保持结果。

命题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。定义Seq(F, w)为F

中从w 出发的所有非空有限状态序列。定义函数last : Seq(F, w) →W 使得对每个序列s = (w0, ..., wn) ∈ Seq(F, w)，last(s) = 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 * = Seq(F, w)。

(2) R * = {(s, su) : u ∈W & last(s)Ru}。

(3) V *(p) = {s : last(s) ∈ V(p)}。框架F 从w 的树型展开定义为unrF[w] = (W *, R *)。显而易见，树型展开不会改变可及状态的数目，因为没有任何状态会在展开

过程中被切除。因此，也有如下关于树型展开的不变性和保持结果。命题1.3 令unrM[w]和unrF[w]是从w 的树型展开结构。对每个ML(κ, ω) 公式φ和序列s ∈Seq(F, w)，

(1) unrM[w], s φ当且仅当M, last(s) φ。

(2) M φ当且仅当unrM[w] φ。

(3) 如果unrF[w], s φ，那么F, last(s) φ。

(4) 如果unrF[w] φ，那么F φ。

在线阅读地址：分次模态语言的模型论在线阅读

在线听书地址：分次模态语言的模型论在线收听

在线购买地址：分次模态语言的模型论在线购买

暂无原文赏析，正在全力查找中！

编辑推荐

div>