The birth of a new principle: P₀

When the research to the modal completeness of $\mathit{ILM_0}$ was renewed by the author, it was suggested that $\mathit{ILM_0}$ might be modally incomplete. Certainly this would not be the first modally incomplete principle. Albert Visser tried to strengthen the frame condition of $\mathit{ILM_0}$ to arrive at a stronger principle. The frame condition of $\mathit{ILM_0}$ is:

$$x_0Rx_1Rx_2S_{x_0}yRy' \rightarrow x_1Ry'.$$

Instead of demanding an R-relation between x₁ and y', one can demand an S_x1-relation between x₂ and y'. As we have x₂S_x1y', we must also have x₁Ry', so indeed the frame condition is hereby strengthened. The corresponding principle is readily found and baptized with the lyrical name of P₀.

$$P_0\ : \ \ A \rhd \Diamond B \rightarrow \Box ( A \rhd B ).$$

At first M₁ was suggested as a name, but at second thought P₀seemed to be more appropriate. The reason is given below. As P₀turns out to be an arithmetically valid principle one is obliged to subject it to a modal and comparative analysis. The target logic is the interpretability logic of all reasonable arithmetical theories, abbreviated $\mathit{GIL}$. As P₀ is a new generally valid principle, it brings us one step closer to $\mathit{GIL}$.