What question did this study set out to answer?

The study aims to propose a direct cut-elimination procedure for various sequent calculi, including classical and modal logics.

April 1, 2026Open Access

Topdown Cut-Elimination

Key Points

The study aims to propose a direct cut-elimination procedure for various sequent calculi, including classical and modal logics.
Proposes a direct cut-elimination procedure without the mix rule.
Demonstrates the method on the hyper sequent calculus.
Applies findings to classical, intuitionistic, and standard modal logics.
Successfully establishes the cut-elimination theorem for the hyper sequent calculus of modal logic S5.
Demonstrates efficacy across different logical frameworks.

Abstract

A direct cut-elimination procedure is proposed, which works for the sequent calculi not only of the classical and the intuitionistic logics but also of the standard modal logics. In the procedure, we do not introduce the inference rule mix but eliminate the usual rule cut directly. We demonstrate the method to establish the cut-elimination theorem for the hyper sequent calculus for the modal logic S5.

Bookmark

View Full Paper

Cite This Study

串田裕彦 (Fri,) studied this question.

synapsesocial.com/papers/69cd7b155652765b073a8d5d https://doi.org/https://doi.org/10.15053/0002000081