How to formulate this lemma into a first order symbolic statement? (Finite Choice Lemma - Tao Analysis I)

Question

Here is a lemma that I have been tasked to prove. I am not interested in how to carry out this proof. Instead, I want to formally formulate the first order symbolic sentence that encodes the lemma. The lemma reads as follows:

Let $n \geq 1$ be a natural number, and for each natural number $1 \leq i \leq n$, let $X_i$ be a non-empty set. Then there exists an $n$-tuple $(x_i)_{1 \leq i \leq n}$ such that $x_i \in X_i$ for all $1\leq i \leq n$.

I am particularly interested in how one encodes the antecedent of this conditional (what I have bolded in the above highlighted lemma). For brevity, I am going to refer to the consequent (i.e. "then there exists an $n$ -tuple...") as $\exists \chi \big(\phi(\chi)\big)$.

The only thing I can really think to do is the following:

$\forall n, X_1 \Big(\big(n \in \mathbb N \land n = 1 \land X_1 \neq\emptyset\big) \rightarrow \exists \chi \big(\phi(\chi)\big) \Big)$

$\forall n, X_1, X_2 \Big(\big(n \in \mathbb N \land n = 2 \land X_1 \neq\emptyset \land X_2 \neq \emptyset \big) \rightarrow \exists \chi \big(\phi(\chi)\big) \Big)$

$\forall n, X_1, X_2, X_3 \Big(\big(n \in \mathbb N \land n = 3 \land X_1 \neq\emptyset \land X_2 \neq \emptyset \land X_3 \neq \emptyset \big) \rightarrow \exists \chi \big(\phi(\chi)\big) \Big)$

$...$

Edit:

After reading the below comments, I wonder if this is a better approach?

$\forall n, X \bigg(\Big( n \in N \land n \geq 1 \land \text{dom}(X) = \{i:1 \leq i \leq n \} \land \forall k \big(1 \leq k \leq n \implies X(k) \neq \emptyset\big)\Big) \implies \exists \chi \big(\phi(\chi)\big)\bigg)$

I probably need to specify that $i$ and $k$ are restricted to $\mathbb N$.

Answer 1

Set theory generally gives us the means to package complicated data into a single object. Ordered tuples and functions are the first things that come to mind.

Notice in the language of first order set theory, we don't have any "subscripting"... this is purely stuff that we do for our own convenience. When we say "for each $i \le n,$ let $X_i$ be a nonempty set", what is actually going on under the hood is we are defining a function:

$X$ is a function whose domain is the natural numbers $\le n$ and whose range contains only nonempty sets.

So we might more accurately write $X(i)$ rather than $X_i.$ But that notation is still not part of the formal language. A much-more-attentive-to-the-microcopic-details, but still not fully unpacked version would be

For every $x\in X,$ $x$ is an ordered pair such that the first component of $x$ is a natural number $\le n$ and the second component is a nonempty set. Furthermore, for each natural number $i\le n$, there is a unique $x\in X$ such that $i$ is the first component of $x$.

And for a given $i,$ the set $X_i$ would be defined as

The second component of the unique element of $X$ whose first component is $i.$

So that's the premise... when we want to write the conclusion -- which I presume says there is a function $f$ such that $f(i)\in X_i$ for all $i$ -- in a similar extreme level of detail, we need to go through the same song and dance as above to say $f$ is a function with domain $i\le n$, and then just say

For each $i\le n,$ the second component of the unique element of $f$ whose first component is $i$ is an element of the the second component of the unique element of $X$ whose first component is $i.$

---

On a side note, it can to massive confusion when we implicitly assume that the "subscripting" is something that somehow happens directly in the formal language. I've seen many-a-question where a student can't grasp how the axiom of choice is not trivially provable, with reasoning along the lines of

Each set $X_i$ is nonempty, so for all $i$, $\exists x_i\in X_i.$ So just set $f(i) = x_i.$

This misses the point because the informal notation misleadingly implies that there is a ready-made element $x_i$ already "chosen". If you unpack what this is actually saying formally, you will see it assumes the axiom choice, rather than proving it.