<p>I'm currently studying <a href="https://www.cs.cornell.edu/fbs/publications/Hyperproperties.pdf" rel="nofollow noreferrer">hyperlogics</a> and in particular <a href="https://arxiv.org/abs/1401.4492" rel="nofollow noreferrer">HyperLTL/CTL*</a>.
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.</p>
<p>Working on better algorithms, a question came up which is actually more general:</p>
<p><em>Let <span class="math-container">$\phi$</span> be a first order logic formula in negation normal form. Further let <span class="math-container">$\alpha(\psi)=k$</span> be the alternation depth of <span class="math-container">$\phi$</span>, 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 <span class="math-container">$\psi^*$</span> of <span class="math-container">$\psi$</span>? Is there an algorithm to constuct a prenex formula for which the lower bound holds?</em></p>
<p>I did not fnd the question anywhere yet. I'm quit sure the answere should be that <span class="math-container">$\alpha(\psi^*)\leq\alpha(\psi)+1$</span> is always possible.</p>
<p>But I can't proof it. I can't find the right induction hypothesis.</p>
<p>Any ideas how to proof it, or where to find the answer?</p>
<p>Best, timtom</p>

CC BY-SA 4.0
2023-04-25T06:52:32.243Z
Yes, this is straightforward. Prove by induction on the complexity of the formula that it has a prenex form with $\alpha(\psi)$ alternations and the first quantifier block existential, and also a prenex form with $\alpha(\psi)$ alternations and the first quantifier block universal (I'm allowing blocks to be empty). Moreover, you can get $\alpha(\psi^*)=\alpha(\psi)$ if $\psi$ starts with a quantifier (but then you do not have choice for the first block type).
Emil Jeřábek
CC BY-SA 4.0
2023-04-25T12:47:08.350Z
But isn't there a problem for the case $\psi=\exists\pi\psi_0$? Let $\alpha(\psi)=\alpha(\psi_0)=k$. By hypothesis there is a prenex form  $\psi_0^*$  with $\alpha(\psi_0^*)=k+1$ starting with a block of existential quantifiers and one starting with a block of universal quantifiers. But how can we deduce that there is one with alt.depth. k+1 and starting with a block of universal quantifiers for $\psi$? We only get it for a prenex form beginning with existential quantifiers..... where is my fault?
timtombobjohn
CC BY-SA 4.0
2023-04-25T12:58:54.273Z
Hmm; maybe this is not the right induction hypothesis after all. The root of the problem is that $\alpha$ is a pretty terrible measure, as it does not obey any simple recursive definition. Consider instead the measures “the number of quantifier alternations starting from an existential state”, denoted $\alpha_\exists(\psi)$, and the universal analogue, $\alpha_\forall(\psi)$. These satisfy $\alpha_Q(\psi)=0$ for $\psi$ quantifier-free and $Q\in\{\exists,\forall\}$, $\alpha_Q(\psi_0\circ\psi_1)=\max\{\alpha_Q(\psi_0),\alpha_Q(\psi_1)\}$ for $\circ\in\{\land,\lor\}$, ...
Emil Jeřábek
CC BY-SA 4.0
2023-04-25T13:04:19.063Z
... $\alpha_Q(Qx_i\,\psi_0)=\alpha_Q(\psi_0)$, and $\alpha_{\overline Q}(Qx_i\,\psi_0)=1+\alpha_Q(\psi_0)$ where $\overline Q$ is the quantifier dual to $Q$. Then a straightforward induction shows that for $Q\in\{\exists,\forall\}$, $\psi$ has a prenex form $\psi_Q$ stating with a $Q$ block such that $\alpha_Q(\psi_Q)=\alpha_Q(\psi)$. Now, to relate this to $\alpha$, we have $\alpha(\psi)=\alpha_Q(\psi)$ if $\psi$ starts with quantfier $Q$, and in general, $\alpha(\psi)\le\min\{\alpha_\exists(\psi),\alpha_\forall(\psi)\}\le\max\{\alpha_\exists(\psi),\alpha_\forall(\psi)\}\le\alpha(\psi)+1$....
Emil Jeřábek
CC BY-SA 4.0
2023-04-25T13:07:22.897Z
... This implies what I wrote before: $\psi$ has a prenex form with $\alpha(\psi)$ alternations if $\psi$ starts with a quantifier, and for general $\psi$, it has both a prenex form starting with an existential block and a prenex form starting with a universal block with $\alpha(\psi)+1$ alternations.
Emil Jeřábek
CC BY-SA 4.0
2023-04-25T13:18:16.283Z
You don’t need the formula to be in negation normal form, by the way. It works for arbitrary formulas; the clauses for $\neg$ are $\alpha_Q(\neg\psi_0)=\alpha_{\overline Q}(\psi_0)$.
Emil Jeřábek
CC BY-SA 4.0
2023-04-25T14:16:01.793Z
Cross-posted from https://math.stackexchange.com/questions/4685690/number-of-quantifier-alternations-in-prenex-form-of-a-formula
Emil Jeřábek
CC BY-SA 4.0
2023-04-25T15:52:17.107Z
not sure if I'm understanding the new measure correctly.  Example: let $\psi=\exists x_1\forall x_2\exists x_3\psi'$, where $\psi'$ is quantifier-free. I expected $\alpha_\forall(\psi)=1$ and $\alpha_\exists(\psi)=1$, but then  $\alpha(\psi)\leq\max\{\alpha_\exists(\psi),\alpha_\forall(\psi)\}$ would not hold, since $\alpha(\psi)=2$
timtombobjohn
CC BY-SA 4.0
2023-04-25T16:08:48.890Z
No, $\alpha_\exists(\psi)=2$ and $\alpha_\forall(\psi)=3$.
Emil Jeřábek
CC BY-SA 4.0
2023-04-25T20:35:52.457Z
I'm really sorry, I don't get the definition of the measure. I missunderstood that you would mean by “the number of quantifier alternations starting from an existential state” the number of alternations from an existential to an universal quantifier - could you maybe rephrase it?
timtombobjohn
CC BY-SA 4.0
2023-04-25T20:40:27.507Z
Another way to put it is that $\alpha_\exists(\psi)=\alpha(\exists x\,\psi)$, $\alpha_\forall(\psi)=\alpha(\forall x\,\psi)$. Or just follow the inductive definition, this leaves no room for interpretation.
Emil Jeřábek
<automata-theory><model-checking><program-verification><temporal-logic><first-order-logic>
Number of quantifier alternations in prenex form of a formula
timtombobjohn
# Number of quantifier alternations in prenex form of a formula

(Asked by: username_0 on 2023-04-24)

I'm currently studying [hyperlogics](https://www.cs.cornell.edu/fbs/publications/Hyperproperties.pdf) and in particular [HyperLTL/CTL\*](https://arxiv.org/abs/1401.4492).
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.

Any ideas how to proof it, or where to find the answer?

Best, timtom

**Tags:** automata-theory, model-checking, program-verification, temporal-logic, first-order-logic

> **Comments:**
> **username_1**: Yes, this is straightforward. Prove by induction on the complexity of the formula that it has a prenex form with $\alpha(\psi)$ alternations and the first quantifier block existential, and also a prenex form with $\alpha(\psi)$ alternations and the first quantifier block universal (I'm allowing blocks to be empty). Moreover, you can get $\alpha(\psi^*)=\alpha(\psi)$ if $\psi$ starts with a quantifier (but then you do not have choice for the first block type).  
> **username_0**: But isn't there a problem for the case $\psi=\exists\pi\psi_0$? Let $\alpha(\psi)=\alpha(\psi_0)=k$. By hypothesis there is a prenex form  $\psi_0^*$  with $\alpha(\psi_0^*)=k+1$ starting with a block of existential quantifiers and one starting with a block of universal quantifiers. But how can we deduce that there is one with alt.depth. k+1 and starting with a block of universal quantifiers for $\psi$? We only get it for a prenex form beginning with existential quantifiers..... where is my fault?  
> **username_1**: Hmm; maybe this is not the right induction hypothesis after all. The root of the problem is that $\alpha$ is a pretty terrible measure, as it does not obey any simple recursive definition. Consider instead the measures “the number of quantifier alternations starting from an existential state”, denoted $\alpha_\exists(\psi)$, and the universal analogue, $\alpha_\forall(\psi)$. These satisfy $\alpha_Q(\psi)=0$ for $\psi$ quantifier-free and $Q\in\{\exists,\forall\}$, $\alpha_Q(\psi_0\circ\psi_1)=\max\{\alpha_Q(\psi_0),\alpha_Q(\psi_1)\}$ for $\circ\in\{\land,\lor\}$, ...  
> **username_1**: ... $\alpha_Q(Qx_i\,\psi_0)=\alpha_Q(\psi_0)$, and $\alpha_{\overline Q}(Qx_i\,\psi_0)=1+\alpha_Q(\psi_0)$ where $\overline Q$ is the quantifier dual to $Q$. Then a straightforward induction shows that for $Q\in\{\exists,\forall\}$, $\psi$ has a prenex form $\psi_Q$ stating with a $Q$ block such that $\alpha_Q(\psi_Q)=\alpha_Q(\psi)$. Now, to relate this to $\alpha$, we have $\alpha(\psi)=\alpha_Q(\psi)$ if $\psi$ starts with quantfier $Q$, and in general, $\alpha(\psi)\le\min\{\alpha_\exists(\psi),\alpha_\forall(\psi)\}\le\max\{\alpha_\exists(\psi),\alpha_\forall(\psi)\}\le\alpha(\psi)+1$....  
> **username_1**: ... This implies what I wrote before: $\psi$ has a prenex form with $\alpha(\psi)$ alternations if $\psi$ starts with a quantifier, and for general $\psi$, it has both a prenex form starting with an existential block and a prenex form starting with a universal block with $\alpha(\psi)+1$ alternations.  
> **username_1**: You don’t need the formula to be in negation normal form, by the way. It works for arbitrary formulas; the clauses for $\neg$ are $\alpha_Q(\neg\psi_0)=\alpha_{\overline Q}(\psi_0)$.  
> **username_1**: Cross-posted from https://math.stackexchange.com/questions/4685690/number-of-quantifier-alternations-in-prenex-form-of-a-formula  
> **username_0**: not sure if I'm understanding the new measure correctly.  Example: let $\psi=\exists x_1\forall x_2\exists x_3\psi'$, where $\psi'$ is quantifier-free. I expected $\alpha_\forall(\psi)=1$ and $\alpha_\exists(\psi)=1$, but then  $\alpha(\psi)\leq\max\{\alpha_\exists(\psi),\alpha_\forall(\psi)\}$ would not hold, since $\alpha(\psi)=2$  
> **username_1**: No, $\alpha_\exists(\psi)=2$ and $\alpha_\forall(\psi)=3$.  
> **username_0**: I'm really sorry, I don't get the definition of the measure. I missunderstood that you would mean by “the number of quantifier alternations starting from an existential state” the number of alternations from an existential to an universal quantifier - could you maybe rephrase it?  
> **username_1**: Another way to put it is that $\alpha_\exists(\psi)=\alpha(\exists x\,\psi)$, $\alpha_\forall(\psi)=\alpha(\forall x\,\psi)$. Or just follow the inductive definition, this leaves no room for interpretation.  

---

## 0 answers

