Is there any use for multiple variables in same quantifier?

Question

For predicates, it is possible to pass multiple variables. They are called polyadic predicates in that case, for example, $P(x, y)$. But how about quantifiers. I have not seen an example of this but want to be sure.

Is there usage for something like:

a)

$$∀(x∈A, y∈B)(x | y)$$

in the first-order logic?

I could provide arguments in the following manner:

If multiple domain sets are provided, then values could be passed to the quantifier in tuples taking one item from each domain to match each argument. Say $A = [1 2 3]$ and $B = [1 2 3 4]$. Then we send arguments in groups of: $(x=1, y=1)$, $(x=2, y=2)$, and $(x=3, y=3)$ and leave the last iteration out because there is no pair for y: $(x=undefined, y=4)$. Is this too far from convention?

Or should it just be:

b)

$$∀x∈A(∀y∈B(x | y))$$

Or maybe even:

c)

$$∀x∈A∀y∈B(x | y)$$

Apparently b) and c) would give same truth value, but a) differs dramatically from the last two...

$|$ is just an arbitrary operation between $x$ and $y$.

Answer 1

Technically, it all depends on how the formal syntax is exactly defined (though I have never seen a formal syntax that would support the first version, I suppose one could define syntax in a way that supports that).

But in practice everyone will understand all these three forms. So, unless you are doing a formal logic proof, go ahead and use any of those forms.

In fact, in math proofs you do often see $\forall x,y ...$

EDIT

OK, so I think I understand now what you are trying to do: you want the one quantifier to signify one object ... but it would have to be an object that exists in $A$ as well as $B$. Hmmm, 'too far from convention' is not a bad phrase to use here :). But I think it is also 'too far from useful' as well. If the quantifier signifies one object, then I would say use one variable as well. ... and if it needs to be in $A$ as well as $B$, then maybe just do:

$$\forall x \in A \cap B \ x|x$$

Answer 2

I never seen the first, and can be better write as $$ \forall(x,y)\in A\times B $$

that I prefer also to the other two notations.

Answer 3

The logics used in proof assistants like those in the HOL family and many others support this kind of syntax for quantifiers. It is often called "pattern-matching abstraction", because in place of the bound variable after the quantifier, we have a "pattern" $(x \in A, y \in B)$.