pith. sign in

arxiv: 2606.31920 · v1 · pith:KHQQRINFnew · submitted 2026-06-30 · 💻 cs.LO

Logics Containing wK4: Selection \`a la Fine

Simon Santschi , Niels C. Vooijs This is my paper

Pith reviewed 2026-07-01 02:10 UTC · model grok-4.3

classification 💻 cs.LO
keywords modal logicwK4finite model propertysubframe logicsiterative selectionweak transitivityFine's theorems
0
0 comments X

The pith

Generalizing Fine's iterative selection to weakly transitive logics yields a frame-theoretic proof of the finite model property for strongly cofinal subframe logics extending wK4.

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

The paper extends Fine's Iterative Selection Method, originally for transitive modal logics, to the setting of logics containing wK4. This produces a direct construction of finite frames that preserves truth of formulas, thereby establishing the finite model property for the relevant class of subframe logics. The identical construction also lifts Fine's Finite Width Theorem into the weakly transitive case. A reader would care because the approach replaces earlier algebraic arguments with an explicit semantic one and links two previously separate results of Fine under a single method.

Core claim

Adapting the iterative selection construction to weakly transitive frames shows that every strongly cofinal subframe logic extending wK4 has the finite model property; the same technique demonstrates that these logics satisfy a finite width property, thereby placing both of Fine's theorems in the same generalized setting.

What carries the argument

Iterative selection method, which successively chooses points in a frame to build a finite subframe while preserving satisfaction of modal formulas, now operating under weak transitivity and strong cofinality.

If this is right

  • Every strongly cofinal subframe logic above wK4 possesses the finite model property via an explicit frame construction.
  • Fine's Finite Width Theorem holds for all weakly transitive logics satisfying the same subframe condition.
  • The finite model property and finite width results are obtained from one uniform selection procedure rather than separate arguments.

Where Pith is reading between the lines

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

  • The method may apply directly to other modal logics whose frames satisfy weak transitivity but not full transitivity.
  • Similar selection constructions could be tested on subframe logics that are cofinal but not strongly cofinal to determine the exact boundary of the technique.
  • The frame-theoretic proof opens the possibility of extracting explicit bounds on model size that algebraic proofs do not immediately supply.

Load-bearing premise

The selection construction produces finite models precisely when the logic is weakly transitive and the subframe property is strongly cofinal.

What would settle it

A concrete counterexample would be any strongly cofinal subframe logic extending wK4 that fails to have the finite model property, or any instance where the iterative selection step fails to terminate with a finite frame.

Figures

Figures reproduced from arXiv: 2606.31920 by Niels C. Vooijs, Simon Santschi.

Figure 1
Figure 1. Figure 1: Diagram describing the definition of ⊑1 in Construction 6.1. All variables live in D. diagram bisimulation. This relation is defined in three stages, where each next stage is defined in terms of the previous stages by conditions resembling the back- and forth-condition for bisimulations. We fix a weakly transitive Kripke model M = ⟨X,R,V⟩ with upset U ⊆ X and D := X \U. Construction 6.1. Let ≡0 be the inte… view at source ↗
Figure 2
Figure 2. Figure 2: Case 1 (R(x,z)) in the proof of (C1) in Lemma 6.9. Lemma 6.8. Suppose that U and P are finite. Then there are only finitely many ≡δ -equivalence classes. If, in addition, each point in U is definable, then each ≡δ -equivalence class is definable and, in particular, dom(≡δ ) is definable. Proof. Notice that for x ∈ dom(≡δ ), we have [x]δ = [x]01 ∩ T {2· ([y]0 → [y]1) | y ∈ {x}∪sp∗ D (x)}. By Lemma 6.5, all … view at source ↗
Figure 3
Figure 3. Figure 3: Case 2 (x = z) in the proof of (C1) in Lemma 6.9. w z z ′ y y ′ x x ≡0 ≡0 ≡0 ∗ ≡1 ∗ w w ′ z z ′ y y ′ x x ≡0 ≡0 ≡0 ≡0 ∗ ≡1 ∗ w x x z ′ y y ′ x x ≡0 ≡0 ≡0 ≡0 ∗ ≡1 ∗ w z z x y y ′ x x ≡0 ≡0 ≡0 ≡0 ∗ ≡1 ∗ w w x x y y ′ x x ≡0 ≡0 ≡0 ≡0 ∗ ≡1 ∗ R(x,z), R(x,z ′ ) x = z, R(x,z ′ ) R(x,z), x = z ′ x = z = z ′ [PITH_FULL_IMAGE:figures/full_fig_p012_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The four cases in the proof of (C2) in Lemma 6.9. [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗
read the original abstract

We generalize Fine's Iterative Selection Method to the weakly transitive setting. In particular, this provides a transparent frame-theoretic proof of the finite model property for (strongly) cofinal subframe logics extending wK4, which was previously established using algebraic methods. Using the same construction, we generalize Fine's Finite Width Theorem to the weakly transitive setting, connecting these two celebrated theorems of Fine.

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

0 major / 2 minor

Summary. The paper generalizes Fine's Iterative Selection Method from the transitive case to weakly transitive frames. It supplies a frame-theoretic proof of the finite model property for (strongly) cofinal subframe logics extending wK4 (previously obtained algebraically) and, via the same construction, extends Fine's Finite Width Theorem to the weakly transitive setting, thereby connecting the two results.

Significance. If the iterative selection construction is verified, the work supplies a transparent, purely frame-theoretic route to the FMP for this family of logics and unifies two classical theorems of Fine under a single method. This strengthens the toolkit for subframe logics over wK4 and may facilitate further generalizations.

minor comments (2)
  1. The abstract states that the construction succeeds precisely under weak transitivity plus strong cofinality; the main text should contain an explicit statement (perhaps as a numbered theorem or proposition) of the precise hypotheses under which the selection procedure terminates with a finite model.
  2. Notation for the selection function and the cofinal subframe relation should be introduced with a short table or diagram in §2 or §3 to aid readability for readers coming from the transitive case.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our work and the recommendation of minor revision. The report correctly identifies the main contributions: the generalization of Fine's iterative selection method to weakly transitive frames, the resulting frame-theoretic proof of the finite model property for strongly cofinal subframe logics over wK4, and the extension of the finite width theorem. No specific major comments appear in the report, so we have no individual points requiring rebuttal or revision at this stage.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper generalizes Fine's Iterative Selection Method (an external prior result) to weakly transitive frames and uses it to reprove the finite model property for cofinal subframe logics over wK4 via frame theory rather than algebra. No equations, fitted parameters, self-citations, or ansatzes are described that reduce the central claim to its own inputs by construction. The work is self-contained against the cited external benchmark (Fine's theorems) with no load-bearing internal reductions.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

No free parameters, axioms, or invented entities are identifiable from the abstract.

pith-pipeline@v0.9.1-grok · 5607 in / 930 out tokens · 37502 ms · 2026-07-01T02:10:08.553210+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

17 extracted references · 12 canonical work pages

  1. [1]

    Baltag, N

    A. Baltag, N. Bezhanishvili & D. Fernández-Duque (2023): The Topological Mu-Calculus: Completeness and Decidability. Journal of the ACM 70(5):33, doi:10.1145/3623268

    work page doi:10.1145/3623268 2023

  2. [2]

    Bezhanishvili & N

    G. Bezhanishvili & N. Bezhanishvili (2012): Canonical Formulas for wK4. The Review of Symbolic Logic 5(4), pp. 731–762, doi:10.1017/S1755020312000251. 690 Logics Containing wK4: Selection à la Fine

    work page doi:10.1017/s1755020312000251 2012

  3. [3]

    Bezhanishvili, L

    G. Bezhanishvili, L. Esakia & D. Gabelaia (2011):Spectral and T0-Spaces in d-Semantics. In N. Bezhanishvili, S. Löbner, K. Schwabe & L. Spada, editors: Logic, Language, and Computation , Lecture Notes in Computer Science, Springer Berlin Heidelberg, pp. 16–29, doi:10.1007/978-3-642-22303-7_2

    work page doi:10.1007/978-3-642-22303-7_2 2011

  4. [4]

    Bezhanishvili, S

    G. Bezhanishvili, S. Ghilardi & M. Jibladze (2011): An Algebraic Approach to Subframe Logics. Modal Case. Notre Dame Journal of Formal Logic 52(2), pp. 187–202, doi:10.1215/00294527-1306190

    work page doi:10.1215/00294527-1306190 2011

  5. [5]

    Blackburn, M

    P. Blackburn, M. de Rijke & Y . Venema (2001):Modal Logic. Cambridge Tracts in Theoretical Computer Science 53, Cambridge University Press

    2001

  6. [6]

    Chagrov & M

    A. Chagrov & M. Zakharyaschev (1997): Modal Logic. Oxford Logic Guides 35, Oxford University Press

    1997

  7. [7]

    Chen & M

    Q. Chen & M. Ma (2025): The McKinsey Axiom on Weakly Transitive Frames. Studia Logica 113(6), pp. 1543–1566, doi:10.1007/s11225-024-10145-x

    work page doi:10.1007/s11225-024-10145-x 2025

  8. [8]

    Esakia (2001): Weak transitivity—a restitution

    L.L. Esakia (2001): Weak transitivity—a restitution . Logical investigations 8, pp. 244–255

    2001

  9. [9]

    Fine (1974): Logics containing K4

    K. Fine (1974): Logics containing K4. part I. The Journal of Symbolic Logic 39(1), doi:10.2307/2272340. arXiv:2272340

    work page doi:10.2307/2272340 1974

  10. [10]

    Fine (1985): Logics containing K4

    K. Fine (1985): Logics containing K4. part II. The Journal of Symbolic Logic 50(3), doi:10.2307/2274318. arXiv:2274318

    work page doi:10.2307/2274318 1985

  11. [11]

    Kracht (1990): Internal Definability and Completeness in Modal Logic

    M. Kracht (1990): Internal Definability and Completeness in Modal Logic. Ph.D. thesis, Freie Universität Berlin

    1990

  12. [12]

    Studia Logica 85(1), pp

    A. Kudinov & I. Shapirovsky (2025): Two Types of Filtrations forwK4 and Its Relatives, doi:10.1007/s11225- 025-10207-8. arXiv:2401.00457

    work page doi:10.1007/s11225- 2025

  13. [13]

    McKinsey & A

    J.C.C. McKinsey & A. Tarski (1944): The algebra of topology. Annals of Mathematics 45(1), pp. 141–191, doi:10.2307/1969080. arXiv:1969080

    work page doi:10.2307/1969080 1944

  14. [14]

    Wolter (1993): Lattices Of Modal Logics

    F. Wolter (1993): Lattices Of Modal Logics. Ph.D. thesis, Freie Universität Berlin

    1993

  15. [15]

    Zakharyaschev (1992): Canonical Formulas for K4

    M. Zakharyaschev (1992): Canonical Formulas for K4. Part I: Basic Results. The Journal of Symbolic Logic 57(4), pp. 1377–1402, doi:10.2307/2275372. arXiv:2275372

    work page doi:10.2307/2275372 1992

  16. [16]

    Zakharyaschev (1996): Canonical Formulas for K4

    M. Zakharyaschev (1996): Canonical Formulas for K4. Part II: Cofinal Subframe Logics. The Journal of Symbolic Logic 61(2), pp. 421–449, doi:10.2307/2275669. arXiv:2275669

    work page doi:10.2307/2275669 1996

  17. [17]

    Zakharyaschev (1997): Canonical Formulas for K4

    M. Zakharyaschev (1997): Canonical Formulas for K4. Part III: The Finite Model Property. The Journal of Symbolic Logic 62(3), pp. 950–975, doi:10.2307/2275581. arXiv:2275581

    work page doi:10.2307/2275581 1997