 A Kripke structure \(\mathbf{K}\) for \(L\) consists of a partially ordered set \(K\) of nodes and a domain function D assigning to each node \(k\) in \(K\) an inhabited set \(D(k),\) such that if \(k \le k',\) then \(D(k) \subseteq D(k').\) In addition \(\mathbf{K}\) has a forcing relation determined as follows.