The ILM.4 characterization conjecture for the frame $\widetilde{\mathfrak{G}_1^{\bullet}}$

Let $\widetilde{\mathfrak{G}_1^{\bullet}}$ be the frame whose validity on the closed fragment $\mathcal{F}_1$ characterizes provability in ${\mathrm{PRA}}$, and let $\mathcal{L}(\widetilde{\mathfrak{G}_1^{\bullet}})$ denote its associated logic. Let $\textbf{ILM.4}$ be the logic obtained by joining $\textbf{ILM}$ and $\textbf{GL.4}$. ILM.4 characterization conjecture.

$$\mathcal{L}(\widetilde{\mathfrak{G}_1^{\bullet}})=\textbf{ILM.4}$$

The conjecture proposes an axiomatic characterization of the logic determined by this frame, building on the known equivalence between validity on the frame, provability in ${\mathrm{PRA}}$, and derivability in $\mathbf{PIL}$ for formulas in $\mathcal{F}_1$.