ИСТИНА

We study algorithmic properties of first-order predicate monomodal logics of the frames (ℕ,<) and (ℕ,≤) in languages with restrictions on the number of individual variables as well as the number and arity of predicate letters. The languages we consider have no constants, function symbols, or the equality symbol. We show that satisfiability for the logic of (ℕ,<) is Σ11-hard in languages with two individual variables and two monadic predicate letters. We also show that satisfiability for the logic of (ℕ,≤) is Σ11-hard in languages with two individual variables, two monadic, and one 0-ary predicate letter. Thus, these logics are Π11-hard, and therefore not recursively enumerable, in languages with the aforementioned restrictions.