Definition 1.4.14 (Kripke model). Let $P$ be a set of primitive propositions. A Kripke model is a tuple $(S,\le ,⊩)$ where $(S,\le )$ is a poset (whose elements are called “worlds” or “states”, and whose ordering is called the “accessibility relation”) and $⊩\subseteq S\times P$ is a binary relation (“forcing”) satisfying the persistence property: if $p\in P$ is such that $s⊩p$ and $s\le s^{\prime }$, then $s^{\prime }⊩p$.