Davide Grossi edited untitled.tex  about 8 years ago

Commit id: f21a85cd8929c67c64e0532e2f452236be49080d

deletions | additions      

       

\Model, a \models \dia{p} \phi & \IFF a \in \{ b \mid \exists c: b R_p c \ \& \ c \in \true{\phi}_\Model \} \\  \Model, a \models \mu p. \phi(p) & \IFF a \in \bigcap \{ X \in 2^A \mid \true{\phi}_{\Model[p:=X]} \subseteq X \}  \end{align*}  where $\true{\phi}_{\Model[p:=X]}$ denotes the truth-set of $\phi$ once $\Val(p)$ is set to be $X$. As usual, we say that: $\phi$ is valid in a model $\M$ $\Model$  iff it is satisfied in all pointed models of $\M$, i.e., $\M $\Model  \models \phi$; $\phi$ is valid in a class of models iff it is valid in all the model in the class. \end{definition}  Intuitively, $\mu p. \phi(p)$ denotes the smallest formula $p$ such that $p \lequiv \phi(p)$.