(This is quite a small question, but also pretty specific so forgive the wall of text!)
I'm trying to learn about Hilbert's $\varepsilon$-calculus (Bourbaki use a similar system in their volume on set theory). The basic idea is that $\varepsilon$ is a term-forming operator (sort of like Russell's iota) which functions like a choice function. The term $\varepsilon_x\phi x$ stands for, in effect, 'the first $\phi$' an arbitrary element of the domain which satisfies $\phi x$ if there are any — if there aren't, then it denotes some other arbitrary object. $\varepsilon$-calculi are supposed to be able to analyse quantificational sentences. In all the introductions I can find online (the IEP and SEP articles, and a few sets of lecture notes) the extent of the detail given about this analysis is just the definitions
$\exists x\phi x := \phi(\varepsilon_x\phi x)$
$\forall x\phi x := \phi(\varepsilon_x¬\phi x)$
I'm interested on how this extends to cover cases of nested quantifiers. The simplest case would be a sentence of the form $\exists x\exists y\phi xy$. I've tried applying these definitions to analyse out these quantifiers but I end up with something confusing. I'll put the scope of the epsilons in square brackets and include all parentheses to make things slightly more legible. Starting at
$\exists x\exists y\phi(x,y)$
I apply the analysis to the outermost quantifier.
$\exists y\phi(\varepsilon_x[\exists y\phi(x,y)],y)$
Then do the same again.
$\phi(\varepsilon_x[\exists y\phi(x,y)],\varepsilon_y[\phi(\varepsilon_x[\exists y \phi(x,y)],y])$
Then since $\exists y\phi(x,y)$ is analysed $\phi(x,\varepsilon_y[\phi(x,y)])$, I substitute this in to arrive at the fully analysed formula:
$\phi(\varepsilon_x[\phi(x,\varepsilon_y[\phi(x,y)])],\varepsilon_y[\phi(\varepsilon_x[\phi(x,\varepsilon_y[\phi(x,y)])],y)])$
The thing I'm confused over is that there is a $\varepsilon_y$ within the scope of another $\varepsilon_y$. When I replace the subordinate of these terms with just 'y', then I get the slightly more sensical
$\phi(\varepsilon_x[\phi(x,\varepsilon_y[\phi(x,y)])],\varepsilon_y[\phi(\varepsilon_x[\phi(x,y)],y]))$
But I don't know what justifies this substitution. Couldn't $\varepsilon_y[\phi(\varepsilon_x[\phi(x,\varepsilon_y[\phi(x,y)])],y)]$ and the subordinate term $\varepsilon_y[\phi(x,y)]$ refer to different objects? In which case substituting $\varepsilon_y[\phi(x,y)]$ for $\varepsilon_y[\phi(\varepsilon_x[\phi(x,\varepsilon_y[\phi(x,y)])],y)]$ might not the preserve truth of the whole sentence in every case?
I'd be very thankful if anyone could help me out.
Best Answer
At first, I thought you'd do better by analyzing the inner quantifier first. So $\exists x\exists y\,\phi(x,y)$ first becomes $$ \exists x\,\phi(x,\varepsilon_y\phi(x,y)) $$ and then becomes $$ \phi(\varepsilon_x\phi(x,\varepsilon_y\phi(x,y)), \varepsilon_y\phi(\varepsilon_x\phi(x,\varepsilon_y\phi(x,y)),y). $$ But that's exactly what you got by analyzing the outer quantifier first. So I think your solution is fine up to that point. Then you said you were confused because there's an $\varepsilon_y$ in the scope of another $\varepsilon_y$. I don't think there's anything wrong with such nested $\varepsilon_y$'s. But if you really don't like them, remember that $\varepsilon$ binds its variable, i.e., $\varepsilon_y\psi(y)$ is synonymous with $\varepsilon_z\psi(z)$ (as long as you avoid clashes of bound variables). So you could replace the inner $\varepsilon_y$ with $\varepsilon_z$ and replace all the $y$'s in its scope by $z$'s.