# When can an inner existential quantifier be eliminated in favour of a function relating terms?

I have a question which somehow relates to the great answer by Bauer in the question Techniques for Reversing the Order of Quantiﬁers, 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, 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)$"?

• 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 Jun 28 '13 at 11:27
• 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 Jun 28 '13 at 12:03
• 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 Jun 28 '13 at 12:21
• @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 Jun 28 '13 at 12:25
• 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 Jun 28 '13 at 12:28