Are there atoms in the lattice of intermediate logics?

Question

A few days ago I stumbled upon this question on MS. The question is: Does the lattice of intermediate logics have an atom, i.e. an element that is strictly stronger than IPC but not strictly stronger than another logic that is itself strictly stronger than IPC? The question has not been answered on MS and I didn't find an answer in any other source too.

Thinking about the question myself I had the idea of finding a systematic way to weaken the sentences an intermediate logic includes in addition to IPC but I couldn't find any way to do so repeatedly in a way that doesn't result in either intuitionistic tautologies or additional sentences intuitionistically equivalent to the sentences I began with. I would appreciate any answer or any proposal about possible ways to go forward with solving the problem.

Answer 1

There are no atoms.

Assume for contradiction that $L$ is an atom. Since $L$ strictly contains IPC, there is a finite rooted Kripke frame $F$ that does not validate $L$, thus $L$ proves the Jankov–De Jongh frame formula for $F$, let me denote it $\beta^\sharp(F)$. Let $G$ be a finite rooted frame that properly contains $F$ as a generated subframe. Then $L\supseteq\mathsf{IPC}+\beta^\sharp(F)\supsetneq\mathsf{IPC}+\beta^\sharp(G)\supsetneq\mathsf{IPC}$. (The indicated inclusions are strict because $F$ is a model of $\mathsf{IPC}+\beta^\sharp(G)$ that does not validate $\beta^\sharp(F)$, and $G$ is a model of $\mathsf{IPC}$ that does not validate $\beta^\sharp(G)$.)