Sequents vs Hypersequents for Åqvist Systems

Abstract Enhancing cut-free expressiveness through minimal structural additions to sequent calculus is a natural step. We focus on Åqvist’s system $$\textbf{F}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>F</mml:mi> </mml:math> with cautious monotonicity ( CM ), a deontic logic extension of $$\textbf{S5}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>S</mml:mi> <mml:mn>5</mml:mn> </mml:mrow> </mml:math> , for which we define a sequent calculus employing (semi) analytic cuts.The transition to hypersequents is key to develop modular and cut-free calculi for $$\mathbf{F + (CM)}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>F</mml:mi> <mml:mo>+</mml:mo> <mml:mo>(</mml:mo> <mml:mi>CM</mml:mi> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> and $$\textbf{G}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>G</mml:mi> </mml:math> , also supporting countermodel construction.