A General Theory of Propositional Modal Bundled Modalities

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.