<p>I have a question which somehow relates to the great answer by Bauer in the question <a href="https://cstheory.stackexchange.com/questions/4473/techniques-for-reversing-the-order-of-quantiers/4478#4478">Techniques for Reversing the Order of Quantiﬁers</a>, where he discusses how the possibility of quantifier reversing depends on properties like companctness of the domain. </p>

<p>Let the quantifiers for $x,y$ range over the appropriate domain. The expressions I'm interested in are of the form </p>

<p>$$\forall x\ \exists y\ \phi(x,y),$$</p>

<p>as in $\ \forall x\ \exists y\  \left( f(x,y)=g(x,y) \right)$, e.g. $\ \forall x\ \exists y\ \left( \text e^{-x\ y}=x \right)$.</p>

<p>What are conditions so that the inner bounded variable can by elimninated by transforming the statement in the following sense:</p>

<p>$$\forall x\ \forall i \ \phi(x,\hat y(x,i)),$$</p>

<p>where $\phi$ is unchanges, but I scanned for all solutions $y(x)$ and indexed them by $i$. In this way, I've essentially solved the problem (the difficult part being to find $\hat y$) and obtained the true formula</p>

<p>$$\phi(x,\hat y(x,i))$$</p>

<p>where above the free variables are implicitly taken to be universally quantified.</p>

<p>The form $\forall x\ \forall i \ \phi(x,\hat y(x,i))$ looks similar to the one in the link to the other question, except for me having introduced the disjuctions for different cases by another universal quantifier in $\forall i $. The point is that I didn't just reverse the order of quantifiers $\forall, \exists$, I literally solved the $\exists$-question. For the numberical problem $\ \forall x\ \exists y\ \left( \text e^{-x\ y}=x \right)$ this works, as there is the a function reklating $x$ and $y$ (the soltion being expressible in terms of the <a href="http://en.wikipedia.org/wiki/Lambert_w_function" rel="nofollow noreferrer">W-function</a>, not that this matters here). I can also view $\hat y$ as implicitly definded by the initial expression. </p>

<p>When can I expect this not to work? And is this just strictly a stronger requirement than being able to transform the expression to, roughly, "$\exists y\ \forall x \ \phi(x,y)$"?</p>

CC BY-SA 3.0
2013-06-28T11:27:57.483Z
I wonder about generality here.  If you are talking about the level of Skolemisation, then can't you just stipulate that your new $\hat y$ function constant behaves as it should?  If the cardinality constraints are fine, I should think you can get satisfiability by a very similar argument to Skolemisation.  But for arbitrary specialised mathematical domains, this problem looks harder.
Charles Stewart
CC BY-SA 3.0
2013-06-28T12:03:26.623Z
I find the question somewhat problematic. What are the domains of $x$, $y$ and $i$? In particular, it seems that the domain of $i$ depends upon the selected $x$.
Dave Clarke
CC BY-SA 3.0
2013-06-28T12:21:02.973Z
I understand the Skolemisation as $\forall x\ \exists y\ \phi(x,y)\longrightarrow \exists \bar y\forall x\ \phi(x,\bar y(x))$. What I want is similar, although I ask for the condition to being able to actually produce the "Skolem function" $\bar y$. In fact, a function $\bar y$ would actually choose a suitable $y$ for each $x$, I on the other hand want to get all $\bar y$'s, that's why I introduce the index. I change the expression $\phi(-,-)$ to $\phi(-,\bar y(-,i))$ and avoid quantification over functions. $i$ is just a parameter. I want to know for which math theories I can expect barriers.
Nikolaj-K
CC BY-SA 3.0
2013-06-28T12:25:09.457Z
@DaveClarke: The $i$'s shouldn't depend on $x$, as they just index the functions. Regarding the domains, I initially am think of (real) numbers as in the formula with the exp-function. But I'm not sure if the restriction is necessary/relevant to this question. The way I stated it, it's essentially a logical question. Though I'm practically motivated - the Wikipedia article on Skolemisation, for example, just talks about the function being there due to the axiom of choise - but this isn't helping me finding the function - the question is in which cases I will *not* be able to compute it.
Nikolaj-K
CC BY-SA 3.0
2013-06-28T12:27:26.903Z
If for one $x$ there are two possibly $y$s, then $i$ should range over $\{1,2\}$ whereas if there are 5, then $i$ should range over $\{1,2,3,4,5\}$. Of course, you could just use (say) $\mathbb{N}$ and map most values of $i$ to one of the 2 or 5 solutions.
Dave Clarke
CC BY-SA 3.0
2013-06-28T12:28:39.330Z
I admit that I'm look at this from a type theoretic perspective, where the domain not only makes sense, but is required.
Dave Clarke
<lo.logic>
When can an inner existential quantifier be eliminated in favour of a function relating terms?
Nikolaj-K
# When can an inner existential quantifier be eliminated in favour of a function relating terms?

(Asked by: username_0 on 2013-06-28)

I have a question which somehow relates to the great answer by Bauer in the question [Techniques for Reversing the Order of Quantiﬁers](https://cstheory.stackexchange.com/questions/4473/techniques-for-reversing-the-order-of-quantiers/4478#4478), where he discusses how the possibility of quantifier reversing depends on properties like companctness of the domain.

Let the quantifiers for $x,y$ range over the appropriate domain. The expressions I'm interested in are of the form

$$\forall x\ \exists y\ \phi(x,y),$$

as in $\ \forall x\ \exists y\ \left( f(x,y)=g(x,y) \right)$, e.g. $\ \forall x\ \exists y\ \left( \text e^{-x\ y}=x \right)$.

What are conditions so that the inner bounded variable can by elimninated by transforming the statement in the following sense:

$$\forall x\ \forall i \ \phi(x,\hat y(x,i)),$$

where $\phi$ is unchanges, but I scanned for all solutions $y(x)$ and indexed them by $i$. In this way, I've essentially solved the problem (the difficult part being to find $\hat y$) and obtained the true formula

$$\phi(x,\hat y(x,i))$$

where above the free variables are implicitly taken to be universally quantified.

The form $\forall x\ \forall i \ \phi(x,\hat y(x,i))$ looks similar to the one in the link to the other question, except for me having introduced the disjuctions for different cases by another universal quantifier in $\forall i $. The point is that I didn't just reverse the order of quantifiers $\forall, \exists$, I literally solved the $\exists$-question. For the numberical problem $\ \forall x\ \exists y\ \left( \text e^{-x\ y}=x \right)$ this works, as there is the a function reklating $x$ and $y$ (the soltion being expressible in terms of the [W-function](http://en.wikipedia.org/wiki/Lambert_w_function), not that this matters here). I can also view $\hat y$ as implicitly definded by the initial expression.

When can I expect this not to work? And is this just strictly a stronger requirement than being able to transform the expression to, roughly, "$\exists y\ \forall x \ \phi(x,y)$"?

**Tags:** lo.logic
> **Comments:**
> **username_1**: I wonder about generality here.  If you are talking about the level of Skolemisation, then can't you just stipulate that your new $\hat y$ function constant behaves as it should?  If the cardinality constraints are fine, I should think you can get satisfiability by a very similar argument to Skolemisation.  But for arbitrary specialised mathematical domains, this problem looks harder.  
> **username_2**: I find the question somewhat problematic. What are the domains of $x$, $y$ and $i$? In particular, it seems that the domain of $i$ depends upon the selected $x$.  
> **username_0**: I understand the Skolemisation as $\forall x\ \exists y\ \phi(x,y)\longrightarrow \exists \bar y\forall x\ \phi(x,\bar y(x))$. What I want is similar, although I ask for the condition to being able to actually produce the "Skolem function" $\bar y$. In fact, a function $\bar y$ would actually choose a suitable $y$ for each $x$, I on the other hand want to get all $\bar y$'s, that's why I introduce the index. I change the expression $\phi(-,-)$ to $\phi(-,\bar y(-,i))$ and avoid quantification over functions. $i$ is just a parameter. I want to know for which math theories I can expect barriers.  
> **username_0**: @DaveClarke: The $i$'s shouldn't depend on $x$, as they just index the functions. Regarding the domains, I initially am think of (real) numbers as in the formula with the exp-function. But I'm not sure if the restriction is necessary/relevant to this question. The way I stated it, it's essentially a logical question. Though I'm practically motivated - the Wikipedia article on Skolemisation, for example, just talks about the function being there due to the axiom of choise - but this isn't helping me finding the function - the question is in which cases I will *not* be able to compute it.  
> **username_2**: If for one $x$ there are two possibly $y$s, then $i$ should range over $\{1,2\}$ whereas if there are 5, then $i$ should range over $\{1,2,3,4,5\}$. Of course, you could just use (say) $\mathbb{N}$ and map most values of $i$ to one of the 2 or 5 solutions.  
> **username_2**: I admit that I'm look at this from a type theoretic perspective, where the domain not only makes sense, but is required.  

---

## 0 answers

