What is the dual of generating Boolean subalgebra by subexpressions of a modal formula?

Question

I am supposed to be answering this question rather than asking it but I really cannot figure out.

There is a variation on Stone duality linking algebraic and (descriptive) Kripke semantics for (normal only?) modal logics. On the algebraic side, we have modal algebras, i. e. pairs $(B,\Box)$ where $B$ is a Boolean algebra and $\Box$ is a multiplicative operator on it. On the Kripke side we have descriptive Kripke frames, i. e. pairs $(X,R)$ where $X$ is a Stone space and $R$ is a binary relation on $X$ such that $R^{-1}C$ is clopen for any clopen subset $C$ of $X$.

Thanks to this duality there is a whole exciting dictionary translating key concepts and facts between these two worlds. For example, free modal algebras correspond to canonical models, inducing modalities on finite subalgebras of $B$ correspond to inducing relations on finite continuous images of $X$, etc.

There is one really important construction though "on the left" which I have problems translating "to the right side". One frequently needs the following: given an instantiation $\varphi(b_1,...,b_n)$ of a modal formula in $(B,\Box)$, generate finite Boolean subalgebra of $B$ by values of subexpressions of $\varphi$. Although this sounds very syntactic, it can be also made more algebraically flavored: you seek a smallest finite Boolean subalgebra containing the $b_i$ and endowed with a modality (but not necessarily modal subalgebra) in such a way that $\varphi(b_1,...,b_n)$ computed in that subalgebra is the same.

My question is whether there is some recognizable construct on descriptive frames that is dual to the above?

My attempts did not go very far. Clearly specifying $b_1,...,b_n$ means a homomorphism from the free $n$-generated modal algebra to $B$, so dually the initial data consist of an $n$-model, i. e. a p-morphism $\pi:X\to\mathscr K(n)$ from $X$ to the $n$-canonical model, together with a specified clopen $C_\varphi$ of $\mathscr K(n)$ which then produces a clopen $C=\pi^{-1}C_\varphi$ of $X$. From that data we seemingly must produce continuous $R$-preserving map (but not necessarily a p-morphism) from $X$ to some finite Kripke frame $F$ and a p-morphism (?) from $F$ to $\mathscr K(n)$ which factor $\pi$ and give the same $C$, but I am not sure.

Update

After discussing the answer below, it now seems that the question reduces to the following.

Let $\mathscr F(n)$ be the free modal algebra on specified free generators $p_1,...,p_n$, and let $\mathscr K(n)$ be its dual (canonical model). Then for any $\varphi(p_1,...,p_n)\in\mathscr F(n)$ we get a uniquely determined finite Boolean subalgebra $B_\varphi\subseteq\mathscr F(n)$ generated by all subexpressions of $\varphi$. Dually this gives a finite quotient $\mathscr K(n)\twoheadrightarrow F_\varphi$ (not necessarily a p-morphism for any choice of $R$ on $F_\varphi$). Then one must describe this $F_\varphi$ explicitly or, even better, characterize it by some universal property.

Answer 1

Update:

If we were looking for the smallest finite Boolean subalgebra containing the $b_i$ and endowed with an arbitrary modality (but not necessarily modal subalgebra) in such a way that $\varphi(b_1,...,b_n)$ computed in that subalgebra is the same, we would get:

A finite Kripke frame $F$ together with a surjective continuous map $f:X \to F$ for which there is a p-morphism $g:F \to \mathscr{K}(n)$ such that:

$\mu gf=\mu \pi$,

and $f^{-1}(g^{-1}(C_\varphi))= \pi^{-1}(C_\varphi)=C$.

Where $\mathscr{K}_B(n)$ is the Stone space dual to the free Boolean algebra on $n$-generators and $\mu: \mathscr{K}(n) \to \mathscr{K}_B(n)$ is the continuous map dual to the homomorphism sending the generator $p_i$ of the free Boolean algebra to the generator $p_i$ of the free modal algebra.

With the following universal property: for every finite Kripke frame $F'$ and surjective continuous map $f':X \to F'$ that satisfy those properties, there is a surjective map $h: F' \to F$ such that $hf'=f$. Such a morphism $h$ is necessarily unique.

---

But this is not enough because nothing guarantees that this subalgebra contains the values of the subformulas of $\varphi$.

Without loss of generality we can assume that $\varphi$ contains only the operator $\Diamond$. What we want is that if $\psi_1, \ldots, \psi_k$ are the subformulas of $\varphi$ such that $\Diamond \psi_i$ is still a subformula of $\varphi$ then $\Diamond$ in the subalgebra coincides with $\Diamond$ in $B$ on the values of the $\psi_i$'s.

Which can be dually translated by asking that for all $i=1, \ldots, k$:

$f^{-1}(g^{-1}( R^{-1}( C_{\psi_i})))= \pi^{-1}(R^{-1}( C_{\psi_i}))$

where $C_{\psi_i}$ is the clopen of $\mathscr{K}(n)$ corresponding to $\psi_i$. Note that $\pi^{-1}(R^{-1}( C_{\psi_i}))=R^{-1}( \pi^{-1}(C_{\psi_i}))$ because $\pi$ is a p-morphism.

---

I think you are right in saying that we can just restrict to the case $B=\mathscr{K}(n)$. So in that case we would get:

A finite Kripke frame $F$ together with a surjective continuous map $f:\mathscr{K}(n) \to F$ for which there is a p-morphism $g:F \to \mathscr{K}(n)$ such that:

$\mu gf=\mu$,

$f^{-1}(g^{-1}(C_\varphi))= C_\varphi$,

and $f^{-1}(g^{-1}( R^{-1}( C_{\psi_i})))= R^{-1}( C_{\psi_i})$

for all $i=1, \ldots, k$. Where $\mathscr{K}_B(n)$ is the Stone space dual to the free Boolean algebra on $n$-generators and $\mu: \mathscr{K}(n) \to \mathscr{K}_B(n)$ is the continuous map dual to the homomorphism sending the generator $p_i$ of the free Boolean algebra to the generator $p_i$ of the free modal algebra.

With the following universal property: for every finite Kripke frame $F'$ and surjective continuous map $f':\mathscr{K}(n) \to F'$ that satisfy those properties, there is a surjective map $h: F' \to F$ such that $hf'=f$. Such a map $h$ is necessarily unique.

---

I feel this is still not a satisfactory answer because the construction is too convoluted and too syntactic.