The logic of the hide and seek game \(\textsf{LHS}\) was proposed to reason about search missions and interactions between agents in pursuit-evasion environments. As proved by Li et al. (2021, 2023), having an equality constant in the language of \(\textsf{LHS}\) drastically increases its computational complexity: the satisfiability problem for \(\textsf{LHS}\) with multiple relations is undecidable. In this work, we improve the existing proof for the undecidability by showing that \(\textsf{LHS}\) with a single relation is undecidable. With the findings by Li et al. (2021, 2023), we provide a van Benthem style characterization theorem for the expressive power of the logic. Then, by ‘splitting’ the language of \(\textsf{LHS}^-\) , a crucial fragment of \(\textsf{LHS}\) without the equality constant, into two ‘isolated parts’, we provide a complete Hilbert style proof system for \(\textsf{LHS}^-\) and prove that its satisfiability problem is decidable, whose proofs would indicate significant differences between \(\textsf{LHS}^-\) and ordinary product logics. Moreover, we extend the proof system with some important modal principles and examine their behavior w.r.t. restricted classes of frames, and show general results about their completeness as well as incompleteness. Although \(\textsf{LHS}\) and \(\textsf{LHS}^-\) are frameworks for interactions of two agents, all results in the article can be easily transferred to their generalizations for settings with any \(n>2\) agents.
