# Tag Info

I would go for something like this (assuming we have a set of actors $A$, a set of states $S$, and a set of levels of security $L$): $$\forall a \in A \forall s \in S( aDs \to \neg \exists s'\in S (c(a,s') > c(a,s))$$ where $D \subseteq A \times S$ is the "desires" relation, $c: A \times S \to L$ is the "level of security function" and $\mathord < ... 0 It might be helpful to look at this as (a formula version of) modus ponens under possibility: it would say that if it's possible that$p\to q$and it's possible that$p$, then it's possible that$q$. But the two hypothetical possibilities could be incompatible with each other, right? What we'd need is for it to be possible that ($p\to q$and$p$), which is ... 1 No it isn't valid in$\text K$. Here's a Kripke semantics countermodel:$W=\{ w_{0},w_{1} \},\; R=\{(w_{0},w_{0}), (w_{0},w_{1}) \} ,\; \nu_{w_{0}}(p)=1,\nu_{w_{0}}(q)=0, \; \nu_{w_{1}}(p)=\nu_{w_{1}}(q)=0. $Will you be fine with checking it yourself? 3 No, it's reasonably easy to think of a model where it is not true that the possibility of the implication implies the implication of the possibilities. Take any model where$\Diamond \neg p, \Diamond p, \Box \neg q$hold. You can show both that$\Diamond (p\to q)$and that$\neg (\Diamond p\to \Diamond q)$are true there in. Thus$\Diamond(p\to ...
Yes, so far so good. The rule is better put schematically rather than by using propositional atoms, i.e. the rule is $$\diamond(\alpha \lor \beta) \equiv (\diamond\alpha \lor \diamond\beta) \text{ for all wffs }\alpha, \beta$$ This makes it clear the rule applies generally, not just to propositional atoms, as perhaps using $p, q$ misleading suggests.