模态对应理论

把模态命题看成为可达关系所应遵守的关系原则时的古典可定义性的系统研究。克里普克关系语义揭示了模态命题跟可达关系之间的联系，模态命题表达了对使之有效的克里普克标架中的可达关系所提的某种“古典”限制条件。例如，模态命题□pp在一个克里普克标架(W，R)中有效，当且仅当，可达关系R是自返的(即，对W中任一个ω有ωRω)。这也就是说，使模态命题□pp有效的克里普克标架，它的可达关系必须是自返的。克里普克标架上的赋值定义相当于把模态命题变成有关可达关系R的古典语句的一个转换，每一个模态命题都可以转换成某个二阶语句。例如，模态命题□(p∨q)(□p∨□q)被转换成

这里，P和Q都是一元谓词变项，分别相应于命题变项p和q。这些二阶语句中有的可以有等价的一阶语句，有的却并没有等价的一阶语句。例如，对应于模态命题□pp的二阶语句xP(y(RxyP(y))P(x))等价于一阶语句xRxx，但对应于模态命题□◇p◇□p的二阶语句却并不等价于任何一个一阶语句。因此要问，哪些模态命题定义了一阶关系条件?这问题就反映在一阶可定义性的概念中。称一个模态命题A为一阶可定义的，是指有一个用二元关系R和等词=表达的一阶语句α，使得A在一个克里普克标架中有效当且仅当此克里普克标架作为一阶结构使α有效。常见的一些模态公理，如□pp、□p□□p、◇□p□◇p和□(p∨q)□p∨□q等都是一阶可定义的。有关一阶可定义性的主要结果是在20世纪70年代得到的，可以利用古典逻辑模型论的概念陈述如下：一模态命题是一阶可定义的等价于它在初等等价下保持有效性。当然，我们也有相反方向的问题，也就是一阶语句的模态可定义性问题。称一个一阶语句α是模态可定义的，是指有一个模态命题跟它一样确定了同一个克里普克标架。有关这方面的主要结果也出现在70年代，涉及的模型论概念更多，我们陈述如下：一个一阶语句是模态可定义的，当且仅当，使它有效的全体克里普克标架对于生成子标架、不相交并和锯齿型同态象封闭，而不使它有效的全体克里普克标架对于超滤扩张封闭。对应理论的研究现在也被推广到了其它逻辑分支中，如时态逻辑、直觉主义逻辑等。