Proof of The Natural Numbers Read in ℝ: a Predicative Condition and a Function from ℕ₀ to ℝ

Throughout, $\mathbb{N}_{0}=\mathbb{N}\cup\{0\}$ with $0\notin\mathbb{N}$ (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii)), and $n_{\mathbb{R}}\in\mathbb{R}$ for every $n\in\mathbb{N}_{0}$: $0_{\mathbb{R}}$ is the zero of $\mathbb{R}$, and for $n\in\mathbb{N}$ the sum $n_{\mathbb{R}}$ is the value at $n$ of a map from $[n]$ to $\mathbb{R}$ (The Image of a Natural Number in a Commutative Ring (i), Iterated Operations: Finite Sums and Finite Products (i)).

The constant function $e$. By Maps and Relations Given by Formulas (i), applied to the sets $\mathbb{N}_{0}$ and $\mathbb{R}$ and the constant expression $1$, there is a function $e:\mathbb{N}_{0}\to\mathbb{R}$ with $e(k)=1$ for every $k\in\mathbb{N}_{0}$. Let $n\in\mathbb{N}$. Then $[n]\subseteq\mathbb{N}_{0}$, and the restriction $e|_{[n]}$ is the constant function $k\mapsto1$ on $[n]$, so by Iterated Operations: Finite Sums and Finite Products (ii) and The Image of a Natural Number in a Commutative Ring (i)

$$n_{\mathbb{R}}=\sum_{k=1}^{n}1=\sum_{k=1}^{n}e_{k}.$$

Proof of (i). Let $c$, $o$ and $z$ be class parameters standing for $e$, the element $0$ of $\mathbb{N}_{0}$ and the zero $0$ of $\mathbb{R}$, distinct from the class variables of the formula $\mathrm{it}$ below. Let $\mathrm{it}(w,n,a)$ be the predicative formula of Iterated Operations Are Given by a Predicative Formula (i) for distinct set variables $w$, $n$ and $a$, with $\mathbb{R}$, the addition of $\mathbb{R}$, $\mathbb{N}$, and the order and the addition of $\mathbb{N}_{0}$ assigned to its class variables, and let $\mathrm{it}(x_{i},x_{j},c)$ be obtained from it by renaming $w$, $n$ and $a$ to $x_{i}$, $x_{j}$ and $c$. Moving the formula to these positions is a renaming of variables, so by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i) it is predicative and, as $c$ stands for the set $e$, it holds exactly when $\mathrm{it}(w,n,a)$ holds with the values of $x_{i}$ and $x_{j}$ and the set $e$ assigned to $w$, $n$ and $a$. Let $\psi$ be

$$x_{j}\in\mathbb{N}_{0}\wedge\bigl((x_{j}=o\wedge x_{i}=z)\vee(x_{j}\in\mathbb{N}\wedge\mathrm{it}(x_{i},x_{j},c))\bigr).$$

It is built by connectives from atomic formulas and the predicative formula $\mathrm{it}$, so it is predicative, and its free variables are $x_{i}$, $x_{j}$ and parameters. Let sets be assigned to $x_{0},\dots,x_{N-1}$. If $x_{j}\notin\mathbb{N}_{0}$, then $\psi$ and the condition both fail. If $x_{j}=0$, then $x_{j}\notin\mathbb{N}$, so $\psi$ holds if and only if $x_{i}=0$ in $\mathbb{R}$, that is, $x_{i}=0_{\mathbb{R}}$ by The Image of a Natural Number in a Commutative Ring (i). If $x_{j}\in\mathbb{N}$, then $x_{j}\neq0$, and $e$ is a function from a set containing $[x_{j}]$ to $\mathbb{R}$, so $\psi$ holds if and only if $x_{i}=\sum_{k=1}^{x_{j}}e_{k}$ by Iterated Operations Are Given by a Predicative Formula (i), that is, $x_{i}=(x_{j})_{\mathbb{R}}$ by the display above. Hence $\psi$ expresses the condition.

Proof of (ii). By (i), for every $n\in\mathbb{N}_{0}$ the set $n_{\mathbb{R}}$ is the only set $x_{i}$ satisfying $\psi$ with $n$ assigned to $x_{j}$. So $n_{\mathbb{R}}$ is a defined set symbol with argument $n$, given by $\psi$ and used properly wherever $n\in\mathbb{N}_{0}$. As $n_{\mathbb{R}}\in\mathbb{R}$ for every $n\in\mathbb{N}_{0}$, Maps and Relations Given by Formulas (i), applied to the sets $\mathbb{N}_{0}$ and $\mathbb{R}$ and the expression $n_{\mathbb{R}}$, gives exactly one function $\iota:\mathbb{N}_{0}\to\mathbb{R}$ with $\iota(n)=n_{\mathbb{R}}$ for every $n\in\mathbb{N}_{0}$.