In page 4 of Gödel's book The Consistency Of The Axiom Of Choice and Of The Generalized Continuum Hypothesis With The Axioms Of Set Theory, Gödel defined the $n$-tuple as
- $\langle x \rangle = x$;
- $\langle x_1, \ldots, x_n\rangle = \langle x_1, \langle x_2, \ldots, x_n \rangle\rangle$ for each $n \in \mathbb N$.
He defines $n$-tuples in a different order, while, customarily, we'd rather accept $\langle x_1, \ldots, x_{n}\rangle = \langle \langle x_1, \ldots, x_{n-1} \rangle, x_{n}\rangle$. But let's ignore this trivial difference.
I know this is a 1-based inductive definition. In my notes (invoking MK), I proved so called finite recursion theorem; it is a theorem without the limit case (the 3rd case) of transfinite recursion and the domain is restricted in $\mathbb N$, which states:
Let $\mathscr U$ denotes the universal class $\mathscr U = \{x: \exists X: x \in X\}$. Given a function $\phi: \mathscr U \to \mathscr U$, then there is a unique function $f: \mathbb N \to \mathscr U$ such that
- Base case: $f(0) = c$;
- Successor case: $f(n^+) = \phi(f(n))$ for each $n \in \mathbb N$.
This theorem can be easily proven (the proof is quite similar to that of the transfinite version), and gives the reason why some terms can be defined inductively. By this theorem, the ellipsis notation (arbitrarily finite case) can be well-defined.
I know MK and NBG are different system, but I'm sure that if (JUST if) inductive definitions must be supported by the definition of natural numbers, then so is Gödel's definition on $n$-tuples.
So, why can Gödel define such an inductive concept before the set theoretical definition of natural numbers is verified in the book? Or, does he used Peano's natural numbers as the foundation of his system implicitly?
This is a question I confused for a long time. So, in my notes, I avoid using ellipsis notation or natural index as possible as I can until the set theoretical $(\mathbb N, +, \times, \le)$ is introduced – even if I state that the Peano's axioms are invoked in the logic system, I have no idea when can I use them in set theory – though I know sometimes I can't.