We present a detailed proof of the admissibility of cut in sequent calculus for some congruent modal logics. The result was announced much earlier during the Trends in Logic Conference, ToruĊ 2006 and the proof for monotonic modal logics was provided already in Indrzejczak [5]. Also some tableau and natural deduction formalizations presented in Indrzejczak [6] and Indrzejczak [7] were based on this result but the proof itself was not published so far. In this paper we are going to fill this gap. The delay was partly due to the fact that the author from time to time was trying to improve the result and extend it to some additional logics by testing other methods of proving cut elimination. Unfortunately all these attempts failed and cut elimination holds only for these logics which were proved to satisfy this property already in 2005.
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.