Kripke frame, lattice and some intermediate logics

Question

For a given finite and rooted intuitionistic Kripke frame $\mathcal{F}$, let $\log(\mathcal{F})=\{\phi : \mathcal{F}\vDash \phi\}$ and assume $S=\{\log(\mathcal{F}): \mathcal{F} \text{ is finite and rooted}\}$.

Is it possible for elements in $S$ to form a lattice under the inclusion relation?

For different $\mathcal{F}_1$ and $\mathcal{F}_2$ and there is no $p$-morphism between them, the product is included in $\log(\mathcal{F}_1)\cap \log(\mathcal{F}_2)$. Under what circumstances does $\log(\mathcal{F}_1\times \mathcal{F}_2)=\log(\mathcal{F}_1)\wedge \log(\mathcal{F}_2)$?

Answer 1

The set $T=\{\log(\def\F{\mathcal F}\F):\text{$\F$ is finite}\}$ of tabular logics is a filter in the (complete, Heyting) lattice $\DeclareMathOperator\Ext{Ext}\def\I{\mathbf{Int}}\Ext\I$ of superintuitionistic logics, and therefore a sublattice. (In fact, it consists of those elements of $\Ext\I$ that only have finitely many elements above them.)

$S$ is the set of meet-irreducible elements of $T$, and therefore it would be a minor miracle if it were a lattice itself. The poset of meet-irreducible elements of a distributive lattice does not in general have any useful structure (e.g., any finite poset arises that way).

For a specific counterexample, let $\F_1$ be the $3$-element chain, $\F_2$ the $3$-element fork, $\F_3$ the $4$-element $Y$-shaped frame, and $\F_4$ the $4$-element tree whose root has two immediate successors. Then $$\log(\F_3)\cup\log(\F_4)\subseteq\log(\F_1)\cap\log(\F_2),$$ but there is no rooted $\F$ such that $$\log(\F_3)\cup\log(\F_4)\subseteq\log(\F)\subseteq\log(\F_1)\cap\log(\F_2).$$ (Any such $\F$ has to be a p-morphic image of rooted subframes of both $\F_3$ and $\F_4$, and it can’t be $\F_3$ or $\F_4$ itself as they are not p-morphic images of each other, hence $|\F|\le3$. On the other hand, since $\F_1$ and $\F_2$ are p-morphic images of rooted subframes of $\F$, a similar argument gives $|\F|\ge4$, a contradiction.)

Thus, in $S$, $\log(\F_1)$ and $\log(\F_2)$ have no meet, and $\log(\F_3)$ and $\log(\F_4)$ have no join.

Assuming $\F_1\times\F_2$ denotes the Cartesian product, $\log(\F_1\times\F_2)$ is never the meet of $\log(\F_1)$ and $\log(\F_2)$ unless one of the frames is trivial, as it is too large. Let $\F$ denote the disjoint sum of $\F_1$ and $\F_2$ endowed with an extra root. Then $\log(\F)\subseteq\log(\F_1)\cap\log(\F_2)$, but if it were the case that $\log(\F)\subseteq\log(\F_1\times\F_2)$, then $|\F|=|\F_1|+|\F_2|+1\ge|\F_1|\,|\F_2|=|\F_1\times\F_2|$, i.e., $(|\F_1|-1)(|\F_2|-1)\le2$, i.e., either one of the frames is trivial, or one frame (say, $\F_1$) has size $2$, and the other ($\F_2$) size $2$ or $3$. In the latter case, $\F_1$ ia a p-morphic image of $\F_2$, hence $\log(\F_1\times\F_2)$ doesn’t equal $\log(\F_1)\cap\log(\F_2)=\log(\F_2)$ either as $|\F_1|\,|\F_2|>|\F_2|$.

Products are structurally the wrong thing to look at; the meet in the lattice should correspond to coproduct of frames (which is dual to product of Heyting algebras), i.e., disjoint sum. But the latter does not exist in $S$ due to the restriction to rooted frames.