different domains for each variable in predicate logic Before I begin, note that this is significantly outside what I've studied, so if it's a load of crap just let me know.
Up till now, everything I've covered assumes the same domain for all variables.
I'm trying to define an arbitrary one-to-one relationship between elements in two different sets, and want each of the variables x and y in the formula below to be in the domain of its particular set:

X = {X1, X2, X3}
Y = {Y1, Y2, Y3}

That is, I want:

x ∈ X, y ∈ Y

If possible, how would I go about specifying this?
Also, I've phrased the formula

∀x ∃y [ A(x, y) ∧ ¬A(¬x, y) ]

Where A(x, y) indicates an relationship between x and y. Is this statement well formed? Particularly the ¬x in ¬A(¬x, y)? And does it mean what I think it means - That A(x, y) for all x ∈ X except the x in question, and for the y in question, must be false in order for the statement ot be true? That is, does it define a one-to-one relationship?
Thanks a lot,
Wyatt
No, I don't think it makes sense to write $\neg x$ in this context. 

The simplest way to specify that $x\in X$ and $y\in Y$ is to make them clauses in your statement. For example, to write that for every $x\in X$ there should exist a $y\in Y$ such that $A(x,y)$ holds, you would usually write:


  $$\forall x \left(x\in X\rightarrow \exists y(y\in Y\wedge A(x,y)\right).$$


For the second part: to say that no other $z\in X$ will also be associated to $y$, the easiest why is to say that anyone who is associated to $y$ is going to be equal to $x$; so you would want a clause $A(z,y)\rightarrow x=z$.

To put it all together:


  $$\forall x\left( x\in X\rightarrow \exists y(y\in Y\wedge A(x,y)\wedge \forall z(z\in X\wedge A(z,y)\rightarrow x=z))\right).$$


It is also possible to use common (but perhaps slightly abusive) notation and write


  $$\forall x\in X\Bigl(\exists y\in Y\Bigl(\forall z\in X\Bigl(A(x,y)\wedge (A(z,y)\rightarrow x=z)\Bigr)\Bigr).$$


Added: As noted in several comments, the above does not completely describe a one-to-one function; it only describes a relation with domain $X$, codomain $Y$, such that for each $y\in Y$ there is at most one $x\in X$ such that $A(x,y)$ holds; this does not fully describe a function (unless you happen to know some other things about $X$ and $Y$, e.g., that they are both finite and of equal size, in which case the other condition will follow), nor a bijective function. In general, the clause you want for "function-ness" is the dual of the condition you have: for all $x\in X$, and for all $y\in Y$, $A(x,y)\wedge A(x,y')\rightarrow y=y'$ (so each input has at most one output). For bijectivity (so you have a true correspondence) you also need that for all $y\in Y$ there exists $x\in X$ such that $A(x,y)$.
There are lots of ways to write a formula A(x,y) that defines a bijection between two sets. If you're trying to keep the depth of quantifiers to a minimum, you could use
$$
\begin{align}
&amp;  (\forall x)(\exists y) [ x \in X \to y \in Y \land A(x,y)] \\
&amp; {} \land (\forall y)(\exists x) [ y \in Y \to x \in X \land A(x,y)]\\
&amp; {} \land (\forall x,x',y,y') ([x \in X \land y \in Y) \\
&amp; \qquad {} \to [(A(x,y) \land A(x',y) \to x=x'] 
 \land [A(x,y) \land A(x,y') \to y = y'])]\\
\end{align}
$$

This can be written more elegantly with the abbreviations $(\forall x \in X) $ and $(\exists x \in X)$:
$$
\begin{align}
(\forall x \in X)\Phi &amp;\equiv (\forall x) [ x \in X \to \Phi] \\
(\exists x \in X)\Phi &amp;\equiv (\exists x) [ x \in X \land \Phi] \\
\end{align}
$$
like so: 
$$
\begin{align}
&amp;  (\forall x \in X)(\exists y\in Y) A(x,y) \land (\forall y \in Y )(\exists x \in X) A(x,y)\\
&amp; {} \land (\forall x \in X)(\forall x' \in X)(\forall y \in Y)(\forall y' \in Y)([(A(x,y) \land A(x',y) \to x=x'] \\
&amp; \qquad \qquad {} \land [A(x,y) \land A(x,y') \to y = y'])\\
\end{align}
$$