Sequent Systems for Modal Logics

Sequent Systems for Modal Logics
复制标题

模态逻辑的顺序系统

DOI:
--
复制
发表时间:
2002
期刊:
影响因子:
--
通讯作者:
H. Wansing
H. Wansing
中科院分区:
--
文献类型:
--
作者:
H. Wansing

文献摘要

被引文献

相似文献

本章概述了各种顺序系统在模态和时序逻辑(也称为时态逻辑)中的应用。出发点是普通的根岑序列及其在技术和哲学上的局限性。本章的其余部分致力于对顺序的普通概念进行概括。这些考虑仅限于没有明确使用可能世界或真值等语义参数的形式主义,从而排除了例如 Gabbay 的标记演绎系统、索引表格演算和 Kanger 式证明系统等。对这些类型的证明系统感兴趣的读者可以参考 [Gabbay, 1996]、[Gore, 1999] 和 [Pliuskeviene, 1998]。还有 Orlowska 的 [1988; 1996] 本章不考虑正态模态逻辑的 Rasiowa-Sikorski 式关系证明系统。在关系证明系统中,逻辑对象语言与关系术语的语言相关联。这些术语可能包含表示可能世界模型中的可访问性关系的子术语,以便语义信息与句法信息在同一级别上可用。关系证明系统中的推导规则操纵由关系项和关系运算构造的关系公式的有限序列。 [Ono, 1998] 中给出了非经典逻辑的普通顺序系统的概述,有关证明论的一般背景,读者可以参考 [Troelstra 和 Schwichtenberg, 2000]。
This chapter surveys the application of various kinds of sequent systems to modal and temporal logic, also called tense logic. The starting point are ordinary Gentzen sequents and their limitations both technically and philosophically. The rest of the chapter is devoted to generalizations of the ordinary notion of sequent. These considerations are restricted to formalisms that do not make explicit use of semantic parameters like possible worlds or truth values, thereby excluding, for instance, Gabbay’s labelled deductive systems, indexed tableau calculi, and Kanger-style proof systems from being dealt with. Readers interested in these types of proof systems are referred to [Gabbay, 1996], [Gore, 1999] and [Pliuskeviene, 1998]. Also Orlowska’s [1988; 1996] Rasiowa-Sikorski-style relational proof systems for normal modal logics will not be considered in the present chapter. In relational proof systems the logical object language is associated with a language of relational terms. These terms may contain subterms representing the accessibility relation in possible-worlds models, so that semantic information is available at the same level as syntactic information. The derivation rules in relational proof systems manipulate finite sequences of relational formulas constructed from relational terms and relational operations. An overview of ordinary sequent systems for non-classical logics is given in [Ono, 1998], and for a general background on proof theory the reader may consult [Troelstra and Schwichtenberg, 2000].