Tabular intermediate logics comparison
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912585327050752 |
|---|---|
| author | Rzążewski, Paweł Stronkowski, Michał |
| author_facet | Rzążewski, Paweł Stronkowski, Michał |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_06841 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Tabular intermediate logics comparison Rzążewski, Paweł Stronkowski, Michał Logic in Computer Science 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. |
| title | Tabular intermediate logics comparison |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2509.06841 |