Source-linked AI summary
Modalities in non-classical variations of $\mathsf{S4}$
Leonardo Pacheco
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.
Method
The paper compares modality equivalence over birelational semantics for CS4, IS4, GS4, and GS4c.
Results
CS4 has infinitely many {¬, ♢}-modalities; IS4 and GS4 have infinitely many {¬, □, ♢}-modalities; GS4c has finitely many {¬, □, ♢}-modalities.
Takeaways & Limitations
The modality patterns provide an explanation for why finite-model-property proofs for these logics are difficult.
Takeaways & Limitations
Further work is constrained by the lack of established semantics for most logics in the constructive modal cube.
Abstract
from arXiv · showhide
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.
- The paper proves and refutes analogous finite-modality results for CS4, IS4, GS4, and GS4c.
- CS4 has finite {□, ♢}- and {¬, □}-modalities but infinitely many {¬, ♢}-modalities.
- IS4 and GS4 have finite {¬, ♢}-modalities but infinitely many {¬, □, ♢}-modalities.
- GS4c has finitely many {¬, □, ♢}-modalities.
- 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.
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 ♢.
- Syntax: Negation is defined as φ → ⊥, while a logic is closed under necessitation and modus ponens.
- Birelational semantics: A birelational CS4-model uses possible worlds, a distinguished subset, two relations, and a valuation satisfying upset and confluence conditions.
- Birelational semantics: Formula forcing is intuitionistic for implication, while □ quantifies over worlds reached through ⪯ then ⊑ and ♢ requires suitable ⊑-successors for every ⪯-extension.
- Semantic properties: Every formula's truth set is a ⪯-upset, and all four logics are sound and strongly complete for their birelational model classes.
- Confluence: Forward confluence simplifies ♢ to existential reachability along ⊑, whereas downward confluence simplifies □ to universal quantification along ⊑.
- Model classes: IS4 models are forward and backward confluent; GS4 models are locally linear IS4 models; GS4c models additionally satisfy downward confluence.
- 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.
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 □¬□¬□¬□¬φ ↔ □¬□¬φ.
- CS4 has finitely many {□, ♢}- and {¬, □}-modalities.
- The constructed structure M CS4 ∞ is a CS4-model.Its preorders and valuation satisfy the model conditions, with backward confluence established separately.
- 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.
- The modalities {(¬♢)n | n ∈ω} are pairwise non-equivalent over CS4.The model therefore supplies infinitely many distinct {¬, ♢}-modalities.
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.
- GS4: The GS4 proof constructs a model M GS4 ∞ that is a GS4-model.
- GS4: The model distinguishes successive iterations by expanding the truth set with additional ci worlds at each step.
- GS4: The modalities {(♢¬¬□)n+1 | n ∈ω} are pairwise non-equivalent over GS4.
- GS4: GS4 has infinitely many {¬, □, ♢}-modalities.
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.
- When ∥φ∥ is a ⪯-updownset, both ∥□φ∥ and ∥♢φ∥ are also ⪯-updownsets.
- Under these conditions, □¬φ is equivalent to ¬♢φ, and ♢¬φ is equivalent to ¬□φ.
- GS4c has finitely many {¬, □, ♢}-modalities.
- 105 is an upper bound on the number of {¬, □, ♢}-modalities in GS4c.
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.
- A future direction is to analyze analogous modality questions for other non-classical modal logics.
- The main roadblock is that most logics in the constructive modal cube lack published semantics, having only proof systems.
- Another future direction is studying S4 variations based on non-classical propositional logics other than intuitionistic logic.