分次模态语言的模型论 阿里云 lit azw3 txt pdf caj 下载 在线

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

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

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

总序

前言

导论

第1章 计数模态语言

1.1 模态逻辑的语义视角

1.2 计数模态语言

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

1.4 分次模态逻辑

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

2.1 模型和框架构造

2.2 分次超滤扩张与饱和

2.3 模型和框架可定义性

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

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

第3章 分次模态余代数

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

3.2 分次模态代数

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

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

3.5 ***L的泛余代数

第4章 公理系统和完全性

4.1 分次正规模态逻辑

4.2 典范余代数模型

4.3 一些完全的逻辑

4.4 代数完全性与典范性

4.5 ***L的嵌入定理

第5章 余代数对应理论

5.1 弱二阶逻辑与翻译

5.2 无变元公式与统一公式

5.3 分次萨奎斯特对应定理

5.4 非分次萨奎斯特公式

5.5 萨奎斯特完全性定理

第6章 有限模型性质

6.1 过滤模型

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

6.3 Kg43的典范公式

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

第7章 公式的分类

7.1 Ω模拟与正存在公式

7.2 点Ω子模型保持

7.3 ***L的Chang-Los-Suszko定理

7.4 保序与正公式

7.5 子框架保持

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

8.1 分次全通模态词

8.2 分次异点算子

8.3 无限基数的模态逻辑

8.4 ***L的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>