# 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

-
Your condition doesn't seem to rule out there being two distinct $y_1$ and $y_2$ such that both $A(x,y_1)$ and $A(x,y_2)$ hold for some $x$. Also, what is your motivation for trying to encode injective (or bijective?) functions into predicate logic? Is it purely curiosity? – Rahul Sep 22 '10 at 6:19

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)$.

-
If you're looking for a bijection, you also need to add the corresponding formula that ensures surjectivity. – Carl Mummert Sep 22 '10 at 10:53

It seems to me what you're trying to do is formulate a first-order theory. This has non-logical axioms. Your theory uses two one-place predicates, say "F" for the Xs and "G" for the Ys. It has one non-logical axiom, perhaps, which says there are Fs and there are Gs. Then it has another which says nothing is both F and G. Then you have a two-place predicate "R" to represent the relationship, and another non-logical axiom for that, one that uses "F" and "G" as well as "R". From the point of view of logic, there's still only one domain; it's your non-logical axioms that divide it up. -- It's the predicates and axioms that are important, not the variables "x" and "y". Shoenfield's text Mathematical Logic is good for examples of first-order theories.

Edit: by non-logical axiom I mean an axiom that's not itself already provable in first-order logic.

-

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} & (\forall x)(\exists y) [ x \in X \to y \in Y \land A(x,y)] \\ & {} \land (\forall y)(\exists x) [ y \in Y \to x \in X \land A(x,y)]\\ & {} \land (\forall x,x',y,y') ([x \in X \land y \in Y) \\ & \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 &\equiv (\forall x) [ x \in X \to \Phi] \\ (\exists x \in X)\Phi &\equiv (\exists x) [ x \in X \land \Phi] \\ \end{align} like so: \begin{align} & (\forall x \in X)(\exists y\in Y) A(x,y) \land (\forall y \in Y )(\exists x \in X) A(x,y)\\ & {} \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'] \\ & \qquad \qquad {} \land [A(x,y) \land A(x,y') \to y = y'])\\ \end{align}

-