Algorithmic properties of first-order modal logics of linear Kripke frames in restricted languages

Abstract

We study the algorithmic properties of first-order monomodal logics of frames $⟨\mathbb{N},\le ⟩$, $⟨\mathbb{N},<⟩$, $⟨\mathbb{Q},\le ⟩$, $⟨\mathbb{Q},<⟩$, $⟨\mathbb{R},\le ⟩$, $⟨\mathbb{R},<⟩$, as well as some related logics, in languages with restrictions on the number of individual variables as well as the number and arity of predicate letters. We show that the logics of frames based on $\mathbb{N}$ are ${\Pi }_1^1$-hard -- thus, not recursively enumerable -- in languages with two individual variables, one monadic predicate letter and one proposition letter. We also show that the logics of frames based on $\mathbb{Q}$ and $\mathbb{R}$ are ${\Sigma }_1^0$-hard in languages with the same restrictions. Similar results are obtained for a number of related logics.

References in corpus (4)

• Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter
• Complexity and expressivity of propositional dynamic logics with finitely many variables
• Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables
• Recursive enumerability and elementary frame definability in predicate modal logic