双模拟与模态逻辑

姚从军

(湖南科技学院思政部，湖南永州 425100)

双模拟与模态逻辑

姚从军

(湖南科技学院思政部，湖南永州 425100)

首先基于模型上的模拟概念定义了模型上的双模拟概念，并给出双模拟模态不变性和模态等价性的定义。在此基础上，讨论了模态逻辑与双模拟之间的关系;进一步分别在语言ML(τ，Φ)和ML∞(τ，Φ)中分析了模态等价性与双模拟不变性之间的关系;最后证明了正存在模态公式与双模拟之间的关系，并把正存在模态公式刻画为一阶公式双模拟不变部分。

模拟;双模拟;模态逻辑;正存在模态公式;双模拟不变性

一、基础知识

定义1.1 基本模态语言ML(◇，Φ)是由一个命题变项的集合Φ和一元模态算子◇组成的。其中Φ的元素通常被记作p，q，r等等。基本模态语言的合式公式φ由下面的规则给出

φ∷=p|⊥|﹁φ|φ∨ψ|◇φ，其中p∈Φ。

在BML中，如果将∨换为∨(允许无穷)得到无穷模态语言ML∞。

定义1.2 一个模态相似型是一个对τ=(0，ρ)，其中0是一个非空集，并且ρ是一个从0到N的函数，即ρ:0→N。0的元素被称为模态算子，我们用Δ，Δ1，Δ2，…表示0中的元素，函数ρ给每一个算子 Δ∈0指定一个自然数，表示 Δ的元数。

为了与定义1.1一致，我们把一元三角Δ1称作菱形，并且把它们记作或〈a〉，其中的a取自某个标号集。有时，我们假设算子的元数是已知的，因此，不区别τ和0。

定义1.3 一个模态语言ML(τ，Φ)是由一个模态相似型τ=(0，ρ)和一个命题变项的集合Φ构成的。τ和Φ上的模态公式的集合Form(τ，Φ)由下面的规则给出

φ∷=p|⊥|﹁φ|φ∨ψ|Δ(φ1，…，φρ(Δ)，其中p∈Φ。

同样，在ML(τ，Φ)中，如果将∨换为∨(允许无穷)得到无穷模态语言ML∞(τ，Φ)。

基本模态语言 ML(◇，Φ)是模态语言ML(τ，Φ)的一个特例，这里τ只包含一个一元模态词。……