Predicative Formulas for Convergence and Limits, and Maps Defined by Limits

In the setting of The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness, with predicative meant for formulas with abbreviations, let $(X,d)$ be a metric space. The letters $s$, $z$, $z'$, $\varepsilon$, $N$ and $m$ are distinct set variables, and $X$, $d$, $\mathbb{N}$, $\mathbb{R}$ and the order $\le$, the strict order $<$ and the element $0$ of $\mathbb{R}$ are parameters. In the formula $\kappa$ below, $\le$, $<$ and $0$ are those of $\mathbb{R}$; on elements of $\mathbb{N}$, $\le$ agrees with the order of $\mathbb{N}_{0}$ by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §agreement.

¶ The formula $\kappa(s,z)$ below, $\mu$ being as in Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §map, is predicative; for sets $s$ and $z$ it holds if and only if $s$ is a sequence in $X$, $z\in X$ and $s$ converges to $z$ in $(X,d)$:

$$\mu(s,\mathbb{N},X)\wedge z\in X\wedge\forall\varepsilon\,((\varepsilon\in\mathbb{R}\wedge0<\varepsilon)\Rightarrow\exists N\,(N\in\mathbb{N}\wedge\forall m\,((m\in\mathbb{N}\wedge N\le m)\Rightarrow d(s(m),z)<\varepsilon))).$$

¶ The formula $\gamma(s)$, that is $\exists z\,\kappa(s,z)$, is predicative and holds if and only if $s$ is a sequence in $X$ convergent in $(X,d)$.

¶ Let $\upsilon(s)$ be the formula $\forall z\,\forall z'\,((\kappa(s,z)\wedge\kappa(s,z'))\Rightarrow z=z')$, where $\kappa(s,z')$ is $\kappa(s,z)$ with $z'$ put for $z$, and let $\gamma'(s)$ be $\gamma(s)\wedge\upsilon(s)$. Then $\kappa(s,z)$ and $\gamma'(s)$ are predicative, and for all values of the parameters and every set $s$ satisfying $\gamma'(s)$, exactly one set $z$ satisfies $\kappa(s,z)$. As $d$ is a metric on $X$, $\upsilon(s)$ holds for every set $s$, so that $\gamma'(s)$ holds if and only if $\gamma(s)$; and then that set $z$ is the limit $\lim s=\lim_{m\to\infty}s_{m}$. So $\lim s$ is a defined set symbol with argument $s$ given by $\kappa$, used properly where $\gamma(s)$ holds, and Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination applies to it with $\kappa$ as its $\theta$ and $\gamma'$ as its $\gamma$.

¶ For the distance $d_{\mathbb{R}}$ on $\mathbb{R}$, $(\mathbb{R},d_{\mathbb{R}})$ is a metric space, and for it $\kappa(s,z)$ holds if and only if $s$ is a sequence in $\mathbb{R}$ that converges to $z\in\mathbb{R}$; then $z=\lim s$, and $\lim s=\lim_{n\to\infty}s_{n}$ of The Limit of a Convergent Sequence §limit.

¶ For a set $a$ and an expression $t(u)$ as in Maps and Relations Given by Formulas §map that is a convergent sequence in $X$ for every $u\in a$, exactly one map $f:a\to X$ has $f(u)=\lim t(u)$ for every $u\in a$.