Extension of the first-order logic by means of multiple domains/universes.

Question

Is there an extension of the first-order logic by means of multiple domains/universes?
I mean, is there a logic that allows to have predicates/functions that get several kinds of parameters?
For example: P(x1, x2), where x1 is from domain D1 and x2 is from domain D2.
Another example: P(x1, x2) = IsFunctionHasItsMaxValueAtX(func, x), where func is from the domain of functions and x is a natural number.

Answer 1

It sounds like you're describing many-sorted (first-order) logic. Note that if there are only finitely many sorts, this can be appropriately simulated in first-order logic via unary predicates.