Defining relations without axiom of choice

Question

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?

Answer 1

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.