I'm working through Blackburn et al.'s monograph Modal Logic and have a hard time grasping exactly what the authors mean by a rooted model.
First some definitions, which for simplicity's sake will be given for the case of the basic modal language (just one diamond). Model $\mathcal{M} =(W, R , V)$ is a generated submodel of model $\mathcal{M'} =(W', R', V')$, if (1)$~\mathcal{M}$ is a submodel of $\mathcal{M'}$, that is
\begin{equation*}
W \subseteq W', R = R' \cap W^2, V(p)= V'(p) \cap W,
\end{equation*}
for all atoms $p$ and (2)$~W$ is upwards closed under $R'$, that is
\begin{equation*}
w \in W \wedge R'wv \Rightarrow v \in W
\end{equation*}
According to the book, for every model $\mathcal{M}$ and every non-empty $X \subseteq W$ there exists the submodel generated by $X$, i.e. the smallest generated submodel of $\mathcal{M}$ whose domain extends $X$. For $X$ a singleton this is called a rooted submodel of $\mathcal{M}$.
I initially thought that for given $\mathcal{M}$ and subset $X$ the submodel generated by $X$ is the intersection of all the generated submodels of $M$ extending $X$ and the corresponding proof worked quite smoothly. But as I understand the authors, the carrier of a rooted submodel of $\mathcal{M}$ is the set $\{y \in W: x R y \}$, where $x$ is the singleton's member. However I seem unable to prove that the carrier of the intersection model I constructed is identical to that set. So in the end I'm not sure whether my intersection construction goes wrong somewhere or whether I simply do not understand its properties in enough detail. Any help would be appreciated.
Best Answer
I'm not sure what you mean by "the intersection of all the generated submodels" -- given that models are triples $(W, R, V)$, how exactly do you define intersection between them?
Informally speaking, the submodel $M$ of $M'$ generated by $X$ means we pick out some points $x$ -- these are the set $X$ -- as starting points, follow through all the points $y$ that can be reached in finitely many steps from any of the starting points $x$, until every path starting from one of the members of $X$ is walked through. Everything that none of the starting points $x \in X$ can transitively reach is cut out. The thereby obtained graph with its points and relations is the generated submodel.
In the general case for $|X|$ arbitrary, this yields the carrier set $W = \{y \in W': xR'y, \text{for } x \in X\}$. (Mind the prime on $W$ an $R$ in the defintions; we construct the submodel $M$ by restricting on $M'$, otherwise the definition becomes circular.)
In the case where $X$ is a singleton $\{x\}$, all points $y$ reachable from one of the starting points $X$ are reachable from $x$. $x$ is thus the root of the graph, and the carrier is $\{y \in W': xR'y\}$.