pith. sign in

arxiv: 2511.19747 · v2 · submitted 2025-11-24 · 🧮 math.LO

Chopping More Finely: Finite Countermodels in Modal Logic via the Subdivision Construction

Tenyo Takahashi This is my paper

Pith reviewed 2026-05-17 04:22 UTC · model grok-4.3

classification 🧮 math.LO
keywords modal logicfinite model propertystable canonical rulessubdivision constructionKripke incompletenessmodal algebrasunion-splittings
0
0 comments X

The pith

The Subdivision Construction produces finite countermodels for modal logics and rule systems axiomatized by stable canonical formulas from finite-height algebras.

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

The paper presents the Subdivision Construction as a method for proving the finite model property in broad classes of modal logics and modal rule systems. It extends the framework of stable canonical rules by building finite modal spaces that function as countermodels. The method applies directly to logics and systems based on finite modal algebras of finite height. A reader would care because the finite model property supports decidability results and completeness classifications in modal logic. As a direct consequence the work isolates a class of union-splittings inside NExt(K4) that exhibit Kripke incompleteness of degree 1.

Core claim

The Subdivision Construction builds on the framework of stable canonical rules and produces a finite modal space, dually a finite modal algebra, that serves as a finite countermodel of such rules, yielding the finite model property for logics and rule systems axiomatized by stable canonical formulas and rules of finite modal algebras of finite height.

What carries the argument

The Subdivision Construction, which subdivides stable canonical rules of finite-height algebras to generate finite modal spaces while preserving stability.

If this is right

  • The finite model property holds for every modal logic axiomatized by stable canonical formulas of finite modal algebras of finite height.
  • The finite model property holds for every modal rule system with the same form of axiomatization.
  • A class of union-splittings in NExt(K4) has degree of Kripke incompleteness exactly 1.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same subdivision technique might be tested on stable canonical rules drawn from algebras whose height is finite but larger than those already covered.
  • If the construction scales, it could supply finite countermodels for additional rule systems that appear in epistemic or temporal reasoning.
  • The classification of union-splittings with incompleteness degree 1 might be compared directly with known examples of Kripke-incomplete logics to measure how finely the method chops the space of extensions.

Load-bearing premise

The logics and rule systems in question must be axiomatized exactly by stable canonical formulas and rules drawn from finite modal algebras of finite height, with subdivision preserving the needed stability and finiteness.

What would settle it

A concrete modal logic or rule system axiomatized by a stable canonical formula from a finite-height algebra for which no finite countermodel exists would show the construction fails to deliver the finite model property.

Figures

Figures reproduced from arXiv: 2511.19747 by Tenyo Takahashi.

Figure 1
Figure 1. Figure 1: One step of the Subdivision Construction. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
read the original abstract

We present a new method, the Subdivision Construction, for proving the finite model property (the fmp) for broad classes of modal logics and modal rule systems. The construction builds on the framework of stable canonical rules, and produces a finite modal space, dually, a finite modal algebra, that serves as a finite countermodel of such rules, yielding the fmp. We apply the Subdivision Construction to prove the fmp for logics and rule systems axiomatized by stable canonical formulas and rules of finite modal algebras of finite height. As a consequence, we identify a class of union-splittings in $\mathsf{NExt}(\mathsf{K4})$ with degree of Kripke incompleteness 1.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The paper introduces the Subdivision Construction, a new method building on the framework of stable canonical rules, to generate finite modal spaces (dually, finite modal algebras) that serve as countermodels. It applies this construction to establish the finite model property for modal logics and rule systems axiomatized by stable canonical formulas and rules arising from finite modal algebras of finite height, and derives as a consequence a class of union-splittings in NExt(K4) that have Kripke incompleteness degree 1.

Significance. If the central claims hold, the Subdivision Construction supplies a systematic technique for obtaining finite countermodels in a broad class of modal logics, extending the stable canonical rules framework and yielding concrete results on union-splittings. This would strengthen the toolkit for proving the finite model property, which is directly tied to decidability questions in modal logic.

major comments (1)
  1. [The central construction and its preservation argument (around the applications to finite-height algebras)] The argument that subdivision preserves stability (and hence the refutation of the target rule while validating the logic) for finite-height algebras is load-bearing for the fmp claim, yet the interaction between the subdivision operation and the stability condition is not made fully explicit. In particular, it is unclear whether the canonical embedding or the finite-height chain structure is maintained after subdivision, as required for the output algebra to remain a countermodel.
minor comments (1)
  1. Notation for the subdivided algebra and the induced modal space could be introduced more gradually to aid readability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading and for recognizing the potential of the Subdivision Construction. We address the single major comment below and will revise the manuscript to improve explicitness as indicated.

read point-by-point responses

  1. Referee: [The central construction and its preservation argument (around the applications to finite-height algebras)] The argument that subdivision preserves stability (and hence the refutation of the target rule while validating the logic) for finite-height algebras is load-bearing for the fmp claim, yet the interaction between the subdivision operation and the stability condition is not made fully explicit. In particular, it is unclear whether the canonical embedding or the finite-height chain structure is maintained after subdivision, as required for the output algebra to remain a countermodel.

    Authors: We thank the referee for identifying this point of potential unclarity. The preservation of stability is established in the proof of Theorem 4.2, which proceeds by showing that subdivision refines the underlying space while the finite-height assumption guarantees that all chains remain of bounded length and that the canonical embedding into the original algebra is preserved by the natural projection sending each subdivided point to its originating element. This ensures the subdivided algebra continues to refute the target stable canonical rule. We agree, however, that the interaction between subdivision and the stability condition could be drawn out more directly. In the revised manuscript we will insert a new lemma immediately preceding Theorem 4.2 that isolates the two preservation claims (chain-height invariance and embedding preservation) and supplies a short diagram illustrating the quotient map on a finite-height chain. This addition will make the argument fully explicit while leaving the original proof unchanged. revision: yes

Circularity Check

0 steps flagged

No significant circularity; Subdivision Construction derives new finite countermodels independently.

full rationale

The paper introduces the Subdivision Construction as a novel method that builds on the existing framework of stable canonical rules to produce finite modal spaces and algebras serving as countermodels. The derivation applies this construction to logics axiomatized by stable canonical formulas and rules from finite modal algebras of finite height, yielding the finite model property and consequences for union-splittings in NExt(K4). No quoted steps reduce the output countermodels to inputs by definition, fitted parameters renamed as predictions, or load-bearing self-citations whose validity depends on the present work. The construction generates new finite objects while preserving stability and finiteness, rendering the central claim self-contained against external benchmarks in modal logic.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the prior framework of stable canonical rules and the assumption that finite modal algebras of finite height admit stable canonical axiomatizations; no free parameters or new entities are introduced in the abstract.

axioms (1)
  • domain assumption Stable canonical rules and formulas provide a complete axiomatization for the target modal logics and rule systems.
    Invoked when the construction is applied to logics axiomatized by stable canonical formulas and rules of finite modal algebras of finite height.

pith-pipeline@v0.9.0 · 5410 in / 1236 out tokens · 25659 ms · 2026-05-17T04:22:14.917675+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

  1. [1]

    C. Bergman. Universal Algebra: Fundamentals and Selected Topics . Chapman and Hall/CRC., 2011. isbn: 9780429108082. https : / / doi . org / 10 . 1201 / 9781439851302

    work page 2011

  2. [2]

    Jankov Formulas and Axiomatization Techniques for Intermediate Logics

    G. Bezhanishvili and N. Bezhanishvili. “Jankov Formulas and Axiomatization Techniques for Intermediate Logics”. In: V.A. Yankov on Non-Classical Logics, History and Philosophy of Mathematics . Edited by A. Citkin and I. M. Van- doulakis. Cham: Springer International Publishing, 2022, pages 71–124. isbn: 978- 3-031-06843-0. https://doi.org/10.1007/978-3-03...

    work page doi:10.1007/978-3-031-06843-0_4 2022

  3. [3]

    Locally Finite Reducts of Heyting Algebras and Canonical Formulas

    G. Bezhanishvili and N. Bezhanishvili. “Locally Finite Reducts of Heyting Algebras and Canonical Formulas”. In: Notre Dame Journal of Formal Logic 58.1 (2017), pages 21–45. https://doi.org/10.1215/00294527-3691563

    work page doi:10.1215/00294527-3691563 2017

  4. [4]

    Stable Canonical Rules

    G. Bezhanishvili, N. Bezhanishvili, and R. Iemhoff. “Stable Canonical Rules”. In: The Journal of Symbolic Logic 81.1 (2016), pages 284–315. https://doi.org/10. 1017/jsl.2015.54

    work page 2016

  5. [5]

    Stable Modal Logics

    G. Bezhanishvili, N. Bezhanishvili, and J. Ilin. “Stable Modal Logics”. In: The Review of Symbolic Logic 11.3 (2018), pages 436–469. https : / / doi . org / 10 . 1017/S1755020317000375

    work page 2018

  6. [6]

    Topo-Canonical Completions of Closure Algebras and Heyting Algebras

    G. Bezhanishvili, R. Mines, and P. J. Morandi. “Topo-Canonical Completions of Closure Algebras and Heyting Algebras”. In: Algebra universalis 58.1 (2008), pages 1–34. https://doi.org/10.1007/s00012-007-2032-2

    work page doi:10.1007/s00012-007-2032-2 2008

  7. [7]

    Blok-Esakia Theorems via Stable Canon- ical Rules

    N. Bezhanishvili and A. M. Cleani. “Blok-Esakia Theorems via Stable Canon- ical Rules”. In: The Journal of Symbolic Logic (2025), pages 1–36. issn: 0022- 4812, 1943-5886. https : / / doi . org / 10 . 1017 / jsl . 2025 . 10126. (Visited on 10/22/2025)

    work page 2025

  8. [8]

    Blackburn, M

    P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Fourth printing with corrections. Cambridge Tracts in Theoretical Computer Science 53. Cambridge: Cambridge University Press, 2001. isbn: 9781107050884. https://doi.org/10. 1017/CBO9781107050884. 30

    work page 2001

  9. [9]

    W. J. Blok. On the Degree of Incompleteness of Modal Logics and the Covering Relation in the Lattice of Modal Logics . Technical Report 78-07. Department of Mathematics, University of Amsterdam, 1978

    work page 1978

  10. [10]

    That All Normal Extensions of S4.3 Have the Finite Model Property

    R. A. Bull. “That All Normal Extensions of S4.3 Have the Finite Model Property”. In: Mathematical Logic Quarterly 12.1 (1966), pages 341–344. https://doi.org/ 10.1002/malq.19660120129

    work page doi:10.1002/malq.19660120129 1966

  11. [11]

    Burris and H

    S. Burris and H. P. Sankappanavar. A Course in Universal Algebra . Volume 78. Graduate Texts in Mathematics. Reprinted in 2011. Springer-Verlag New York Inc., 1981. isbn: 978-1-4613-8132-7

    work page 2011

  12. [12]

    Chagrov and M

    A. Chagrov and M. Zakharyaschev. Modal Logic. Oxford Logic Guides. Oxford, New York: Oxford University Press, 1997. isbn: 978-0-19-853779-3

    work page 1997

  13. [13]

    An Incomplete Logic Containing S4

    K. Fine. “An Incomplete Logic Containing S4”. In: Theoria 40.1 (1974), pages 23–

    work page 1974

  14. [14]

    https://doi.org/10.1111/j.1755-2567.1974.tb00076.x

    work page doi:10.1111/j.1755-2567.1974.tb00076.x 1974

  15. [15]

    Logics Containing K4. Part I

    K. Fine. “Logics Containing K4. Part I”. In: The Journal of Symbolic Logic 39.1 (1974), pages 31–42. https://doi.org/10.2307/2272340

    work page doi:10.2307/2272340 1974

  16. [16]

    Logics Containing K4. Part II

    K. Fine. “Logics Containing K4. Part II”. In: The Journal of Symbolic Logic 50.3 (1985), pages 619–651. https://doi.org/10.2307/2274318

    work page doi:10.2307/2274318 1985

  17. [17]

    The Logics Containing S4.3

    K. Fine. “The Logics Containing S4.3”. In: Mathematical Logic Quarterly 17.1 (1971), pages 371–376. https://doi.org/10.1002/malq.19710170141

    work page doi:10.1002/malq.19710170141 1971

  18. [18]

    A General Filtration Method for Modal Logics

    D. M. Gabbay. “A General Filtration Method for Modal Logics”. In: Journal of Philosophical Logic 1.1 (1972), pages 29–34. https : / / doi . org / 10 . 1007 / BF00649988

    work page 1972

  19. [19]

    On Decidable, Finitely Axiomatizable, Modal and Tense Logics without the Finite Model Property Part I

    D. M. Gabbay. “On Decidable, Finitely Axiomatizable, Modal and Tense Logics without the Finite Model Property Part I”. In: Israel Journal of Mathematics 10.4 (1971), pages 478–495. issn: 1565-8511. https://doi.org/10.1007/BF02771736

    work page doi:10.1007/bf02771736 1971

  20. [20]

    Continuity, Freeness, and Filtrations

    S. Ghilardi. “Continuity, Freeness, and Filtrations”. In: Journal of Applied Non- Classical Logics 20.3 (2010), pages 193–217. https://doi.org/10.3166/jancl. 20.193-217. https://doi.org/10.3166/jancl.20.193-217

    work page doi:10.3166/jancl 2010

  21. [21]

    On the Existence of Finite Models and Decision Procedures for Propo- sitional Calculi

    R. Harrop. “On the Existence of Finite Models and Decision Procedures for Propo- sitional Calculi”. In: Mathematical Proceedings of the Cambridge Philosophical So- ciety 54.1 (1958), pages 1–13. https://doi.org/10.1017/S0305004100033120

    work page doi:10.1017/s0305004100033120 1958

  22. [22]

    Filtration Revisited: Lattices of Stable Non-Classical Logics

    J. Ilin. “Filtration Revisited: Lattices of Stable Non-Classical Logics”. Ph.D. the- sis. Amsterdam: Institute for Logic, Language and Computation, University of Amsterdam, 2018

    work page 2018

  23. [23]

    The Relationship between Deducibility in the Intuitionistic Propo- sitional Calculus and Finite Implicational Structures

    V. A. Jankov. “The Relationship between Deducibility in the Intuitionistic Propo- sitional Calculus and Finite Implicational Structures”. In: Soviet Mathematics Doklady 4 (1963), pages 1203–1204

    work page 1963

  24. [24]

    Canonical Rules

    E. Jeˇ r´ abek. “Canonical Rules”. In: The Journal of Symbolic Logic 74.4 (2009), pages 1171–1205. https://doi.org/10.2178/jsl/1254748686. 31

    work page doi:10.2178/jsl/1254748686 2009

  25. [25]

    Investigations on the Intuitionistic Propositional Calculus

    D. de Jongh. “Investigations on the Intuitionistic Propositional Calculus”. Ph.D. thesis. University of Wisconsin, 1968

    work page 1968

  26. [26]

    Modal logics with transitive closure: com- pleteness, decidability, filtration

    S. Kikot, I. Shapirovsky, and E. Zolin. “Modal logics with transitive closure: com- pleteness, decidability, filtration”. In:Advances in Modal Logic. Volume 13. College Publications, 2020, pages 369–388. isbn: 978-1-84890-341-8

    work page 2020

  27. [27]

    Modal Consequence Relations

    M. Kracht. “Modal Consequence Relations”. In: Studies in Logic and Practical Reasoning. Edited by P. Blackburn, J. van Benthem, and F. Wolter. Volume 3: Handbook of Modal Logic. Elsevier, 2007, pages 491–545. isbn: 978-0-444-51690-

    work page 2007

  28. [28]

    https://doi.org/10.1016/S1570-2464(07)80011-5

    work page doi:10.1016/s1570-2464(07)80011-5

  29. [29]

    Segerberg

    K. Segerberg. An Essay in Classical Modal Logic . Uppsala: Filosofiska f¨ oreningen och Filosofiska institutionen vid Uppsala universitet, 1971

    work page 1971

  30. [30]

    On Some Two-dimensional Modal Logics

    V. Shehtman. “On Some Two-dimensional Modal Logics”. In: Proceedings of the 8th International Congress on Logic, Methodology and Philosophy of Science . Vol- ume 1. Abstracts. 1987, pages 326–330

    work page 1987

  31. [31]

    Takahashi

    T. Takahashi. Decidability of Being a Union-splitting . 2025. https://arxiv.org/ abs/2510.14520

    work page arXiv 2025

  32. [32]

    Takahashi

    T. Takahashi. Stable Canonical Rules and Formulas for Pre-transitive Logics via Definable Filtration. 2025. https://arxiv.org/abs/2510.22638

    work page arXiv 2025

  33. [33]

    Union-splittings, the Axiomatization Problem, and the Rule Di- chotomy Property in Modal Logic

    T. Takahashi. “Union-splittings, the Axiomatization Problem, and the Rule Di- chotomy Property in Modal Logic”. Master’s thesis. Institute for Logic, Language and Computation, University of Amsterdam, 2025

    work page 2025

  34. [34]

    A Dual Characterization of Subdirectly Irreducible BAOs

    Y. Venema. “A Dual Characterization of Subdirectly Irreducible BAOs”. In: Studia Logica: An International Journal for Symbolic Logic 77.1 (2004), pages 105–115. https://doi.org/10.1023/B:STUD.0000034188.80692.46

    work page doi:10.1023/b:stud.0000034188.80692.46 2004

  35. [35]

    Algebras and Coalgebras

    Y. Venema. “Algebras and Coalgebras”. In: Studies in Logic and Practical Reason- ing. Edited by P. Blackburn, J. van Benthem, and F. Wolter. Volume 3: Handbook of Modal Logic. Elsevier, 2007, pages 331–426. isbn: 978-0-444-51690-9. https: //doi.org/10.1016/S1570-2464(07)80009-7

    work page doi:10.1016/s1570-2464(07)80009-7 2007

  36. [36]

    Canonical Formulas for K4. Part I: Basic Results

    M. Zakharyaschev. “Canonical Formulas for K4. Part I: Basic Results”. In: The Journal of Symbolic Logic 57.4 (Dec. 1992), pages 1377–1402. https://doi.org/ 10.2307/2275372

    work page doi:10.2307/2275372 1992

  37. [37]

    Canonical Formulas for K4. Part II: Cofinal Subframe Logics

    M. Zakharyaschev. “Canonical Formulas for K4. Part II: Cofinal Subframe Logics”. In: The Journal of Symbolic Logic 61.2 (1996), pages 421–449. https://doi.org/ 10.2307/2275669

    work page doi:10.2307/2275669 1996

  38. [38]

    Canonical Formulas for K4. Part III: The Finite Model Prop- erty

    M. Zakharyaschev. “Canonical Formulas for K4. Part III: The Finite Model Prop- erty”. In: The Journal of Symbolic Logic 62.3 (1997), pages 950–975. https:// doi.org/10.2307/2275581. 32

    work page doi:10.2307/2275581 1997