Cut Elimination for GLS Using the Terminability of its Regress Process

被引：4

作者：

Brighton, Jude ^{[1
]}

机构：

[1] POB 26073, Toronto, ON M4P 0A8, Canada

来源：

JOURNAL OF PHILOSOPHICAL LOGIC | 2016年 / 45卷 / 02期

关键词：

Modal logic; GL; Gentzen-style logic; Cut-elimination; Regress trees; MODAL LOGIC; PROVABILITY;

D O I：

10.1007/s10992-015-9368-4

中图分类号：

B81 [逻辑学（论理学）];

学科分类号：

010104 ; 010105 ;

摘要：

The system GLS, which is a modal sequent calculus system for the provability logic GL, was introduced by G. Sambin and S. Valentini in Journal of Philosophical Logic, 11(3), 311-342, (1982), and in 12(4), 471-476, (1983), the second author presented a syntactic cut-elimination proof for GLS. In this paper, we will use regress trees (which are related to search trees) in order to present a simpler and more intuitive syntactic cut derivability proof for GLS(1), which is a (more connectively and inferentially economical) variant of GLS without the cut rule.

引用

页码：147 / 153

页数：7

共 9 条

[1]

[Anonymous], ADV MODAL LOGIC 08

[2]

[Anonymous], J NANZAN ACAD SOC MA

[3]

[Anonymous], 1967, Mathematical logic

[4]

[Anonymous], 2000, BASIC PROOF THEORY

[5]

Borga M., 1983, STUDIA LOGICA, V42, P453

[6]

Lb MH., 1955, J. Symb. Logic, V20, P115, DOI [DOI 10.2307/2266895, 10.2307/2266895]

[7] THE MODAL LOGIC OF PROVABILITY - THE SEQUENTIAL APPROACH [J].

SAMBIN, G ;

VALENTINI, S ;

MONTAGNA, F .

JOURNAL OF PHILOSOPHICAL LOGIC, 1982, 11 (03) :311-342

[8]

SOLOVAY RM, 1976, ISRAEL J MATH, V25, P287, DOI 10.1007/BF02757006

[9] THE MODAL LOGIC OF PROVABILITY, CUT-ELIMINATION [J].

VALENTINI, S .

JOURNAL OF PHILOSOPHICAL LOGIC, 1983, 12 (04) :471-476

← 1 →