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

2025. No. 2505.00531.

Rybakov M.

The paper presents a solution to the long-standing question about the decidability of the two-variable fragment of the superintuitionistic predicate logic QLC defined by the class of linear Kripke frames, which is also the  superintuitionistic’ fragment of the modal predicate logic QS4:3, under the Gödel translation. We prove that the fragment is undecidable. 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 ! as a Kripke frame is not  ecursively enumerable 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.

Keywords: undecidability, superintuitionistic predicate logic

Publication based on the results of: Плюралистические взгляды на логику и формальную философию (2026)