# Modal formula connectives unraveling

I've been reading lately Model Theory of Modal Logic by Otto and Goranko. At one point, I found something like this:

"Let $\varphi$ be a modal formula with modal depth of $n+1$. Propositional connectives in $\varphi$ can be unravelled so that without loss of generality $\varphi$ is of the form $\diamond\psi$ for some $\psi$ with modal depth equal to $n$."

Does anyone know how to prove this?

• Usually the trick for such syntactic claims is to use some inductive algorithm on the structure of the formula using dualities. Could you clarify what other connectives you are using in your syntax? – Agnishom Chattopadhyay Jun 30 '18 at 9:04
• I'm talking about formulas of basic modal logic, formed inductively using propositional letters, diamond $\diamond$ and boolean connectives – Martin Jun 30 '18 at 10:25
• When speaking about dualities, this problems reminds me of deriving prenex normal form for some first order formula – Martin Jun 30 '18 at 10:28
• I think that they mean that $\varphi$ can be presented as a $combination$ of propositional variables and formulas $\diamond \psi$. Then we apply the Induction Hypothesis. See Modal Logic by Blackburn, de Rijke, and Venema (Proposition 2.29). – Charles Bronson Jul 2 '18 at 12:16