On Local Finiteness of Modal K4 Algebras

Gabriel Agnew

arxiv: 2606.02941 · v1 · pith:52OFOAQPnew · submitted 2026-06-01 · 🧮 math.LO

On Local Finiteness of Modal K4 Algebras

Gabriel Agnew This is my paper

Pith reviewed 2026-06-28 11:23 UTC · model grok-4.3

classification 🧮 math.LO

keywords modal K4 algebraslocal finitenessgeneral framesfinite model propertywell-quasi-orderingstransitive relationsKripke framestunability

0 comments

The pith

A tunability condition on dual general frames is sufficient for local finiteness of modal K4 algebras, and necessary and sufficient for complex ones.

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

The paper establishes a sufficient condition for local finiteness of modal K4 algebras by identifying a structure that must be present in non-locally finite ones via the tunability of their dual general frames. This condition is shown to be both necessary and sufficient when the algebras are complex. The condition is translated into a pair of order-theoretic conditions on transitive Kripke frames to classify local finiteness of their dual modal algebras. The paper further proves that the logic of any class of well-founded transitive relations with no infinite antichains has the finite model property. As a consequence, the logic of the class of well-quasi orderings has the finite model property.

Core claim

We study local finiteness for modal K4 algebras via the tunability of their dual general frames. In particular, we provide a sufficient condition for modal K4 algebras to be locally finite by identifying a structure which must be present in non-locally finite modal K4 algebras. We then show that this condition becomes both necessary and sufficient for complex modal K4 algebras. Next, we translate this condition into a pair of order-theoretic conditions on transitive Kripke frames, providing a classification of local finiteness on their dual modal algebras. We further show that the logic of any class of well-founded transitive relations with no infinite antichains has the finite model propert

What carries the argument

Tunability of dual general frames, which detects a structure that non-locally finite modal K4 algebras must contain.

If this is right

Logics of well-founded transitive relations without infinite antichains have the finite model property.
The logic of well-quasi-orderings has the finite model property.
Local finiteness for complex modal K4 algebras is equivalent to the tunability condition on dual frames.
Transitive Kripke frames have locally finite dual algebras exactly when they meet the two order-theoretic conditions.

Where Pith is reading between the lines

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

The order-theoretic conditions might help identify new classes of frames with locally finite dual algebras.
Local finiteness could imply other properties like finite axiomatizability in related algebraic varieties.
The FMP result may extend to other modal logics whose frames satisfy similar well-foundedness conditions.

Load-bearing premise

The duality between modal K4 algebras and general frames translates the tunability condition into order-theoretic conditions on transitive Kripke frames without gaps.

What would settle it

A modal K4 algebra that violates local finiteness while its dual frame meets the tunability condition, or a class of well-founded transitive relations without infinite antichains whose associated logic lacks the finite model property.

read the original abstract

We study local finiteness for modal $K4$ algebras via the tunability of their dual general frames. In particular, we provide a sufficient condition for modal $K4$ algebras to be locally finite by identifying a structure which must be present in non-locally finite modal $K4$ algebras. We then show that this condition becomes both necessary and sufficient for complex modal $K4$ algebras. Next, we translate this condition into a pair of order-theoretic conditions on transitive Kripke frames, providing a classification of local finiteness on their dual modal algebras. We further show that the logic of any class of well-founded transitive relations with no infinite antichains has the finite model property, and conclude that the logic of the class of well-quasi orderings has the finite model property.

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.

Desk Editor's Note private letter to a colleague

The paper classifies local finiteness for modal K4 algebras via tunability and derives FMP for WQO logics, but the abstract gives no proofs to check the steps.

read the letter

The core contribution is a sufficient condition for local finiteness of modal K4 algebras based on the absence of a certain structure in their dual frames, shown to be necessary and sufficient for complex algebras, then translated into two order-theoretic conditions on transitive Kripke frames. From there it concludes that any class of well-founded transitive relations without infinite antichains has the finite model property, so in particular the logic of well-quasi-orderings does.

This is a clean chain from algebra to frames to a concrete FMP result. The order-theoretic reformulation and the WQO application look like the genuinely new pieces; they connect existing duality tools to a decidability-adjacent property in a direct way.

The main limitation is that the abstract contains no proof outlines, no examples of the forbidden structure, and no indication of how the necessity direction is obtained. Without those, it is impossible to judge whether the translation from tunability to the two frame conditions is tight or whether the FMP argument for the well-founded no-antichain case actually goes through. The duality steps are standard, but any gap there would make the later claims collapse.

The work is aimed at people who already work with algebraic semantics for modal logics and care about finiteness or decidability results. A reader who follows the K4 literature would find the classification and the WQO corollary worth seeing in full.

It is worth sending to referees. The claims are specific enough that a careful review can settle whether the arguments hold; desk rejection would be premature given the potential payoff if the details check out.

Referee Report

0 major / 3 minor

Summary. The paper studies local finiteness of modal K4 algebras by means of tunability conditions on their dual general frames. It identifies a structural obstruction to local finiteness, proves that the obstruction is necessary and sufficient for complex K4 algebras, translates the condition into order-theoretic properties of transitive Kripke frames, and deduces that the logic of any class of well-founded transitive relations without infinite antichains (in particular, the class of well-quasi-orderings) has the finite model property.

Significance. If the central claims hold, the work supplies a concrete algebraic-to-order-theoretic dictionary for local finiteness in the K4 variety and establishes FMP for an important family of modal logics, including those of WQOs. The explicit translation between tunability and the absence of infinite antichains in well-founded frames is a useful bridge between duality theory and order-theoretic model theory.

minor comments (3)

§3, Definition 3.4: the notion of 'tunability' is introduced via a universal quantification over ultrafilters; a short remark clarifying why this is equivalent to the order-theoretic formulation used later would help readers who skip the duality preliminaries.
Theorem 5.7: the statement that the logic of well-founded transitive frames without infinite antichains has FMP is proved by reducing to the complex algebra case; it would be useful to record explicitly which earlier lemma supplies the reduction.
The paper cites several standard references on K4 duality and WQO theory but omits a pointer to recent work on finite model property for well-founded modal logics (e.g., the 2022 paper by Bezhanishvili et al. on Esakia spaces).

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary and recommendation of minor revision. No major comments were provided in the report, so we have no points to address point-by-point at this stage. We will make the minor revisions as appropriate in the updated manuscript.

Circularity Check

0 steps flagged

No significant circularity in the derivation chain

full rationale

The paper's chain—from sufficient conditions on modal K4 algebras via tunability of dual frames, to necessity/sufficiency for complex algebras, translation to order-theoretic conditions on transitive frames, and FMP for well-founded transitive relations without infinite antichains (hence for WQOs)—builds on standard duality between algebras and general frames. No step reduces by construction to fitted inputs, self-definitions, or self-citation load-bearing premises; all claims are independent mathematical derivations in modal logic.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on established duality theorems in modal logic and basic facts from order theory such as properties of well-founded relations and antichains; no free parameters, new entities, or ad hoc axioms are apparent from the abstract.

axioms (2)

standard math Duality between modal K4 algebras and general frames holds and tunability can be used to characterize local finiteness.
Invoked directly in the study of local finiteness via dual general frames.
standard math Transitive Kripke frames correspond to modal K4 algebras under standard duality.
Used in translating the condition to order-theoretic properties on frames.

pith-pipeline@v0.9.1-grok · 5653 in / 1374 out tokens · 39007 ms · 2026-06-28T11:23:41.400401+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

13 extracted references · 6 canonical work pages

[1]

465–473, doi:10.1007/s00012-005-1958-5

Guram Bezhanishvili & Revaz Grigolia (2005):Locally finite varieties of Heyting algebras.Algebra Univer- salis54(4), p. 465–473, doi:10.1007/s00012-005-1958-5

work page doi:10.1007/s00012-005-1958-5 2005
[2]

Cambridge University Press, 2001

Patrick Blackburn, Maarten de Rijke & Yde Venema (2001):Modal Logic. Cambridge University Press, doi:10.1017/cbo9781107050884

work page doi:10.1017/cbo9781107050884 2001
[3]

W. J. Blok (1980):Pretabular varieties of modal algebras.Studia Logica39(2–3), p. 101–124, doi:10.1007/bf00370315

work page doi:10.1007/bf00370315 1980
[4]

Stanley Burris & H. P. Sankappanavar (1981):A course in Universal Algebra. Springer

1981
[5]

413, doi:10.2307/2370405

Leonard Eugene Dickson (1913):Finiteness of the odd perfect and primitive abundant numbers with n dis- tinct prime factors.American Journal of Mathematics35(4), p. 413, doi:10.2307/2370405

work page doi:10.2307/2370405 1913
[6]

Springer-Verlag Berlin and Heidelberg

Thomas Jech (2002):Set Theory, third millenium edition. Springer-Verlag Berlin and Heidelberg

2002
[7]

A Kuznetsov (1971):Some properties of the structure of varieties of pseudo-boolean algebras.Proceedings of the Xlth USSR Algebraic Colloquium, pp. 255–256

1971
[8]

L Maksimova (1975):Modal logics of finite slices.Algebra and Logic, pp. 304–319

1975
[9]

Krister Segerberg (1971):An essay in classical modal logic.Filosofska Studier13

1971
[10]

35:216–221

Krister Segerberg (1973):Franzen’s proof of Bull’s theorem.Ajatus, pp. 35:216–221

1973
[11]

610–618, doi:10.1007/978-3-662-59533-6_37

Ilya Shapirovsky (2019):Modal logics of finite direct powers ofωhave the finite model property.Lecture Notes in Computer Science, p. 610–618, doi:10.1007/978-3-662-59533-6_37

work page doi:10.1007/978-3-662-59533-6_37 2019
[12]

Ilya Shapirovsky & Valentin Shehtman (2016):Local tabularity without transitivity.Advances in Modal Logic11, pp. 520–534

2016
[13]

Available at https://arxiv.org/html/2509.17612

Ilya B Shapirovsky (2026):Generalizations of the Finite Height Criterion for Local Tabularity. Available at https://arxiv.org/html/2509.17612

work page arXiv 2026

[1] [1]

465–473, doi:10.1007/s00012-005-1958-5

Guram Bezhanishvili & Revaz Grigolia (2005):Locally finite varieties of Heyting algebras.Algebra Univer- salis54(4), p. 465–473, doi:10.1007/s00012-005-1958-5

work page doi:10.1007/s00012-005-1958-5 2005

[2] [2]

Cambridge University Press, 2001

Patrick Blackburn, Maarten de Rijke & Yde Venema (2001):Modal Logic. Cambridge University Press, doi:10.1017/cbo9781107050884

work page doi:10.1017/cbo9781107050884 2001

[3] [3]

W. J. Blok (1980):Pretabular varieties of modal algebras.Studia Logica39(2–3), p. 101–124, doi:10.1007/bf00370315

work page doi:10.1007/bf00370315 1980

[4] [4]

Stanley Burris & H. P. Sankappanavar (1981):A course in Universal Algebra. Springer

1981

[5] [5]

413, doi:10.2307/2370405

Leonard Eugene Dickson (1913):Finiteness of the odd perfect and primitive abundant numbers with n dis- tinct prime factors.American Journal of Mathematics35(4), p. 413, doi:10.2307/2370405

work page doi:10.2307/2370405 1913

[6] [6]

Springer-Verlag Berlin and Heidelberg

Thomas Jech (2002):Set Theory, third millenium edition. Springer-Verlag Berlin and Heidelberg

2002

[7] [7]

A Kuznetsov (1971):Some properties of the structure of varieties of pseudo-boolean algebras.Proceedings of the Xlth USSR Algebraic Colloquium, pp. 255–256

1971

[8] [8]

L Maksimova (1975):Modal logics of finite slices.Algebra and Logic, pp. 304–319

1975

[9] [9]

Krister Segerberg (1971):An essay in classical modal logic.Filosofska Studier13

1971

[10] [10]

35:216–221

Krister Segerberg (1973):Franzen’s proof of Bull’s theorem.Ajatus, pp. 35:216–221

1973

[11] [11]

610–618, doi:10.1007/978-3-662-59533-6_37

Ilya Shapirovsky (2019):Modal logics of finite direct powers ofωhave the finite model property.Lecture Notes in Computer Science, p. 610–618, doi:10.1007/978-3-662-59533-6_37

work page doi:10.1007/978-3-662-59533-6_37 2019

[12] [12]

Ilya Shapirovsky & Valentin Shehtman (2016):Local tabularity without transitivity.Advances in Modal Logic11, pp. 520–534

2016

[13] [13]

Available at https://arxiv.org/html/2509.17612

Ilya B Shapirovsky (2026):Generalizations of the Finite Height Criterion for Local Tabularity. Available at https://arxiv.org/html/2509.17612

work page arXiv 2026