Superintuitionistic predicate logics of linear frames: undecidability with two individual variables

Abstract

The paper presents a solution to the long-standing question about the decidability of the two-variable fragment of the superintuitionistic predicate logic $\mathbf{QLC}$ defined by the class of linear Kripke frames, which is also the `superintuitionistic' fragment of the modal predicate logic $\mathbf{QS4.3}$, under the G\"odel translation. We prove that the fragment is undecidable ($\Sigma^0_1$-complete). The result remains true for the positive fragment, even with a single binary predicate letter and an infinite set of unary predicate letters. Also, we prove that the logic defined by ordinal $\omega$ as a Kripke frame is not recursively enumerable (even both $\Sigma^0_1$-hard and $\Pi^0_1$-hard) with the same restrictions on the language. The results remain true if we add also the constant domain condition. The proofs are based on two techniques: a modification of the method proposed by M.Marx and M.Reynolds, which allows us to describe tiling problems using natural numbers rather than pairs of numbers within an enumeration of Cantor's, and an idea of `double labeling' the elements from the domains, which allows us to use only two individual variables in the proof when applying the former method.