In studies of bundled modalities, we encode a complex conceptual notion into the semantics of a single modal operator and study its logic. Although there is already a substantial body of work on various concrete bundled operators, we still lack a general understanding of them. In this paper, we provide a general theory of the expressivity and axiomatization of bundled modalities. We offer a uniform way to define bisimulations for arbitrary bundled modalities and justify our definition by the corresponding Hennessy-Milner property. We also define a special class of bundled modalities called positive-negative-independent bundles. This class of bundles, together with their duals, cover most bundled modalities studied in the literature, and their axiomatizations can be done with the help of a more abstract notion of convex neighborhood semantics and corresponding representation results. As case studies, we axiomatize the "someone knows" bundle a∈A a φ over S5-models, the "disagreement within group" bundle a, b∈A a φ ∧ b ¬φ over KD45-models, and the "belief without knowledge" bundle Bφ ∧ ¬Kφ over S4. 2-models. * The authors thank three anonymous referees for their helpful comments, and also the audience at the workshop "Bundles in Logic" at Lorentz Center. Definition 2. 2 (Kripke Models). A Kripke model is a triple M = (W, R a a∈A, V), where W = / 0 is the set of worlds; for each a ∈ A, R a is a (ρ (a) + 1) -ary relation on W and in particular, R ι n = w∈W w n+1 ; and V is a valuation function from P to ℘ (W). For w ∈ W and a ∈ A, we use R a (w) to denoteThe structures of the bundles are expressed by the following bundle terms, which are essentially formulas of a polyadic modal language with only one propositional letter in negation normal form (where (+) is the only propositional letter, and (-) is its negation): Definition 2. 3 (Bundle Terms). Terms in T A are defined recursively as follows: τ: : = (+) | (-) | ∇ a (τ,. . . , τ ρ (a) -many) | ∆ a (τ,. . . , τ ρ (a) -many) (where a ∈ A). As usual, when ρ (a) = 1, we may use a τ and a τ to denote ∇ a (τ) and ∆ a (τ), respectively. Note that Boolean connectives are not included as primitive components in our definition of bundle terms: this is because they can be viewed as modalities corresponding to the ι n 's. For example, binary disjunction and conjunction can be viewed as ∇ ι 2 and ∆ ι 2, respectively. 2 Then, for any bundle term τ, we define the corresponding bundled semantics for L as follows. Definition 2. 4 (Bundled Semantics). Let M = (W, R a a∈A, V) be a Kripke model. First, for any w ∈ W and X ⊆ W, we define the following satisfaction relation for terms inThen, for any τ ∈ T A, w ∈ W and φ ∈ L, the satisfaction relation τ for τ is defined recursively as follows (Boolean cases are omitted, andIntuitively, we "unzip" the modal structure encoded by τ when we compute the truth value of φ. This formalizes the usual way in which semantics of bundled modalities are defined. Note that since R ι 2 = (w, w, w) | w ∈ W, M, w, X ∇ ι 2 (τ 0, τ 1) iff (M, w, X τ 0) ∨ (M, w, X τ 1), while M, w, X ∆ ι 2 (τ 0, τ 1) iff (M, w, X τ 0) ∧ (M, w, X τ 1), so ∇ ι 2 and ∆ ι 2 can be safely viewed as ∨ and ∧. For the sake of readability, we shall directly write ∨ and ∧ rather than ∇ ι 2 and ∆ ι 2 from now on. As a concrete example, if we want to give φ the non-contingency semantics, we may take some a ∈ A s. t. ρ (a) = 1, and let τ △ = a (+) ∨ a (-). Then, it is not hard to see that M, w τ △ φ iff (∀v ∈ R a (w) M, v τ △ φ) ∨ (∀v ∈ R a (w) M, v τ △ φ), as intended.
Ding et al. (Sun,) studied this question.