Using Kuratowskis definition of n-tuples, we get:
$\langle ~ \rangle := \emptyset \\ \langle a_1 \rangle := a_1 \\ \langle a_1,a_2 \rangle := \{\{a_1 \},\{ a_1,a_2 \} \} \\ \langle a_1, a_2, …, a_{n+1} \rangle := \langle \langle a_1, a_2, …, a_n \rangle, a_{n+1} \rangle$
We can simply prove the existence of arbitrarily many n-tupels by applying the axiom of pairing. Let $a_1$ and $a_2$ be arbitrary sets. By the axiom of pairing, we get $\{a_1\}$ and $\{a_1,a_2\}$. Using the axiom of pairing again, we get $\{\{a_1\}, \{\{a_1,a_2\}\}$ and, by the above definition, $\langle a_1, a_2 \rangle$. You can define n-tuples easily this way. Nonetheless, you will only get finitely many n-tuples.
Now since there are functions with infinite domains and (the graphs of) functions are defined as sets of tuples, there must also be infinitely many tuples. But how do the axioms of set theory guarantee that this is the case?
It seems to me that the axiom of replacement plays an important role here in combination with the axiom of infinity. Define the natural numbers as the cut of all inductive subsets of the powerset of any set A the axiom of infinity specifies:
$\mathbb{N} := \bigcap \{x\in\mathfrak{P}(A)\mid\forall y (y\in A \to y\cup\{y\}\in A)\}$
Now replace every element of $\mathbb{N}$ by a tuple. That's the informal idea. Let $\alpha[x,y]$ be an open formula containing only $x$ and $y$ free. The formal idea is to find a substitution instance for the following axiom:
$\forall x\forall y\forall z(\alpha[x,y] \land \alpha [x,z] \to y=z) \to \forall x\exists y\forall z(z\in y \leftrightarrow \exists x'(x'\in x \land \alpha[x',z]))$
Now I have two questions:
- How exactly does the substitution instance look like? Why are there equivalent formulations of the axiom of replacement which feature replacement functions?
- There of course are infinitely many tuples. But are there also tuples with infinitely many components, e.g. $\langle 0,1,2,...\rangle$? If so, how can you prove it? If not, how can you prove it?