A Reasoning System for Graded Modal Logic

In this paper, we propose a deduction system for the modal logic <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\mathbf{K}$</tex> with graded modalities, which is obtained by adding numerical constraints to the modal operators. Graded modalities can be seen as a generalization of traditional modal operators since they include numerical bounds in the modalities, thus enabling the formal treatment of more detailed expressions, such as “there are at least <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$n+1$</tex> individuals satisfying a certain property”, where <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$n$</tex> is a natural number. This kind of properties commonly arise in contexts such as concurrent systems: “if at least 3 processors are free, then proceed to compute the next task”, or epistemic logic:”if more than 2 people know <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$P$</tex>, then <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$P$</tex> is known”. The system is based on the notion of tree-hypersequents. We show the system is correct, i.e. sound and complete.