deletions | additions       diff --git a/section_Fixpoint_Logics_for_Boolean__.tex b/section_Fixpoint_Logics_for_Boolean__.tex  index c15a1de..9f61b35 100644  --- a/section_Fixpoint_Logics_for_Boolean__.tex  +++ b/section_Fixpoint_Logics_for_Boolean__.tex 
...
The language of the $\mu$-calculus expands the basic modal language with a least fixpoint operator $\mu$. Here is the BNF of the language:  \[  \L^\mu}: \L^\mu:  \phi ::= p \mid \bot \mid \neg \phi \mid \phi \land \phi \mid \dia{p} \phi \mid \mu p. \phi(p) \]  where $p$ ranges over $\Atoms$ and $\phi(p)$ indicates that $p$ occurs free in $\phi$ (i.e., it is not bounded by fixpoint operators) and under an even number of negations.\footnote{This syntactic restriction guarantees that every formula $\phi(p)$ defines a set transformation which preserves $\subseteq$, which in turn guarantees the existence of least and greatest fixpoints by the Knaster-Tarski fixpoint theorem (cf. \cite{Stirling_2001}).} In general, the notation $\phi(\psi)$ stands for $\psi$ occurs in $\phi$. The usual definitions for Boolean and modal operators apply. Intuitively, $\mu p. \phi(p)$ denotes the smallest formula $p$ such that $p \lequiv \phi(p)$. The greatest fixpoint operator $\nu$ can be defined from $\mu$ as follows: $\nu p. \phi(p) := \neg \mu p. \neg \phi( \neg p)$.