we have $M,\nu \models {\Phi}$ iff $M,\nu \models {\Phi}'$.

Let us identify two important fragments of MSO logic: *First-order* () formulas do not make use of second-order quantification (however, they may contain formulas $x \in X$). Moreover, *existential* MSO (${\textup{EMSO}}$) formulas are of the form $\exists X_1 \ldots \exists X_n.{\Phi}$ with ${\Phi}\in {\textup{FO}}$.

Let ${\mathcal{F}}$ be ${\textup{MSO}}$ or ${\textup{EMSO}}$ or ${\textup{FO}}$ and let $R
\subseteq\{{\rightarrow},{\lhd},\le\}$. We obtain the logic ${\mathcal{F}}[{R}]$ by restricting ${\mathcal{F}}$ to formulas that do not make use of $\{{\rightarrow},{\lhd},\le\}
\setminus {R}$. Note that ${\mathcal{F}}= {\mathcal{F}}[{\rightarrow},{\lhd},\le]$. Moreover, we let ${\mathcal{L}}({\mathcal{F}}[R]) {:=}\{{\mathbb{L}}({\Phi}) \mid {\Phi}\in {\mathcal{F}}[R]$ is a sentence$\}$.

Since the reflexive transitive closure of an MSO-definable binary relation is MSO-definable, ${\textup{MSO}}$ and ${\textup{MSO}}[{\rightarrow},{\lhd}]$ have the same expressive power: ${\mathcal{L}}({\textup{MSO}}[{\rightarrow},{\lhd},\leq])={\mathcal{L}}({\textup{MSO}}[{\rightarrow},{\lhd}])$. However, ${\textup{MSO}}[\le]$ (without the message relation) is strictly weaker than ${\textup{MSO}}$ [@BolligJournal].

We give an FO formula that allows us to recover, at some event $f$, the most recent event $e$ that happened in the past on, say, process $p$. More precisely, we define the predicate $\mathit{latest}_p(x,y)$ as $x \le y \wedge
  p(x) \wedge \forall z\bigl((z \le y \wedge p(z)) \implies z \le x\bigr)$. The “gossip language” says that process $q$ always maintains the latest information that it can have 