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

TL;DR

This work resolves the long-standing open problem of the decidability of the two-variable fragment of the superintuitionistic predicate logic $\mathbf{QLC}$ on linear Kripke frames, proving it undecidable and in fact $\Sigma^0_1$-complete. The authors develop a tiling-based reduction that leverages a Cantor pairing encoding and a novel double-labeling technique to realize grid-like structures using only two individual variables, enabling a faithful simulation of tiling constraints within $\mathcal{L}$. Their construction yields a single formula $\varphi_T$ whose refutability aligns with the existence of a valid tiling, establishing both $\Sigma^0_1$- and $\Pi^0_1$-hardness for broad classes of logics, including those with expanding or constant domains, and extensions like $\mathbf{QLC.cd}$. The results carry over to positive fragments and suggest applicability to modal predicate logics, highlighting the depth of undecidability in non-classical logics even in very small languages; the paper also raises open questions about monadic simulations and the role of domain variations in these logics.

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ödel translation. We prove that the fragment is undecidable ($Σ^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 $ω$ as a Kripke frame is not recursively enumerable (even both $Σ^0_1$-hard and $Π^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.

Figures (6)

• Figure 1: Enumeration of $\mathds{N}\times\mathds{N}$
• Figure 2: Simulating a tiling
• Figure 3: Tile types $t_0$, $t_\Box^{\ast\ast}$, $t_s^\ast$, and $t_{\#}^\ast$
• Figure 4: Tile types for the instructions $\delta_0\colon qs\mapsto q's'S$ and $\delta_0\colon q\#\mapsto q'\#S$
• Figure 5: Tile types for the instructions $\delta_0\colon qs\mapsto q's'R$ and $\delta_0\colon q\#\mapsto q'\#R$

Theorems & Definitions (36)

• Lemma 5.1
• proof
• Lemma 5.2
• proof
• proof
• Theorem 6.1
• proof
• Theorem 6.2
• proof
• Corollary 6.3