I'm currently studying hyperlogics and in particular HyperLTL/CTL*. In model checking algorithms for such logics the number of quantifier alternations appearing in a formula can play an important role regarding the complexity of the algo.
Working on better algorithms, a question came up which is actually more general:
Let $\phi$ be a first order logic formula in negation normal form. Further let $\alpha(\psi)=k$ be the alternation depth of $\phi$, i.e. the maximal number of quantifier alternations in a branch of the formulas structure tree. What is the smallest number of quantifier alternation we can obtain for a prenex form $\psi^*$ of $\psi$? Is there an algorithm to constuct a prenex formula for which the lower bound holds?
I did not fnd the question anywhere yet. I'm quit sure the answere should be that $\alpha(\psi^*)\leq\alpha(\psi)+1$ is always possible.
But I can't proof it. I can't find the right induction hypothesis. I tried some kind of double induction over the structure of the formula and the alternation depth, because this would provide the algorithm for free, but when I tried it there appears a problem in the case $\psi=\psi_1\vee\psi_2$.
Any ideas how to proof it, or where to find the answer?
Best, timtom