Tabular intermediate logics comparison

Abstract

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