Proof of Kit for def:cauchy-sequence-nbg

Throughout, formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), and the given $x_{0},\dots,x_{n-1}$ are the first of distinct set variables $x_{0},x_{1},\dots$ as in Renaming and Substituting Variables in Predicative Formulas. The parameters are those of the statement, at their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i).

The formula for the Cauchy condition. Let $\varepsilon$, $N$, $m$ and $m'$ be distinct set variables, distinct from $x_{0},x_{1},\dots$ and from the parameters. Take the auxiliary set variables $p$, $u$, $u'$, $v$ and $v'$ of the formula $\mu$ of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii) pairwise distinct and distinct from $x_{0},x_{1},\dots$, from $\varepsilon$, $N$, $m$ and $m'$, and from the parameters; with $x_{0}$, $\mathbb{N}$ and $\mathbb{R}$ as its $F$, $A$ and $B$, this meets the distinctness hypotheses of that lemma. Let $\chi(x_{0})$ be the formula

$$\mu(x_{0},\mathbb{N},\mathbb{R})\wedge\forall\varepsilon\,\bigl((\varepsilon\in\mathbb{R}\wedge0<\varepsilon)\Rightarrow\exists N\,\bigl(N\in\mathbb{N}\wedge\forall m\,\forall m'\,\bigl((m\in\mathbb{N}\wedge m'\in\mathbb{N}\wedge N\le m\wedge N\le m')\Rightarrow d_{\mathbb{R}}(x_{0}(m),x_{0}(m'))<\varepsilon\bigr)\bigr)\bigr).$$

Its free variables are $x_{0}$ and the parameters $\mathbb{N}$, $\mathbb{R}$, $\le$, $<$, $0$ and $d_{\mathbb{R}}$.

Predicativity. The quantifiers of $\mu(x_{0},\mathbb{N},\mathbb{R})$ are over the set variables $p$, $u$, $u'$, $v$ and $v'$, and the remaining quantifiers $\forall\varepsilon$, $\exists N$, $\forall m$ and $\forall m'$ of $\chi$ are over set variables. Thus $\chi$ is written with ordered pairs, values (defined set symbols by Functions, Values of a Function, and Functions from One Class to Another (ii)) and the relation notation of Partial and Total Orders on a Set and the Associated Strict Relation (i) and Partial and Total Orders on a Set and the Associated Strict Relation (iii) only, and no quantifier is over a class variable, so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i).

Meaning. Let $x_{0}$ be a set. 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 (vii), $\mu(x_{0},\mathbb{N},\mathbb{R})$ holds if and only if $x_{0}$ is a map $x_{0}:\mathbb{N}\to\mathbb{R}$, that is, by Sequences (i), a sequence in $\mathbb{R}$. If $x_{0}$ is not a sequence in $\mathbb{R}$, then $\chi(x_{0})$ fails by its first conjunct, and $x_{0}$ is not a Cauchy sequence in $\mathbb{R}$. Let now $x_{0}$ be a sequence in $\mathbb{R}$, and let $m,m'\in\mathbb{N}$. Then

$$d_{\mathbb{R}}(x_{0}(m),x_{0}(m'))=|x_{0}(m)-x_{0}(m')|\in\mathbb{R}$$

by The Distance on the Real Numbers (i) (the values are used properly and lie in $\mathbb{R}$, as $x_{0}:\mathbb{N}\to\mathbb{R}$ and $d_{\mathbb{R}}:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$, these uses lying under the conjunct saying that $x_{0}$ is a map $\mathbb{N}\to\mathbb{R}$ and the antecedent $m\in\mathbb{N}\wedge m'\in\mathbb{N}\wedge N\le m\wedge N\le m'$, as Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (viii) requires). By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii), applied in turn to the values $x_{0}(m)$, $x_{0}(m')$ and $d_{\mathbb{R}}(x_{0}(m),x_{0}(m'))$, innermost first, each used properly there, and 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 (iii) for the ordered pairs, the part $d_{\mathbb{R}}(x_{0}(m),x_{0}(m'))<\varepsilon$ holds if and only if the real number $|x_{0}(m)-x_{0}(m')|$ is less than $\varepsilon$ in $\mathbb{R}$, and the parts $0<\varepsilon$, $N\le m$ and $N\le m'$ hold if and only if these relations hold in $\mathbb{R}$. (For $N,m,m'\in\mathbb{N}$, the order of $\mathbb{R}$ agrees with that of $\mathbb{N}_{0}$, The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (vi).) So the second conjunct of $\chi(x_{0})$ states that for every real $\varepsilon>0$ there is a natural number $N$ with

$$|x_{0}(m)-x_{0}(m')|<\varepsilon\qquad\text{for all }m,m'\in\mathbb{N}\text{ with }m,m'\ge N.$$

This is the condition of Cauchy Sequences of Real Numbers (i) for the sequence $x_{0}$, whose $m$-th term is $x_{0}(m)$. Hence, for every set $x_{0}$, $\chi(x_{0})$ holds if and only if $x_{0}$ is a Cauchy sequence in $\mathbb{R}$; so $\chi$ is a predicative formula in $x_{0}$ in the sense of Renaming and Substituting Variables in Predicative Formulas.

Cauchy sequences. By Renaming and Substituting Variables in Predicative Formulas (i) with $k=1$ and $\sigma(0)=i$, the formula $\chi(x_{i})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds, under every assignment of sets to $x_{0},\dots,x_{n-1}$, exactly when $x_{i}$ is a Cauchy sequence in $\mathbb{R}$. This proves (i).

The class. The Class Comprehension Theorem for Predicative Formulas (i), applied to the predicative formula $\chi(x_{0})$ in $x_{0}$ (the case $n=1$, $i=0$ above), with $x_{0}$ as its single variable and the parameters of the statement as its parameters, gives a class $K$ whose set elements are exactly the Cauchy sequences in $\mathbb{R}$, and since every element of a class and every Cauchy sequence in $\mathbb{R}$ is a set, this proves (ii) (the one-entry tuple $\langle a\rangle$ is $a$, The Ordered Pair of Two Sets and Nested Tuples (ii); elements of classes are sets, Classes, Membership, Sets and Proper Classes (i); a Cauchy sequence in $\mathbb{R}$, a map $\mathbb{N}\to\mathbb{R}$, lies in the class $\mathbb{R}^{\mathbb{N}}$ of functions from $\mathbb{N}$ to $\mathbb{R}$, as $\mathbb{N}$ and $\mathbb{R}$ are sets, The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)).