Definition 1.4.15 (Forcing relation). Let $(S,\le ,⊩)$ be a Kripke model for a propositional language. We define the extended forcing relation inductively as follows:

• There is no $s\in S$ with $s⊩\perp$;

• $s⊩\phi \wedge \psi$ if and only if $s⊩\phi$ and $s⊩\psi$;

• $s⊩\phi \vee \psi$ if and only if $s⊩\phi$ or $s⊩\psi$;

• $s⊩(\phi \to \psi )$ if and only if $s^{\prime }⊩\phi$ implies $s^{\prime }⊩\psi$ for every $s^{\prime }\ge s$.