Modal Logics and Local Quantifiers: A Zoo in the Elementary Hierarchy

We study a family of modal logics interpreted on tree-like structures, and featuring local quantifiers there exists(k)p that bind the proposition p to worlds that are accessible from the current one in at most k steps. We consider a first-order and a second-order semantics for the quantifiers, which enables us to relate several well-known formalisms, such as hybrid logics, S5Q and graded modal logic. To better stress these connections, we explore fragments of our logics, called herein round-bounded fragments. Depending on whether first or second-order semantics is considered, these fragments populate the hierarchy 2NExP subset of 3NExP subset of ... or the hierarchy 2AExP(pol) subset of 3AExP(pol) subset of ..., respectively. For formulae up-to modal depth k, the complexity improves by one exponential.