How do I notate this statement about a state of affairs (similar to a possible world)? I'd like to notate this statement formally:
If any given agent desires that a certain state of affairs obtains, then there is no state of affairs in which she enjoys greater security than that one.
$ \forall{a}\forall s_1 \in S (\mathbf{D_a}Os_{1} \rightarrow \neg \exists s_2 \in S...) $
In the ellipsis, I want to express 'such that the security, $c$, of $a$, in $s_{2}$ is greater than the $c$ of $a$ in $s_1$, although I don't know how to represent that notationally. 
How might I notate this? Even speculative answers would help. 
Thank you. 
-Hal
 A: 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 < \subseteq L \times L$ is the "ordering on levels of security".

The guiding principles in writing these things are: 


*

*Represent booleans as relation symbols;

*Represent properties and mappings as function symbols.


It is often easier to use many-sorted expressions (in this case, we have the "sorts" $A, S, L$) to represent these things. Otherwise, you will have to tire yourself with unary predicates "$x$ is an actor", "$x$ is a state of affairs", etcetera, which only serve to obscure what you're trying to express. (But do note that conventional model theory usually assumes a single-sorted universe, so it might be useful to make this transition if you want to apply model-theoretic results.)
