Assign ForAll and Exists to two different variables in same equation

Questions
1

I want to Resolve a multivariate inequality but assign different quantifiers to different variables.

Example:

Resolve[Exists[{x}, x^2 + y^2 < 1]]

Now I want to add ForAll quantifier to y. Is there any other way than the following to achieve this because the following would be mess if the number of variables are increased?

Resolve[Exists[{x}, x^2 + y^2 < 1] && ForAll[y, x^2 + y^2 < 1]]

2

In logic, you normaly nest quantifiers. Using Mathematica’s notation that would be written:

ForAll[y,Exists[x, x^2 + y^2 < 1]]

Or

Exists[x, ForAll[y,x^2 + y^2 < 1]]

These mean different things because the order of quantitifcation matters.

I’m not sure what your statement means however:

Exists[{x}, x^2 + y^2 < 1] && ForAll[y, x^2 + y^2 < 1]

In the first part of the conjunction, y is being treated as a constant, but then it’s being bound to a quantifier in the second part of the conjunction. Are they meant to be different symbols? I’m not sure what it would mean if they weren’t. I don’t think it makes sense as you’ve written it right now.