Recursive inseparability of classical theories of a binary predicate and non-classical logics of a unary predicate

Abstract

The paper considers algorithmic properties of classical and non-classical first-order logics and theories in bounded languages. The main idea is to prove the undecidability of various fragments of classical and non-classical first-order logics and theories indirectly, by extracting it as a consequence of the recursive inseparability of special problems associated with them. First, we propose a domino problem, which makes it possible to catch the recursive inseparability of two sets. Second, using this problem, we prove that the classical first-order logic of a binary predicate and the theory of its finite models where the predicate is symmetric and irreflexive are recursively inseparable in a language with a single binary predicate letter and three variables (without constants and equality). Third, we prove, for an infinite class of logics, that the monadic fragment of a modal predicate logic and the logic of the class of its finite Kripke frames are recursively inseparable in languages with a single unary predicate letter and two individual variables; the same result is obtained if we replace the condition of finiteness of frames with the condition of finiteness of domains allowed in frames. Forth, we expand the results to a wide class of superintuitionistic predicate logics. In particular, it is proved that the positive fragments of the intuitionistic predicate logic and the logic of the class of finite intuitionistic Kripke frames are recursively inseparable in the language with a single unary predicate letter and two individual variables. The technique used and the results obtained allow us to answer some additional questions about the decidability of special monadic fragments of some modal and superintuitionistic predicate logics.