# Defining relations without axiom of choice

One can show that the axiom of choice is equivalent to: "the product of a family of non-empty sets $\{ X_i \}_{i \in I}$ is never empty". Now, I've always seen a relation being defined via $R \subset X \times X$ and $x \leq y \Leftrightarrow (x, y) \in R$. But doesn't one use the axiom of choice implicitly for the existence of $X \times X$? Or is there another way to define a relation?

• Finite products are a non-issue. Besides, $X$ could be empty anyway. – Zhen Lin Sep 24 '15 at 12:05
• A missing axiom of choice does not mean that you couldn't happen to be able to do the same operation in certain cases. You could for example (manage to) prove that $X\times X$ is non-empty without the axiom of choice (given that $X$ is non-empty). – skyking Sep 24 '15 at 12:06
• @Zhen Lin: Thanks, edited it. – Steven Sep 24 '15 at 12:08

Relations as subsets of binary products exist regardless of the axiom of choice: they're just sets of ordered pairs, and ordered pairs can be constructed from the axiom of pairing by identifying $(a,b)$ with $\{ \{ a \}, \{ a, b \} \}$ for example.
The key word in your question is 'never', which refers to a hidden universal quantifier - the equivalent form of the axiom of choice you're thinking of is: for all sets $I$, and all families of non-empty sets $\{ X_i \}_{i \in I}$ indexed by $I$, the product $\prod_{i \in I} X_i$ is non-empty.
When $I$ is finite, the statement is true. But the truth for arbitrary $I$ depends on (and is equivalent to) the axiom of choice.