Undecidable Propositional Bimodal Logics and One-Variable First-Order Linear Temporal Logics with Counting

摘要

First-order temporal logics are notorious for their bad computational behavior. It is known that even the two-variable monadic fragment is highly undecidable over various linear timelines, and over branching time even one-variable fragments might be undecidable. However, there have been several attempts at finding well-behaved fragments of first-order temporal logics and related temporal description logics, mostly either by restricting the available quantifier patterns or by considering sub-Boolean languages. Here we analyze seemingly "mild" extensions of decidable one-variable fragments with counting capabilities, interpreted in models with constant, decreasing, and expanding first-order domains. We show that over most classes of linear orders, these logics are (sometimes highly) undecidable, even without constant and function symbols, and with the sole temporal operator "eventually."