On the satisfiability problem for a 4-level quantified syllogistic and some applications to modal logic

We introduce a fragment of multi-sorted stratified syllogistic, called $4LQS^R$, admitting variables of four sorts and a restricted form of quantification, and prove that it has a solvable satisfiability problem by showing that it enjoys a small model property. Then, we consider the sublanguage $(4LQS^R)^k$ of $4LQS^R$, where the length of quantifier prefixes (over variables of sort 1) is bounded by k >= 0, and prove that its satisfiability problem is NP-complete. Finally we show that modal logics S5 and K45 can be expressed in $(4LQS^R)^1$.