deletions | additions       diff --git a/section_Fixpoint_Logics_for_Boolean__.tex b/section_Fixpoint_Logics_for_Boolean__.tex  index 1ef3283..0a55538 100644  --- a/section_Fixpoint_Logics_for_Boolean__.tex  +++ b/section_Fixpoint_Logics_for_Boolean__.tex 
...
\Model, a \models \ldia{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 $\O(p)$ is set to be $X$. As usual, we say that: $\phi$ is valid in a model $\Model$ iff it is satisfied in all points of $\Model$, i.e., $\Model \models \phi$; $\phi$ is valid in a class of models iff it is valid in all the model models  in the class. \end{definition}  Intuitively, $\mu p. \phi(p)$ denotes the smallest formula $p$ such that $p \lequiv \phi(p)$.