- This event has passed.
Semantical considerations on cut elimination and analytic cut property
June 19 @ 1:00 pm - 3:30 pm
Speaker: Hiroakira Ono (Japan Advanced Institute of Science and Technology)
Cut elimination is a powerful tool of proof-theory, but sometimes we are faced with difficulties of finding a natural cut-free sequent systems even for standard logics, e.g. modal logic S5 and bi-intuitionistic logic. On the other hand, we can still find sequent systems for them with analytic cut property i.e., every sequent provable in the system has a proof in which every cut formula is a subformula of the lower sequent of cut rule. In such a case, the subformula property holds in them, and hence many useful logical property like Craig’s interpolation property can be derived.
In my talk, first we introduce a (frame) semantical framework for showing cut elimination and analytic cut property, following the idea by M. Takano. The method can be applied also for proving cut elimination of sequent systems for intuitionistic and modal predicate logics. Next, we try to establish a link of this semantical approach with existing algebraic approach to cut elimination, using quasi-embeddings of Gentzen structures into quasi-completions (by F. Belardinelli, P. Jipsen and HO, and also A. Ciabattoni, N. Galatos and K. Terui). This can be done by introducing the notion of semi-completeness of sequent systems, which came out of S. Maehara's paper of 1991. Thus, we can have a unified understanding of these two semantical approaches.