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

TL;DR

The paper addresses decidability boundaries for classical and non-classical first-order logics within bounded languages by proving recursive inseparability via a domino-tiling construction that encodes Turing-computations into first-order formulas. It extends Trakhtenbrot-type results from $\mathbf{QCl}$ to the theories of symmetric/irreflexive graphs and to modal and superintuitionistic predicate logics, including their finite-frame variants, and it derives both dyadic and monadic inseparability, often with two-variable reductions. A central technical device is simulating worlds as elements of the domain and relativizing predicates to eliminate extra relations, enabling sharp results for $\mathbf{SIB}$, $\mathbf{SRB}$, and a range of modal and intuitionistic logics; the paper also discusses complexity and positive-fragment analogues. Overall, the work yields undecidability and non-recursive-enumerability results for numerous fragments and clarifies decidability boundaries for monadic fragments across classical, modal, and intuitionistic predicate logics, providing partial resolutions to several open questions about finite-frame and finite-domain logics.

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.

Figures (18)

• Figure 1: Simulating worlds by individuals
• Figure 2: Tile with marks
• Figure 3: Example of a tiling
• Figure 4: Tile types $t_0$, $t_s^\ast$, and $t_{\#}^\ast$
• Figure 5: Tile types for instructions $\delta_0\colon qs\mapsto q's'S$ and $\delta_0\colon q\#\mapsto q'\#S$

Theorems & Definitions (231)

• Proposition 2.1
• proof
• Lemma 3.1
• proof
• Lemma 3.2
• proof
• Theorem 3.3: Trakhtenbrot
• proof
• Lemma 3.4
• proof