English

Tabular intermediate logics comparison

Logic in Computer Science 2025-09-16 v2

Abstract

Tabular intermediate logics are intermediate logics characterized by finite posets treated as Kripke frames. For a poset P\mathbb{P}, let L(P)L(\mathbb{P}) denote the corresponding tabular intermediate logic. We investigate the complexity of the following decision problem LogContain\mathsf{LogContain}: given two finite posets P\mathbb P and Q\mathbb Q, decide whether L(P)L(Q)L(\mathbb P) \subseteq L(\mathbb Q). By Jankov's and de Jongh's theorem, the problem LogContain\mathsf{LogContain} is related to the problem SPMorph\mathsf{SPMorph}: given two finite posets P\mathbb P and Q\mathbb Q, decide whether there exists a surjective pp-morphism from P\mathbb P onto Q\mathbb Q. Both problems belong to the complexity class NP. We present two contributions. First, we describe a construction which, starting with a graph G\mathbb{G}, gives a poset Pos(G)\mathsf{Pos}(\mathbb{G}) such that there is a surjective locally surjective homomorphism (the graph-theoretic analog of a pp-morphism) from G\mathbb{G} onto H\mathbb{H} if and only if there is a surjective pp-morphism from Pos(G)\mathsf{Pos}(\mathbb{G}) onto Pos(H)\mathsf{Pos}(\mathbb{H}). This allows us to translate some hardness results from graph theory and obtain that several restricted versions of the problems LogContain\mathsf{LogContain} and SPMorph\mathsf{SPMorph} are NP-complete. Among other results, we present a 18-element poset Q\mathbb{Q} such that the problem to decide, for a given poset P\mathbb{P}, whether L(P)L(Q)L(\mathbb{P})\subseteq L(\mathbb{Q}) is NP-complete. Second, we describe a polynomial-time algorithm that decides LogContain\mathsf{LogContain} and SPMorph\mathsf{SPMorph} for posets T\mathbb{T} and Q\mathbb{Q}, when T\mathbb{T} is a tree.

Keywords

Cite

@article{arxiv.2509.06841,
  title  = {Tabular intermediate logics comparison},
  author = {Paweł Rzążewski and Michał Stronkowski},
  journal= {arXiv preprint arXiv:2509.06841},
  year   = {2025}
}