Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question
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
up vote 5 down vote accepted

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

share|cite|improve this answer
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.

share|cite|improve this answer

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} $$

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.