Algebraic Aspects of Cut Elimination |
| |
| Authors: | Belardinelli Francesco Jipsen Peter Ono Hiroakira |
| |
| Affiliation: | (1) Classe di Lettere e Filosofia, Scuola Normale Superiore, P.zza dei Cavalieri, n° 7, 56126 Pisa, Italy;(2) Department of Mathematics, CS, Physics, Chapman University, Orange, CA 92866, USA;(3) School of Information Science, Japan Advanced Institute of Science and Technology, 1-1 Asahidai, Tatsunokuchi, Ishikawa, 923-1292, Japan |
| |
| Abstract: | We will give here a purely algebraic proof of the cut elimination theorem for various sequent systems. Our basic idea is to introduce mathematical structures, called Gentzen structures, for a given sequent system without cut, and then to show the completeness of the sequent system without cut with respect to the class of algebras for the sequent system with cut, by using the quasi-completion of these Gentzen structures. It is shown that the quasi-completion is a generalization of the MacNeille completion. Moreover, the finite model property is obtained for many cases, by modifying our completeness proof. This is an algebraic presentation of the proof of the finite model property discussed by Lafont [12] and Okada-Terui [17]. |
| |
| Keywords: | Algebraic Gentzen systems cut elimination substructural logics residuated lattices finite model property |
| 本文献已被 SpringerLink 等数据库收录！ |
|
