A LABELLED SEQUENT CALCULUS FOR HALF-ORDER MODAL LOGIC

We introduce the labelled Gentzen-type structural rules and cut-free sequent calculus GHOML for the half-order modal logic without function symbols and prove that the calculus is sound and complete for the logic. Using syntactic methods, we prove that the structural and cut rules are admissible in GHOML. The obtained calculus enables us to present a decision procedure for the half-order modal logic considered.