Some results in model theory of inquisitive modal logic

Inquisitive logic is a generalization of classical logic which, besides statements, also expresses questions. The language of classical propositional logic is extended with a new connective ⪕, called inquisitive disjunction. For example, p ⪕ q can be read as the question “whether p or q is the case”. Although intuitively there is no sense for a question to be true or false, there is a sense in which a question can be said to be settled by given information. This is achieved by using the so-called support semantics, a possible world semantics in which, instead of a satisfaction relation between worlds and formulas, a support relation is established between sets of worlds and formulas.
Since a possible world semantics is used, it is very natural to combine inquisitive and modal logic, so, for example, in the epistemic context we can express statements like “agent knows whether p”, namely by □(p ⪕ ¬p).
A further enrichment, the inquisitive modal logic InqML, was first introduced in Ciardelli's dissertation. Its language contains a new modality ⊞, which is a natural analogue of □ w.r.t. the support semantics, and enables expressing statements like “agent wonders whether p”. This makes the semantics even more complex — not only sets of worlds, but also sets of sets of worlds need to be considered.
In Ciardelli's dissertation, soundness and completeness of InqML is proved. Notions of bisimulations, bisimulation games and translations from InqML to two-sorted first-order logic are developed, and analogues of the Van Benthem Characterization Theorem are proved in works by Ciardelli and Otto and by Meissner and Otto.
Our contributions include the adaptation of the filtration technique to support semantics, and the definition and properties of the bisimulation quotient for InqML. Using filtration, we show that InqML has the finite model property and, consequently, InqML is decidable.