Elementary modal logics and circuit complexity

Tenyo Takahashi

REVIEW

Elementary modal logics and circuit complexity

Tenyo Takahashi

Logic · Submitted 9 Sep 2026

Pith's verdict: A clean conditional result connecting elementarity to polynomial-time validity, with a novel graph-theoretic reduction producing infinitely many non-elementary K4-stable logics under P ≠ NP.

T0 · AI review

How this review was made: An AI referee (deepseek/deepseek-v4-flash) read the paper on September 11, 2026 and answered a fixed list of questions about it. T0 is the starting level every paper gets. The levels describe how deeply Pith has checked the paper, never the authors.

T0 AI review An AI read the paper and answered a fixed list of questions.
T1 Audit Automatic checks that the references and files the paper relies on exist and match.
T2 Compute The paper's code or calculations re-run with the same results.
T3 Formal statement The claims written out in a formal math language a computer can read.
T4 Proof Those claims proved, and the proof checked by computer.

How Pith checks papers →

· 3 minor · Ask about this paper · The compiled record · Read the full review →

Challenge this review Comment (0) Read on arXiv ↗

Cite ▾

arXiv ID2609.10872 (version 2)

Pith IDKJHVFK7K, Pith's permanent record of this paper and its review

CitationTenyo Takahashi. "Elementary modal logics and circuit complexity." arXiv:2609.10872 (2026). https://pith.science/paper/KJHVFK7K

Cite this reviewBibTeX for Pith's review of this paper

Claim paper

Why Pith says this

Highlight any text to comment on it.

Editor's note

read the letter

Bottom line: this is a good paper, and the reader report is accurate. The genuinely new thing is Theorem 2.7: if a finitely axiomatizable modal logic L is elementary, then Val(L) is in P. It is a simple idea once packaged, but it is real and useful: it converts elementarity into a complexity upper bound, and therefore lets NP-hardness results become non-elementarity results, conditionally. The application to K4-stable logics is also new: the reflexive bipartition-frame construction and the reduction from surjective H-coloring problems are carefully designed, and Claim 3.5 is the heart of the matter and it holds. The paper gives credit where due for the external NP-completeness results and for the earlier stable-formula machinery. The proofs are explicit and checkable; no code or formalization, but also no felt gaps.

Soft spots, in proportion. First, the central assumption P ≠ NP is load-bearing: if P = NP, the constructed logics might still be elementary, and the open question from [Bezhanishvili et al. 2018] remains open. The paper is explicit about this, so I do not count it as a flaw, but it is a real limitation on the strength of the conclusion. Second, the pairwise-distinctness argument in Theorem 3.7 is a bit terse: the cardinality point works because a stable image is surjective, but a referee may want that spelled out. Minor. Third, the K-stable and S4-stable cases are explicitly left open, with honest reasons given in Remarks 3.9 and 3.10. That is the right way to handle it. The self-citation to the author's earlier stable-canonical-formulas paper is legitimate and necessary for the pre-transitive generalization in Theorem 3.8; it is not padding.

Who this is for: modal logicians working on elementarity, canonicity, and stable logics, and possibly complexity theorists interested in modal validity problems. It deserves a serious referee. My own verdict is close to the reader's: accept, with minor revision. I would send it to review without hesitation, and I would be surprised if a competent referee found a substantive error.

Referee report

Minor objections (3)

[Section 3, Lemma 3.4] In the proof of Lemma 3.4, the reduction constructs F_G as the disjoint union of F*_{G,0} and F*_{G,1}. It is stated that 'a bipartition of G can be computed in polynomial time', which is correct. However, the unique bipartition of a connected bipartite graph is unique only up to reversal; the reduction handles both cases by constructing two copies. This is clear from the construction, but a brief remark that the reversal corresponds to swapping the two parts would improve readability.
[Section 3, Claim 3.5] In the converse direction of Claim 3.5, the argument that 'each preimage f^{-1}(a_H), f^{-1}(b_H), and f^{-1}(c_H) is a non-empty set of irreflexive points' relies on the fact that a_H, b_H, c_H are irreflexive in F*_H. This is correct. The proof then deduces that U must equal F*_{G,0} or F*_{G,1} because U is rooted and contains all irreflexive points of that component. This reasoning is valid, but it also implicitly uses that F*_{G,0} and F*_{G,1} each have exactly three irreflexive points (a, b, c), which is clear from the definition.
[Section 3, Theorem 3.7] In the proof of Theorem 3.7, the infinite family of bipartite graphs is given as H_m = C_{2m+6} or H_m = M_{m+4}. For M_{m+4}, the condition k≥4 corresponds to m≥0, which is fine. It might be helpful to explicitly note that m is a natural number (including 0) and that the graphs are distinct, so the resulting logics are distinct. The cardinality argument at the end of the proof already ensures distinctness, but a small remark about the indexing would improve clarity.

How Pith checks papers → · Full audit of this paper →

The paper

The paper claims

Infinitely many non-elementary modal logics exist, assuming P ≠ NP.

The reading

This paper establishes a bridge between the elementarity of a modal logic and the computational complexity of its finite-frame validity problem. The author proves that if a finitely axiomatizable modal logic L is elementary (i.e., sound and complete with respect to an elementary class of Kripke frames), then the problem of deciding whether a given finite Kripke frame validates L belongs to the complexity class P. Using this result as a tool, the paper then constructs an infinite family of finitely axiomatizable K4-stable logics for which the validity problem is coNP-complete. Under the assumption that P ≠ NP, these logics cannot be elementary because otherwise their validity problems would be in P. The construction relies on a reduction from surjective homomorphism problems on bipartite graphs (known to be NP-complete) to the non-validity of certain stable formulas. If the author is right, this gives a conditional negative answer to an open question about the elementarity of K4-stable logics and shows that an unconditional positive answer would imply P = NP.

What carries the argument

The chain of reasoning rests on two main mechanisms. (1) The connection established in Theorem 2.7: the elementarity of a finitely axiomatizable logic implies that its finite-frame validity problem is in P. (2) The class of stable formulas γ(F,∅) for transitive frames, which characterize when a finite rooted K4-frame F is a stable image of a rooted upset of another K4-frame. The paper constructs a specific family of rooted K4-frames F^*_H derived from bipartite graphs H, and shows that the validity problem of the logic axiomatized by K4 plus γ(F^*_H,∅) is coNP-complete by reducing the NP-complete Sur-Col(H) problem (testing surjective homomorphisms between graphs) to the complement problem of that validity. The reduction uses a careful orientation of bipartite graphs into reflexive bipartition frames, then into K4-frames with auxiliary irreflexive points that control the structure of stable images.

Extended reading notes

Core claim

The paper's central contribution is a conditional method for proving non-elementarity of modal logics via complexity theory. It first proves Theorem 2.7: for any finitely axiomatizable modal logic L, if L is elementary then Val(L) (the problem of deciding whether a given finite Kripke frame satisfies L) is in P. This is shown by combining a known characterization of elementarity (Proposition 2.4, due to Goldblatt et al.) with a compactness argument that extracts a finite first-order axiomatization of an elementary class containing all finite frames of L. The author then applies the contrapositive of Theorem 2.7: a logic whose validity problem is not in P (e.g., coNP-complete) cannot be elementary, assuming P ≠ NP. Using stable formulas for K4 (γ(F,∅)), the paper shows that for each bipartite graph H for which Sur-Col(H) is NP-complete on connected graphs (e.g., even cycles C_{2k} for k ≥ 3, or the graphs M_k from Campos et al.), the logic K4 + γ(F^*_H, ∅) has a coNP-complete validity problem (Lemma 3.4). Frameworks F^*_H are rooted transitive Kripke frames with a reflexive root and several irreflexive points. The reduction from Sur-Col(H) to the complement of Val(K4 + γ(F^*_H, ∅)) translates a connected bipartite graph G into a transitive frame F_G such that a surjective homomorphism from G to H exists exactly when the frame F^*_H is a stable image of a rooted upset of F_G. By Lemma 3.2, each such logic is K4-stable. Hence, for infinitely many distinct K4-stable logics, if they were elementary then Val would be in P, contradicting coNP-completeness under P ≠ NP (Theorem 3.7).

Load-bearing premise

The entire construction of non-elementary K4-stable logics depends on the unproven conjecture that P is not equal to NP; if P = NP, then the argument that these logics are non-elementary collapses, and the open question would remain open.

Editorial extensions

If this is right

If P ≠ NP, then infinitely many distinct finitely axiomatizable K4-stable logics are non-elementary; they also provide a conditional negative answer to the open problem [5, Problem 6.4] restricted to K4-stable logics.
For each m ≥ 1, the same method yields infinitely many finitely axiomatizable K4^{m+1}_1-stable logics that are non-elementary under P ≠ NP, and these logics are not K4^{m'+1}_1-stable for any m' < m (Theorem 3.8).
If one could prove unconditionally that all K4-stable logics are elementary, that proof would imply P = NP.
The approach does not directly extend to K-stable logics (because stable formulas are not available as axiomatizations) or to S4-stable logics (because the construction relies on irreflexive points).

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The paper suggests that non-elementarity among modal logics may be widespread, as it ties the existence of non-elementary logics to the existence of NP-complete graph problems. Any bipartite graph H whose surjective homomorphism problem is NP-complete gives rise to a non-elementary K4-stable logic under P≠NP. Future work could identify new such graphs, possibly leading to a richer landscape of non
The method implicitly shows that if P = NP, then all finitely axiomatizable K4-stable logics whose validity problem is defined through the constructed F^*_H would be elementary. This would not contradict the known existence of non-elementary logics like Grz, but it would remove the present family of examples.
A natural next step is to search for unconditional proofs of non-elementarity for the logics constructed here, perhaps by adapting the approach of Goldblatt–Hodkinson–Venema that uses Erdős graphs to separate elementarity and canonicity. If such unconditional proofs exist, they would strengthen the case that the assumption P≠NP is not essential for the result.
The reduction technique (orienting bipartite graphs into frames with a reflexive root and irreflexive auxiliary nodes) appears to be a general template; it may be applicable to other classes of modal logics that enjoy a stable formula characterization with suitable frame conditions.

Original abstract

A modal logic is elementary if it is sound and complete with respect to an elementary class of Kripke frames. We prove that if a finitely axiomatizable modal logic $L$ is elementary, then the validity problem for $L$, which asks whether a given finite Kripke frame validates $L$, is in the circuit complexity class uniform $\mathsf{AC}^0$. As an application, we construct infinitely many finitely axiomatizable $\mathsf{K4}$-stable logics that are not elementary. This result provides a negative answer to Problem 6.4 in [Bezhanishvili et al., 2018] for $\mathsf{K4}$-stable logics.

The compiled record

The paper's own sentences, arranged, kept beside the review and separate from it. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.

Compiled by classifier-1.13.0 via TypeSafe API, question bank abstract-p1-20260923, 2026-09-23: 1 request, 4,268 input tokens.

What the abstract itself states, as probabilities: claims first 0.04 · states limitation 0.81 · human participants 0.01 · controlled comparison 0.02 · randomized assignment 0.01 · states quantitative result 0.33 · compares with prior results 0.64 · mentions code or data availability 0.02.

The abstract, sentence by sentence

arXiv listing abstract v1. Results and the main claim are underlined; show every role.

A modal logic is elementary if it is sound and complete with respect to an elementary class of Kripke frames. We prove that if a finitely axiomatizable modal logic L is elementary, then the validity problem for L, which asks whether a given finite Kripke frame validates L, is in P. This allows us to transfer complexity results in graph theory to the study of elementarity of modal logics. As an application, we construct infinitely many finitely axiomatizable K4-stable logics that are not elementary, assuming P $\neq$ NP. This result provides a conditional negative answer to an open question in [Bezhanishvili et al., 2018] for K4-stable logics.

background contribution method result interpretation main claim

What the classifier reports for each sentence. The number is the probability it gave the label.
#	sentence	role	the authors' own work	states the main conclusion	strength
s0	A modal logic is elementary if it is sound and complete with respect to an elementary class of Kripke frames.	background 1.00	0.06	0.03	asserted 0.99
s1	We prove that if a finitely axiomatizable modal logic L is elementary, then the validity problem for L, which asks whether a given finite Kripke frame validates L, is in P.	result 0.95	0.93	0.54	asserted 1.00
s2	This allows us to transfer complexity results in graph theory to the study of elementarity of modal logics.	interpretation 0.78	0.67	0.05	asserted 0.93
s3	As an application, we construct infinitely many finitely axiomatizable K4-stable logics that are not elementary, assuming P $\neq$ NP.	result 0.90	0.96	0.73	asserted 0.99
s4	This result provides a conditional negative answer to an open question in [Bezhanishvili et al., 2018] for K4-stable logics.	interpretation 0.97	0.83	0.23	asserted 0.95

What kind of paper the classifier reports this is: theoretical result 1.00 · evidence from proof or derivation 1.00.

What was examined, and what was not

sources read

arXiv listing abstract v1

not examined

full text
figures and tables
references and citing sentences
relations to other papers

levels run

P abstract

not run

S sections
T body sentences
C citations
R cross-paper relations

Every quoted sentence on this record is the authors'. Every label is from Pith's closed vocabulary, with the probability shown beside it. Every number in the measurements table is the authors', checked by code. Record as JSON

Figures

**Figure 1.** The Kripke frame F. 3 Non-elementary K4-stable logics In this section, we show the existence of non-elementary K4-stable logics, assuming P ̸= NP. More specifically, we show that for certain K4-stable logics L, the problem Val(L) is coNP-complete, which by the contraposition of Theorem 2.7 implies that L is not elementary, assuming P ̸= NP. First, let us recall stable logics and stable formulas from [5] (see also [19] for a more comprehensive account). We follow the relational approach since it is more directly related to graph theory. A modal space, also known as a descriptive…

**Figure 2.** for an illustration of the reflexive bipartition frame FC6 of the 6-cycle C6; in this case, the reflexive bipartition frame is unique up to isomorphism. Note that a reflexive bipartition frame FH is not rooted in general. C6 ◦ ◦ ◦ ◦ ◦ ◦ FC6

**Figure 3.** The Kripke frame F ∗ C6 . Relations obtained by transitivity are omitted. Proof. First, note that the Kripke frame F ∗ H is a rooted K4-frame with root rH, so the stable formula γ(F ∗ H , ∅) is well-defined. For any finite K4-frame F, by Proposition 3.1, we have F ̸|= γ(F ∗ H , ∅) iff F ∗ H is a stable image of a rooted upset of F. Since deciding whether a finite Kripke frame validates K4 (i.e., is transitive) is clearly in P, it suffices to show that, given a finite K4-frame F, the problem of deciding whether the latter condition holds is NP-complete. Let us call this pr

**Figure 4.** The bipartite graphs K4,4 and M4. Theorem 3.7. There are infinitely many finitely axiomatizable K4-stable logics that are not elementary, assuming P ̸= NP. Proof. We begin by gathering examples of bipartite graphs to which Lemma 3.6 is applicable. Note that graphs of bounded diameter are connected. Vikas [25] showed that for the 6-cycle C6, the problem Sur-Col(C6) is NP-complete for graphs of diameter 4, and pointed out that the proof generalizes to even k-cycles for k ≥ 6. Recall that the complete bipartite graph Kk,k is the bipartite graph with a bipartition into two sets of k…

Figures reproduced from arXiv:2609.10872 by the authors.

References

Discussion

Disagree with the review, or know something it missed? Leave a comment, highlight any passage above to comment on it, or challenge this review formally.