Modalities in non-classical variations of $\mathsf{S4}$

Leonardo Pacheco

Source-linked AI summary

Modalities in non-classical variations of $\mathsf{S4}$

Leonardo Pacheco

arXiv:2609.00736v1Sep 1, 2026math.LOcs.LO

TL;DR

The paper asks how the classical 14-modality result changes for four non-classical variants of S4. It develops modality-equivalence results across these logics and finds contrasting finite and infinite cases. These results also bear on the difficulty of finite-model-property proofs.

Problem
The paper addresses the lack of modality results for intuitionistic modal logics using both boxes and diamonds.
Source: §1 · p. 1, §2 · p. 5
Method
The paper compares modality equivalence over birelational semantics for CS4, IS4, GS4, and GS4c.
Source: §2 · pp. 3, 5
Results
CS4 has infinitely many {¬, ♢}-modalities; IS4 and GS4 have infinitely many {¬, □, ♢}-modalities; GS4c has finitely many {¬, □, ♢}-modalities.
Source: §1 · p. 1
Takeaways & Limitations
The modality patterns provide an explanation for why finite-model-property proofs for these logics are difficult.
Source: §1 · p. 1
Further work is constrained by the lack of established semantics for most logics in the constructive modal cube.
Source: §6 · p. 11

Abstract

from arXiv · show

A classical result in modal logic states that $\mathsf{S4}$ has $14$ modalities, that is, every sequence of negations, boxes, and diamonds is equivalent to one in a set of $14$ such sequences. We study analogous results for the non-classical analogues $\mathsf{CS4}$, $\mathsf{IS4}$, $\mathsf{GS4}$, and $\mathsf{GS4^c}$ of $\mathsf{S4}$. First, we show that, while all these logics have finitely many $\{\Box,\Diamond\}$- and $\{\neg,\Box\}$-modalities, the logic $\mathsf{CS4}$ has infinitely many $\{\neg,\Diamond\}$-modalities. Second, we show that $\mathsf{IS4}$ and $\mathsf{GS4}$ have finitely many $\{\neg,\Diamond\}$-modalities, but they have infinitely many $\{\neg,\Box,\Diamond\}$-modalities. At last, we show that $\mathsf{GS4^c}$ has finitely many $\{\neg,\Box,\Diamond\}$-modalities.

1 Introduction

The paper extends the classical study of finitely many modalities to four non-classical variations of S4. It establishes distinct finite and infinite modality patterns and relates them to difficulties in finite-model-property proofs.

14 modalities suffice over classical S4 for sequences of negations, boxes, and diamonds.Source: §1 · p. 1
The paper proves and refutes analogous finite-modality results for CS4, IS4, GS4, and GS4c.Source: §1 · p. 1
CS4 has finite {□, ♢}- and {¬, □}-modalities but infinitely many {¬, ♢}-modalities.Source: §1 · p. 1
IS4 and GS4 have finite {¬, ♢}-modalities but infinitely many {¬, □, ♢}-modalities.Source: §1 · p. 1
GS4c has finitely many {¬, □, ♢}-modalities.Source: §1 · p. 1
These modality results help explain why finite-model-property proofs are difficult for the four logics, including complicated filtration methods and a published mistake for IS4.Source: §1 · p. 1

2 Preliminaries

The preliminaries define intuitionistic modal syntax, birelational semantics, the four model classes, and modality equivalence. They establish the semantic framework and a monotonicity principle used to compare finite-modality results across logics.

Syntax

In intuitionistic modal logic, □ and ♢ are not interdefinable, and formulas are generated from ⊥, propositions, connectives, □, and ♢.Source: §2 · p. 2
Negation is defined as φ → ⊥, while a logic is closed under necessitation and modus ponens.Source: §2 · p. 2

Birelational semantics

A birelational CS4-model uses possible worlds, a distinguished subset, two relations, and a valuation satisfying upset and confluence conditions.Source: §2 · p. 3
Formula forcing is intuitionistic for implication, while □ quantifies over worlds reached through ⪯ then ⊑ and ♢ requires suitable ⊑-successors for every ⪯-extension.Source: §2 · pp. 3–4

Semantic properties

Every formula's truth set is a ⪯-upset, and all four logics are sound and strongly complete for their birelational model classes.Source: §2 · pp. 4–5

Confluence

Forward confluence simplifies ♢ to existential reachability along ⊑, whereas downward confluence simplifies □ to universal quantification along ⊑.Source: §2 · p. 4

Model classes

IS4 models are forward and backward confluent; GS4 models are locally linear IS4 models; GS4c models additionally satisfy downward confluence.Source: §2 · pp. 4–5

Modalities

An X-modality is a finite sequence from X, and finitely many modalities means every such sequence is equivalent to one in a finite representative set.Source: §2 · p. 5

3 The case for CS4

The CS4 analysis proves finite modality results for boxes and negation with boxes, then constructs a CS4-model showing infinitely many negation-diamond modalities.

CS4 reductions involving negations and boxes are derived using intuitionistic tautologies together with axioms 4 and T.These derivations include equivalences such as □¬¬□¬φ ↔ □¬φ and □¬□¬□¬□¬φ ↔ □¬□¬φ.Source: §3 · pp. 5–6
CS4 has finitely many {□, ♢}- and {¬, □}-modalities.Source: §3 · p. 6
The constructed structure M CS4 ∞ is a CS4-model.Its preorders and valuation satisfy the model conditions, with backward confluence established separately.Source: §3 · p. 6
For every n ∈ω, the modality (¬♢)n defines exactly the worlds in M CS4 ∞ at level n + 1.The proof proceeds by induction on n and separates the truth sets for different levels.Source: §3 · pp. 6–7
The modalities {(¬♢)n | n ∈ω} are pairwise non-equivalent over CS4.The model therefore supplies infinitely many distinct {¬, ♢}-modalities.Source: §3 · p. 7

4 The case for IS4 and GS4

IS4 has finitely many {¬, ♢}-modalities, whereas GS4 has infinitely many {¬, □, ♢}-modalities. The GS4 result is witnessed by a model distinguishing an infinite sequence of iterated modalities.

IS4

IS4 has finitely many {¬, ♢}-modalities.Source: §4 · p. 8

GS4

The GS4 proof constructs a model M GS4 ∞ that is a GS4-model.Source: §4 · p. 8
The model distinguishes successive iterations by expanding the truth set with additional ci worlds at each step.Source: §4 · p. 9
The modalities {(♢¬¬□)n+1 | n ∈ω} are pairwise non-equivalent over GS4.Source: §4 · p. 9
GS4 has infinitely many {¬, □, ♢}-modalities.Source: §4 · p. 9

5 The case for GS4c

GS4c has finitely many {¬, □, ♢}-modalities. The proof uses up-downset properties to make boxes and diamonds essentially dual, then bounds the total by 105 modalities.

Negated formulas denote ⪯-updownsets in GS4c-models.Source: §5 · p. 9
When ∥φ∥ is a ⪯-updownset, both ∥□φ∥ and ∥♢φ∥ are also ⪯-updownsets.Source: §5 · pp. 9–10
Under these conditions, □¬φ is equivalent to ¬♢φ, and ♢¬φ is equivalent to ¬□φ.Source: §5 · p. 10
GS4c has finitely many {¬, □, ♢}-modalities.Source: §5 · p. 10
105 is an upper bound on the number of {¬, □, ♢}-modalities in GS4c.Source: §5 · p. 10

6 Conclusion

The paper shows that modality finiteness becomes more complicated in intuitionistic variations of S4 than in classical S4. It identifies constructive semantics as a main obstacle for extending the analysis to other logics.

Classical S4 has finitely many {¬, □, ♢}-modalities, while the studied intuitionistic variations have more complicated behavior.Source: §6 · p. 10
A future direction is to analyze analogous modality questions for other non-classical modal logics.Source: §6 · p. 10
The main roadblock is that most logics in the constructive modal cube lack published semantics, having only proof systems.Source: §6 · p. 11
Another future direction is studying S4 variations based on non-classical propositional logics other than intuitionistic logic.Source: §6 · p. 11