EXPSPACE-Completeness of the Logics K4xS5 and S4xS5 and the Logic of Subset Spaces, Part 1: ESPACE-Algorithms

Gisela Krommes; Peter Hertling

EXPSPACE-Completeness of the Logics K4xS5 and S4xS5 and the Logic of Subset Spaces, Part 1: ESPACE-Algorithms

T0 review · 0 major / 6 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The satisfiability problems of K4×S5, S4×S5, and the subset space logic SSL are decidable in single-exponential space, placing them in ESPACE.

desk verdict A solid, careful upper-bound proof that settles a twenty-year-old question; the tableau-cloud method and counting lemma are genuinely new. read the letter →

arxiv 1908.03501 v1 pith:DDTIMHCG submitted 2019-08-09 cs.LO cs.CCmath.LO

Peter Hertling , Gisela Krommes This is my paper · ORCID

classification cs.LOcs.CCmath.LO MSC 03B4568Q1703D15

keywords bimodalproductlogicssubsetspacelogicsatisfiabilityproblemEXPSPACE-completenessESPACEtableaualgorithmsK4×S5S4×S5

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper establishes that the satisfiability problems for the bimodal product logics K4×S5 and S4×S5 and for the subset space logic SSL are solvable by deterministic Turing machines using only single-exponential space, i.e., O($2^{{c n}}$) for a constant c. More precisely, K4×S5 is decided in O(n·$2^{{3n}}$) space, while S4×S5 and SSL are decided in O(n·$2^{{2n}}$) space. These are the first ESPACE upper bounds for the three problems, improving the previous N2EXPTIME bound. Together with the companion paper's EXPSPACE-hardness result, this settles a conjecture stated in the literature that these logics are EXPSPACE-complete.

What carries the argument

The load-bearing objects are 'tableau-clouds': sets of complete tableau-sets that represent the equivalence classes of the K-modality, so that all K-formulas are satisfied inside one cloud and commutativity conditions are automatically satisfied when clouds are linked. The algorithms recursively assemble these clouds into partial tableaux, trying backwards loops to already built clouds before creating a new successor cloud. The proof of the space bound rests on the maximum-chain-length lemma for transitive relations lifted to the power set: a transitive relation on a finite set S induces a transitive relation on P(S) whose chains have length at most 2·|S_≡|, bounding how often the minimal-cloud set can change and hence bounding recursion depth.

What would settle it

Exhibit a bimodal formula that is satisfiable in a K4×S5 commutator model but not in any K4×S5 product model (or the analogous counterexample for S4×S5, or a formula with a cross axiom model but no subset space model). No such counterexample is known, and the paper relies on the cited theorem that none exists.

Watch

Extended reading notes

Core claim

The central discovery is a decision method that replaces the search for a possibly infinite product model by the search for a finite object built from prefabricated parts called 'tableau-clouds' — collections of complete formula-sets that mirror the equivalence classes of the knowledge modality. The paper proves that a formula is satisfiable in the appropriate class of models exactly when such a partial tableau exists, and gives recursive algorithms that search for partial tableaux. The recursion depth is controlled by a combinatorial bound on chains in the induced relation on sets of tableau-sets, which yields O(n·|T|^3) space where T is the set of relevant tableau-sets. Since |T| ≤ 2^n, this gives O(n·$2^{{3n}}$) for K4×S5; an extra counting argument improves the bound to O(n·$2^{{2n}}$) for S4×S5 and SSL.

Load-bearing premise

The load-bearing premise is the cited equivalence between satisfiability in product frames and satisfiability in the more general commutator frames (and, for SSL, between subset space models and cross axiom models); if that equivalence ever failed, the algorithms would decide the wrong class of models and the ESPACE upper bound would not apply to the logics as standardly defined.

Editorial extensions

If this is right

The three satisfiability problems are EXPSPACE-complete, once paired with the companion paper's EXPSPACE-hardness proof.
K4×S5 can be decided in O(n·2^{3n}) space, and S4×S5 and SSL in O(n·2^{2n}) space, by explicit deterministic algorithms.
The previous N2EXPTIME upper bound for these problems is superseded, and the conjectured EXPSPACE-completeness is confirmed.
Satisfiability in these logics is equivalent to existence of a finite partial tableau over at most 2^n tableau-sets, so an infinite-model search is replaced by a finite one.
Because ESPACE is closed under complements, the same space bounds apply to validity as well as satisfiability for these logics.

Reading between the lines

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

The maximum-chain-length bound in Proposition 4.11 is a general combinatorial tool that could give recursion-depth bounds for other tableau or mosaic methods without first constructing exponential-size models.
The counting argument bounding the number of tableau-sets might be refined further, especially for K4×S5 with a modified tableau definition, to lower the exponents below 3 and 2.
A natural testable extension is to adapt the tableau-cloud construction to other product combinations, such as products with transitive or Euclidean modalities; if the chain-length control survives, similar ESPACE bounds would follow.
For SSL, richer subset-space logics with additional modalities could be approached by extending cross-axiom tableau-clouds, although the paper does not address such extensions.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Peter, if you want to know whether this paper is worth your time: yes. Hertling and Krommes give an ESPACE upper bound for K4×S5, S4×S5, and SSL, improving the standing N2EXPTIME bound and, with their companion lower-bound paper, establishing EXPSPACE-completeness for all three. The result itself is the main event and, as far as I can tell, correct.

What's actually new: the tableau-cloud construction. Instead of building tableaux point by point, they work with prefabricated sets of tableau-sets—clouds—that mirror L-equivalence classes. This neatly handles both the diamond successors and the commutativity conditions. The recursive algorithm is similar in spirit to Ladner's for S4, but the cloud machinery is original. The combinatorial core is a set of observations about transitive relations and maximum chain length, culminating in Proposition 4.11, which bounds the chain length of the lifted preorder on the power set. On top of that they prove a counting lemma (Proposition 9.1) showing that for S4×S5 and SSL the number of tableau-sets is at most 2^{2n/3}, which yields the sharper O(n·2^{2n}) space bound. The counting argument is a little tedious but sound.

Where are the soft spots? The upper bound is proved for commutator models, not product models directly. They rely on Lemma 2.7, citing Gabbay–Shehtman, to equate X×S5-satisfiability in product frames with satisfiability in commutator frames, and on Dabrowski–Moss–Parikh for the SSL cross-axiom characterization. These are standard published results, so it's a verification dependency, not a flaw. But if either of those cited theorems had an unstated restriction, the result wouldn't apply to the logics as usually defined. I see no evidence of that.

The space analysis is an implementation sketch on a multi-tape Turing machine, not a formal proof with explicit tape counts. That's normal for this kind of paper; the bounds are plausible and the recursion-depth argument is transparent. The paper is also one half of a pair—the lower bound is in Part 2, so the abstract's completeness claim rests on the companion.

Overall: this deserves a serious referee. I would send it to a good modal-logic journal and expect acceptance after minor comments. The main thing to check carefully is the transfer lemma and the counting induction.

Referee Report

0 major / 6 minor

Summary. The paper presents deterministic single-exponential-space decision procedures for the satisfiability problems of the bimodal product logics K4×S5 and S4×S5 and of the subset space logic SSL. The main result, Theorem 3.1, states that K4×S5 satisfiability can be decided in space O(n·2^{3n}) and that S4×S5 and SSL satisfiability can be decided in space O(n·2^{2n}), where n is the input formula length. The algorithms are based on a tableau method using 'tableau-clouds', prefabricated sets of complete tableau-sets, and on recursive procedures similar to Ladner's algorithm for S4. The proof proceeds by establishing an equivalence between satisfiability and the existence of partial tableaux (Proposition 6.5), proving the correctness of the recursive algorithms (Propositions 7.2 and 7.4), and giving space bounds through a careful analysis of the recursion depth using combinatorial estimates on the maximum chain length of certain relations (Propositions 4.11, 8.1, 8.3, and Corollary 8.2). A separate counting argument (Proposition 9.1) improves the bound on the number of tableau-sets for S4×S5 and SSL, yielding the sharper O(n·2^{2n}) bound. The companion paper establishes EXPSPACE-hardness, so together the results show EXPSPACE-completeness.

Significance. If the results are correct, they constitute a substantial improvement over the previously known N2EXPTIME upper bound for these three logics and settle the upper-bound side of Marx's conjecture that K4×S5 and S4×S5 are EXPSPACE-complete. The tableau-cloud framework and the combinatorial observations about maximum chain lengths (Section 4.2, especially Proposition 4.11) are likely to be of independent interest for other modal and description logics. The upper-bound proofs are largely self-contained, with the only external dependencies being the standard Gabbay-Shehtman equivalence between product and commutator frames (Lemma 2.7) and the Dabrowski-Moss-Parikh characterization of SSL by cross axiom models. The paper gives detailed, checkable proofs of the tableau-model equivalence, the correctness of the recursive algorithms, and the space bounds, including explicit high-level implementation sketches for the Turing-machine storage of tableau-sets and tableau-clouds.

minor comments (6)

[Lemma 6.4.2] The Truth Lemma is stated as a biconditional for all points (F,F) in the model MT, but the proof of the 'only if' direction for the case ψ=□χ invokes 'the second condition in Definition 5.5', which applies only to F∈T\{F0,...,F_{m-1}}. For a partial tableau for a one-point sequence (ϕ,F0), the condition does not apply to F0. This is not merely a gap in the proof: the statement is false. For example, take X=K4×S5, ϕ=□p, F0={{□p},∅}, and T={F0}. Then T is a partial tableau for (ϕ,F0), but in MT there are no ♦-successors from (F0,∅) (since F0≤XF0 fails because {□p}≼{□p} would require p∈{□p}), so MT,(F0,∅)|=□p vacuously, while □p∉∅. The 'if' direction, which is the direction used in Proposition 6.5, is correct. I recommend either restricting the 'only if' direction to points with F∉{F0,...,F_{m-1}}, or stating the lemma only in the direction actually needed.
[Proof of Proposition 8.3] In the paragraph beginning 'Otherwise, as at least the first part of (II) is satisfied for m', the text reads 'there is some G∈F_{m+1} with F_m≼X G and χ_m∈G' and later 'χ_~m∈G'. These should be 'χ_m∉G' and 'χ_~m∉G', respectively, to match condition (II) in Definition 7.1, which requires that the successor tableau-set excludes the formula χ. The intended argument is clear, but the typos should be corrected.
[Remark 8.4] Twice, the alphabet for the length of a bimodal formula is given as '{(,),¬,∧,□,K,X,0,1}'. Since variables in Definition 2.1 are written with a lowercase 'x' (as in x0, x101), the alphabet should presumably include 'x' rather than 'X'.
[Proposition 9.1 and its proof] The notation '2(2·n/3)' and similar expressions (e.g., '2(2·n/3)−1') are meant to denote powers 2^{2n/3} and 2^{(2n/3)−1}. The current notation is ambiguous and should be typeset with an explicit exponent.
[Definition 5.2(1)(a)] The condition '{ψ∈L| □ψ∈F}⊆ G' uses the entire language L, but since F⊆sf(ϕ), the set is actually a subset of sf(ϕ). Rewriting it as '{ψ∈sf(ϕ)| □ψ∈F}⊆ G' would improve readability and avoid any confusion about infinite languages.
[Section 8 (proof of Proposition 8.1)] The space analysis is presented as a high-level implementation sketch. In particular, it would be helpful to explain how the recursion stack stores the sequence (F0,...,Fm) without storing the entire sequence in each activation record, e.g., by storing only the new cloud and traversing the stack to check the pairwise-difference condition. This is not a correctness concern, but it would make the O(n(n+A)^3) bound easier to verify.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the ESPACE upper bounds are proved by self-contained tableau constructions and space analysis, with external semantic equivalences cited from independent prior work.

full rationale

The derivation chain for the ESPACE upper bounds is self-contained. The main correctness link between satisfiability and tableau existence is proved directly in Propositions 6.5 and 7.2 via Lemma 6.4 (the Truth Lemma), not assumed from prior work. The only non-derived bridge is Lemma 2.7, which equates satisfiability in product models with satisfiability in commutator models and explicitly cites Gabbay and Shehtman [8, Theorem 7.12], and the analogous SSL characterization by cross axiom models, cited from Dabrowski, Moss, and Parikh [4]. These are external, independently published results, not citations to the present authors' own work, and they are not equivalent to the paper's target theorem. The space bounds are obtained by explicit counting: |T_X^phi| ≤ 2^n in Proposition 8.1, the refined counting bound |T_X^phi| ≤ 2^{2n/3} in Proposition 9.1, and the chain-length estimates in Section 4.2. No parameter is fitted to data, and no prediction is renamed as an input. The companion paper [14] is cited only for the lower-bound part of EXPSPACE-completeness and is explicitly not used in this paper's upper-bound proof; the self-citations [16,17] are historical context for the previous PSPACE lower bound for SSL. Accordingly, there is no circular step, not even a load-bearing self-citation.

Assumptions & free parameters 0 free parameters · 4 assumptions · 1 invented entities

The proof uses standard mathematical induction and counting arguments, plus two external semantic equivalences that are cited but not proved. No free parameters are fitted to data. The only new objects are the tableau-sets and tableau-clouds, which are explicitly defined and used as proof devices rather than unexplained postulates.

assumptions (4)

domain assumption Equivalence of product and commutator models for K4×S5 and S4×S5 (Lemma 2.7, citing Gabbay-Shehtman)
Used to define satisfiability for K4×S5 and S4×S5 in terms of commutator models, on which the tableau algorithms are based.
domain assumption Equivalence of subset space models and cross axiom models for SSL (citing Dabrowski, Moss, and Parikh)
Used to define SSL-satisfiability in terms of cross axiom models, on which the tableau algorithms are based.
standard math Standard model of computation (multi-tape Turing machines) and the definition of ESPACE
Underpins the space complexity bounds and the machine model for the algorithms.
standard math Structural induction on formulas
Used in the truth lemma (Lemma 6.4.2) to show that tableau membership matches truth in the constructed model.

invented entities (1)

Tableau-clouds
purpose: A set of tableau-sets representing an equivalence class of worlds in the intended model; used to build finite tableaux while automatically satisfying commutativity.
New mathematical object defined in Deﬁnition 5.1.4. It is fully specified and used transparently in the proofs; it does not require empirical support, and its use is not circular because the tableau correspondence is proved directly.

how reviews work

0 comments

Cite this review

Pith. "Pith review of EXPSPACE-Completeness of the Logics K4xS5 and S4xS5 and the Logic of Subset Spaces, Part 1: ESPACE-Algorithms." pith.science (2026). https://pith.science/paper/DDTIMHCG

@misc{pith2026190803501,
  author       = {Pith},
  title        = {Pith review of: EXPSPACE-Completeness of the Logics K4xS5 and S4xS5 and the Logic of Subset Spaces, Part 1: ESPACE-Algorithms},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DDTIMHCG}},
  note         = {Machine review of arXiv:1908.03501}
}

read the original abstract

It is known that the satisfiability problems of the product logics K4xS5 and S4xS5 and of the logic SSL of subset spaces are in N2EXPTIME. We improve this upper bound for the complexity of these problems by presenting ESPACE-algorithms for these problems. In another paper we show that these problems are EXPSPACE-hard. This shows that all three problems are EXPSPACE-complete.

Figures

Figures reproduced from arXiv: 1908.03501 by the authors.

**Figure 2.** An illustration of a model (on the left) and the tableau (on the right) based on it. [PITH_FULL_IMAGE:figures/full_fig_p016_2.png] view at source ↗

**Figure 3.** An illustration of a tableau (on the left) and the model (on the right) based on it. [PITH_FULL_IMAGE:figures/full_fig_p018_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

24 extracted references · 17 canonical work pages

[1]

Baader and U

F. Baader and U. Sattler. An overview of tableau algorithms for description logics. Studia Logica, 69:5–40, 2001

work page 2001
[2]

Blackburn, J

P. Blackburn, J. van Benthem, and F. Wolter, editors.Handbook of Modal Logic, vol- ume 3 ofStudies in Logic and Practical Reasoning. Elsevier B. V., Amsterdam, 2007

work page 2007
[3]

S. A. Cook. The complexity of theorem-proving procedures. In M. A. Harrison, R. B. Banerji, and J. D. Ullman, editors,Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, pages 151–158. ACM, 1971

work page 1971
[4]

Dabrowski, L

A. Dabrowski, L. S. Moss, and R. Parikh. Topological reasoning and the logic of knowl- edge. Ann. Pure Appl. Logic, 78:73–110, 1996. References 30

work page 1996
[5]

D’Agostino, D

M. D’Agostino, D. M. Gabbay, R. Hähnle, and J. Posegga, editors.Handbook of Tableau Methods. Kluwer Academic Publishers, Dordrecht, 1999

work page 1999
[6]

M. Fitting. Proof Methods for Modal and Intuitionistic Logics, volume 169. Springer Science & Business Media, 1983

work page 1983
[7]

M. Fitting. Modal proof theory. InHandbook of Modal Logic, volume 3 ofStud. Log. Pract. Reason., pages 85–138. Elsevier B. V., Amsterdam, 2007

work page 2007
[8]

D. M. Gabbay and V. B. Shehtman. Products of modal logics, part 1.Logic Journal of IGPL, 6(1):73–146, 1998

work page 1998

Show all 24 references

[9]

R. Goré. Tableau methods for modal and temporal logics. In Handbook of Tableau Methods, pages 297–396. Kluwer Acad. Publ., Dordrecht, 1999

1999
[10]

Governatori

G. Governatori. Labelled modal tableaux. InAdvances in Modal Logic,, volume 7, pages 87–110, 2008

2008
[11]

G. Grätzer. Lattice Theory: Foundation. Birkhäuser/Springer Basel AG, Basel, 2011

2011
[12]

Heinemann

B. Heinemann. Augmenting subset spaces to cope with multi-agent knowledge. In International Symposium on Logical Foundations of Computer Science, pages 130–145. Springer, 2016

2016
[13]

Heinemann

B. Heinemann. A subset space perspective on agents cooperating for knowledge. In International Conference on Knowledge Science, Engineering and Management, pages 503–514. Springer, 2016

2016
[14]

Hertling and G

P. Hertling and G. Krommes. EXPSPACE-completeness of the logics K4× S5 and S4× S5 and the logic of subset spaces, part 2:EXPSPACE-hardness, 8 2019. Submitted for publication

2019
[15]

A. S. Kechris.Classical Descriptive Set Theory.Graduate Texts in Mathematics. 156. Berlin: Springer-Verlag, 1995

1995
[16]

G. Krommes. A new proof of decidability for the modal logic of subset spaces. InEighth ESSLLI Student Session, pages 137–148. Citeseer, 2003

2003
[17]

G. Krommes. Untersuchungen zur modalen Logik von Mengenräumen: Vollständigkeit, Entscheidbarkeit, Komplexität. Master’s thesis, FernUniversität Hagen, 2003

2003
[18]

Kurucz, F

A. Kurucz, F. Wolter, M. Zakharyaschev, and D. M. Gabbay.Many-Dimensional Modal Logics: Theory and Applications, Volume 148 (Studies in Logic and the Foundations of Mathematics). North Holland, 2003

2003
[19]

R. E. Ladner. The computational complexity of provability in systems of modal propo- sitional logic. SIAM Journal on Computing, 6(3):467–480, 1977

1977
[20]

M. Marx. Complexity of products of modal logics.Journal of Logic and Computation, 9(2):197–214, 1999. References 31

1999
[21]

I. Németi. Decidable versions of ﬁrst order logic and cylindric-relativized set algebras. In D. G. L. Csirmaz and M. de Rijke, editors,Logic Colloquium, volume 92, pages 171–241. CSLI Publications, 1995

1995
[22]

C. H. Papadimitriou. Computational Complexity. Amsterdam: Addison-Wesley Pub- lishing Company, 1994

1994
[23]

Parikh, L

R. Parikh, L. S. Moss, and C. Steinsvold. Topology and epistemic logic. InHandbook of Spatial Logics, pages 299–341. Springer, 2007

2007
[24]

Schröder.Ordered sets

B. Schröder.Ordered sets. Birkhäuser/Springer, second edition, 2016. An introduction with connections from combinatorics to topology

2016

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

Baader and U

F. Baader and U. Sattler. An overview of tableau algorithms for description logics. Studia Logica, 69:5–40, 2001

work page 2001

[2] [2]

Blackburn, J

P. Blackburn, J. van Benthem, and F. Wolter, editors.Handbook of Modal Logic, vol- ume 3 ofStudies in Logic and Practical Reasoning. Elsevier B. V., Amsterdam, 2007

work page 2007

[3] [3]

S. A. Cook. The complexity of theorem-proving procedures. In M. A. Harrison, R. B. Banerji, and J. D. Ullman, editors,Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, pages 151–158. ACM, 1971

work page 1971

[4] [4]

Dabrowski, L

A. Dabrowski, L. S. Moss, and R. Parikh. Topological reasoning and the logic of knowl- edge. Ann. Pure Appl. Logic, 78:73–110, 1996. References 30

work page 1996

[5] [5]

D’Agostino, D

M. D’Agostino, D. M. Gabbay, R. Hähnle, and J. Posegga, editors.Handbook of Tableau Methods. Kluwer Academic Publishers, Dordrecht, 1999

work page 1999

[6] [6]

M. Fitting. Proof Methods for Modal and Intuitionistic Logics, volume 169. Springer Science & Business Media, 1983

work page 1983

[7] [7]

M. Fitting. Modal proof theory. InHandbook of Modal Logic, volume 3 ofStud. Log. Pract. Reason., pages 85–138. Elsevier B. V., Amsterdam, 2007

work page 2007

[8] [8]

D. M. Gabbay and V. B. Shehtman. Products of modal logics, part 1.Logic Journal of IGPL, 6(1):73–146, 1998

work page 1998