Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let finite sets be as in Finite Sets §finite and $[n]$ as in Intervals of Natural Numbers §segment. All three clauses are statements of the metatheory. Formulas may be written with abbreviations, defined set symbols being used properly, and predicative is meant as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols; set variables, class variables and free variables are as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols, and sets and classes are assigned to them as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading.

¶ Let $z$ and $n$ be any distinct set variables and $Y$ and $R$ any distinct class variables, assigned $\mathbb{N}$ (as in The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets) and the order $\le$ of $\mathbb{N}_{0}$, respectively. There is a predicative formula $\mathrm{seg}(z,n)$, whose free variables are among $z$, $n$, $Y$ and $R$, such that for every set $z$ and every $n\in\mathbb{N}_{0}$, $\mathrm{seg}(z,n)$ holds if and only if $z=[n]$.

¶ Let $A$ be any set variable and $X$, $Y$ and $R$ any distinct class variables, assigned $\mathbb{N}_{0}$, $\mathbb{N}$ and the order $\le$ of $\mathbb{N}_{0}$, respectively. There is a predicative formula $\mathrm{fin}(A)$, whose free variables are among $A$, $X$, $Y$ and $R$, such that for every set $C$, $\mathrm{fin}(A)$ holds when $C$ is assigned to $A$ if and only if $C$ is finite.

¶ Let $A$ be any set variable. This clause asserts one statement for each predicative formula $\varphi$ having $A$ among its free variables; the other free variables of $\varphi$, of either kind, are its parameters, and for a set $C$, $\varphi(C)$ means that $\varphi$ holds when $C$ is assigned to $A$. For every assignment of values to the parameters: if $\varphi(\emptyset)$ holds, and $\varphi(C\cup\{x\})$ holds for every finite set $C$ with $\varphi(C)$ and every set $x\notin C$, then $\varphi(C)$ holds for every finite set $C$. Here $C$ and $x$ denote sets, not variables of $\varphi$.