A General Theory of Propositional Modal Bundled Modalities

1. Problem Statement

The field of modal logic has seen a proliferation of "bundled modalities"—operators that encode complex conceptual notions (e.g., "someone knows," "false belief," "disagreement") into a single primitive modal operator. While specific logics for individual bundled operators have been studied extensively, there is a lack of a unified general theory covering:

• Expressivity: How to uniformly define bisimulations for arbitrary bundled modalities to characterize their expressive power.
• Axiomatization: How to systematically derive complete axiomatizations for these logics, as current methods (like the "almost-definability" schema) are often ad hoc or restricted to specific classes.

Existing approaches struggle with the diversity of bundle structures, leading to fragmented research where bisimulations are often left as open problems and canonical models are constructed using radically different techniques for similar logics.

2. Methodology

The authors propose a unified framework based on neighborhood semantics and convexity.

A. Uniform Semantics and Bisimulations

• Bundle Terms: The authors define a formal language of "bundle terms" ($\tau$) using positive ($\nabla$) and negative ($\Delta$) modal operators over a set of indices. This allows any bundled modality to be viewed as a specific semantic interpretation of a single operator $\#$.
• Generated Neighborhoods: They treat bundled semantics as a special form of neighborhood semantics. For a given model and bundle term, they define a "generated neighborhood" function ($Nbh_M$) which maps a world to a set of pairs $(X, Y)$, representing minimal sets of worlds where a formula must be true ($X$) and false ($Y$) for the bundled modality to hold.
• Uniform Bisimulation: Using these neighborhoods, they define a $\tau$-bisimulation. Two worlds are bisimilar if they satisfy the same atomic propositions and their generated neighborhoods are "coherent" (i.e., they agree on which subsets of the domain are valid truth/falsity witnesses).
• Hennessy-Milner Property: They prove that for image-finite models, logical equivalence ($\equiv_\tau$) coincides with $\tau$-bisimilarity ($\leftrightarrow_\tau$), establishing that the defined bisimulation correctly captures the expressivity of the logic.

B. Convex Bundles and Axiomatization

• Convexity: The authors identify a crucial class of bundles called convex bundles. A bundle is convex if its neighborhood structure satisfies a "convexity" property: if $(X_1, Y_1)$ and $(X_2, Y_2)$ are valid witnesses, and $X_1 \cap Y_2 = \emptyset$, then $(X_1, Y_2)$ is also a valid witness. This class covers most literature examples (e.g., contingency, false belief, disagreement).
• Convex Neighborhood Models: They introduce a specialized semantics using convex neighborhood frames (pairs of neighborhood functions $N^+$ and $N^-$) and core models (where $N^+$ and $N^-$ are disjoint and minimal).
• Two-Step Axiomatization Strategy:
  1. Abstract Completeness: Prove completeness for the logic over the abstract class of convex neighborhood models using a canonical model construction that naturally yields "core models."
  2. Representation: Use representation theorems to map these abstract neighborhood models back to concrete Kripke models (e.g., S5, KD45, S4.2) that satisfy the specific bundle semantics.

3. Key Contributions

1. General Theory of Bisimulations:

   • Provided the first uniform definition of bisimulations for arbitrary bundled modalities.
   • Proved the Hennessy-Milner theorem for these bisimulations, resolving open problems regarding the expressivity of various bundled logics.
   • Introduced a stronger "convex bisimulation" for convex bundles, which is more efficient (quantifying only over generated neighborhoods rather than all subsets).

2. Convex Bundle Classification:

   • Defined the syntactic class of convex bundles ($T^\times_A$) and proved that almost all known bundled modalities fall into this category or are duals of it.
   • Showed that convex bundles admit a well-behaved semantics between minimal and monotonic neighborhood logics.

3. Systematic Axiomatization:

   • Developed a general recipe for axiomatizing convex bundles using convex neighborhood semantics.
   • Introduced a set of axioms (e.g., $CONV$, $EQU$, $D\#$, $4'$, $5^{Cn}$) that correspond to specific frame properties (symmetry, seriality, introspection, etc.) in the neighborhood setting.
   • Proved that these axioms are sound and strongly complete with respect to the corresponding Kripke classes via representation theorems.

4. New Case Studies (First-time Axiomatizations):
   The paper provides the first complete axiomatizations for several specific bundled logics:

   • "Someone Knows" ($\bigvee_{a \in A} \Box_a \phi$): Axiomatized over S5-models.
   • "Disagreement in Group" ($\bigvee_{a,b \in A} \Box_a \phi \land \Box_b \neg \phi$): Axiomatized over KD45-models.
   • "Belief without Knowledge" ($\Diamond\Box\phi \land \Diamond\neg\phi$): Axiomatized over S4.2-models (and S4F-models), capturing the concept of "mere belief" or Dunning-Kruger ignorance.

4. Results

• Expressivity: The paper establishes that $\tau$-bisimilarity is the exact characterization of logical equivalence for bundled modalities on image-finite models.
• Completeness: The logic CONV (the minimal convex modal logic) is proven sound and strongly complete with respect to the class of all convex neighborhood models.
• Specific Logics: The paper successfully derives complete axiomatizations for the three case studies mentioned above, demonstrating that the general method works for complex, multi-agent, and non-normal modalities.
• Representation: The paper proves that core convex neighborhood models satisfying specific properties (like introspection and colorability) can be represented by standard Kripke models (S5, KD45, S4.2), bridging the gap between abstract semantics and concrete epistemic/doxastic models.

5. Significance

• Unification: This work moves the study of bundled modalities from a collection of isolated case studies to a cohesive general theory. It provides a "toolkit" for analyzing new bundled operators without reinventing the wheel for bisimulations or canonical models.
• Technical Advancement: By introducing convex neighborhood semantics, the authors create a middle ground that is expressive enough to handle complex bundles but structured enough to allow for standard completeness proofs (unlike general neighborhood logics which are often intractable).
• Foundational Impact: The identification of convexity as the key property for tractability suggests a new direction for modal logic research. It clarifies why certain bundled logics behave well while others do not.
• Future Directions: The paper opens avenues for Sahlqvist-style correspondence theory for convex logics and automated generation of axiomatizations, potentially leading to a comprehensive library of bundled modal logics.

In summary, Ding and Yang provide a robust theoretical foundation that unifies the semantics, bisimulation theory, and axiomatization of propositional bundled modalities, successfully applying this framework to solve long-standing open problems in epistemic and doxastic logic.