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, 311–342,, and in 12, 471–476,, the second author presented a syntactic cut-elimination proof for GLS. In this paper, we will use regress trees in order to present a simpler and more intuitive syntactic cut derivability proof for GLS1, which is a variant of GLS without the cut rule.

In the paper a decision procedure for S5 is presented which uses a cut-free sequent calculus with additional rules allowing a reduction to normal modal forms. It utilizes the fact that in S5 every formula is equivalent to some 1-degree formula, i.e. a modally-flat formula with modal functors having only boolean formulas in its scope. In contrast to many sequent calculi for S5 the presented system does not introduce any extra devices. Thus it is a standard version of SC but (...) with some additional simple rewrite rules. The procedure combines the proces of saturation of sequents with reduction of their elements to some normal modal form. (shrink)

A well established technique toward developing the proof theory of a Hilbert-style modal logic is to introduce a Gentzen-style equivalent (a Gentzenisation), then develop the proof theory of the latter, and finally transfer the metatheoretical results to the original logic (e.g., [1, 6, 8, 18, 10, 12]). In the first-order modal case, on one hand we know that the Gentzenisation of the straightforward first-order extension of GL, the logic QGL, admits no cut elimination (if the rule is included as primitive; (...) or, if not included, then the rule is not admissible [1]). On the other hand the (cut-free) Gentzenisations of the first-order modal logics M3 and ML3 of [10, 12] do have cut as an admissible rule. The syntactic cut admissibility proof given in [18] for the Gentzenisation of the propositional provability logic GL is extremely complex, and it was the basis of the proofs of cut admissibility of the Gentzenisations of M3 and ML3, where the presence of quantifiers and quantifier rules added to the complexity and length of the proof. A recent proof of cut admissibility in a cut-free Gentzenisation of GL is given in [5] and is quite short and easy to read. We adapt it here to revisit the proofs for the cases of M3 and ML3, resulting to similarly short and easy to read proofs, only slightly complicated by the presence of quantification and its relevant rules. (shrink)