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

TL;DR

This paper proves that the two-variable fragment of superintuitionistic predicate logic over linear frames is undecidable, even with restrictions like positive formulas, a single binary predicate, or constant domains, advancing understanding of logical complexity.

Contribution

It establishes the undecidability of the two-variable fragment of superintuitionistic predicate logic over linear frames, using novel techniques involving tiling problems and double labeling.

Findings

The two-variable fragment is undecidable ($\,\Sigma^0_1$-complete).

Undecidability persists for the positive fragment with limited predicates.

The logic over the ordinal  is not recursively enumerable.

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.