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

TL;DR

This paper investigates the computational complexity of first-order modal logics over linear frames like natural numbers, rationals, and reals, revealing high complexity and non-recursive enumerability under certain language restrictions.

Contribution

It establishes the hardness results for these logics, showing they are $ ext{Pi}^1_1$-hard or $ ext{Sigma}^0_1$-hard depending on the underlying frame and language constraints.

Findings

Logics over $ ext{N}$ are $ ext{Pi}^1_1$-hard with specific language restrictions.

Logics over $ ext{Q}$ and $ ext{R}$ are $ ext{Sigma}^0_1$-hard under similar restrictions.

Certain related logics exhibit comparable high complexity results.

Abstract

We study the algorithmic properties of first-order monomodal logics of frames $\langle \mathbb{N}, \leq \rangle$, $\langle \mathbb{N}, < \rangle$, $\langle \mathbb{Q}, \leq \rangle$, $\langle \mathbb{Q}, < \rangle$, $\langle \mathbb{R}, \leq \rangle$, $\langle \mathbb{R}, < \rangle$, 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^0_1$-hard in languages with the same restrictions. Similar results are obtained for a number of related logics.