A Characterization of Properly Displayable Atomic and Molecular Logics

We apply the general results of Ciabattoni & Ramanayake about display calculi to atomic and molecular logics. We obtain an instantiation of their "I2 acyclic" formulas in our framework. Then, we show that our versions of I2 acyclic formulas are inductive formulas in the sense of Goranko & Vakarelov, again adapted to our framework. This allows us to provide a characterization of displayable calculi extending basic atomic and molecular logics in terms of these formulas: a calculus is properly displayable iff it is sound and complete w.r.t. a class of models defined by I2 acyclic formulas. For molecular logics, connectives should be of a specific format for that theorem to apply. Then, we give examples of correspondences between structural inference rules and first-order frame properties. We also detail some of the computations that enable to transform one to the other. Afterwards, we apply our characterization theorem and we obtain proper display calculi for propositional logic. In doing so, we show how classical and standard inference rules reappear as simplifications of more general and abstract rules that stem from the display calculi of our atomic logics