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

Each result cited below is universally quantified over the data in its own statement, and is applied to the data named where it is cited.

Segments. This proof concerns formulas of class theory: elements of $\mathbb{N}_{0}$ are assigned to set variables and are read as sets only in that sense, and in the formulas below a variable to which a number is assigned occurs only to the left of $\in$ or as a component of an ordered pair. For $n\in\mathbb{N}_{0}$, $[n]=\{k\in\mathbb{N}:k\le n\}$ and $[0]=\emptyset$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment; so, by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, a set $w$ lies in $[n]$ if and only if $w\in\mathbb{N}$ and $w\le n$, and $[n]$ is a set by Sets and Maps: Ordinary Notation §set-builder. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §successor, $[n+1]=[n]\cup\{n+1\}$ and $n+1\notin[n]$.

The formula seg. Let $z$, $n$, $Y$ and $R$ be as in the segment clause, let $w$ be a set variable other than $z$ and $n$, and let $\mathrm{seg}(z,n)$ be the formula

$$\forall w\,\bigl(w\in z\Leftrightarrow(w\in Y\wedge(w,n)\in R)\bigr),$$

where $(w,n)\in R$ is the formula 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 §pair-membership with $R$, $w$ and $n$ in place of $s$, $t_{1}$ and $t_{2}$. That formula is predicative by the same clause, with free variables among $w$, $n$ and $R$ (the elimination of the pair introduces only bound variables), so it applies no quantifier to a class variable; $\mathrm{seg}(z,n)$ adds only atomic formulas, connectives and a quantifier over the set variable $w$, so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure, no quantifier being applied to a class variable, and its free variables are among $z$, $n$, $Y$ and $R$. Now let $Y$ and $R$ be assigned $\mathbb{N}$ and $\le$, let $z$ be a set and $n\in\mathbb{N}_{0}$. For every set $w$, $(w,n)\in R$ holds if and only if $(w,n)\in{\le}$, 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 §pair-membership, that is, if and only if $w\le n$, by The Order on Omega §order. Hence $\mathrm{seg}(z,n)$ holds if and only if every set $w$ satisfies $w\in z\Leftrightarrow w\in[n]$, which by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality holds if and only if $z=[n]$. This proves the segment clause.

The formula fin. Let $A$, $X$, $Y$ and $R$ be as in the predicative clause, let $n$, $z$, $w$ and $f$ be distinct set variables other than $A$, let $\mathrm{seg}(z,n)$ be the formula of the preceding paragraph, built with these $z$, $n$, $w$, $Y$ and $R$, and let $\beta(f,z,A)$ be the formula 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 §bijective with $f$, $z$ and $A$ in place of its variables $F$, $A$ and $B$, respectively, its bound set variables $p$, $u$, $u'$, $v$, $v'$ being chosen distinct from $f$, $z$, $A$ and $n$. By that clause $\beta(f,z,A)$ is predicative, its free variables are $f$, $z$ and $A$, and for sets $g$, $c$ and $C$ it holds if and only if $g$ is a bijection from $c$ onto $C$. Let $\mathrm{fin}(A)$ be the formula

$$\exists n\,\exists z\,\exists f\,\bigl(n\in X\wedge\mathrm{seg}(z,n)\wedge\beta(f,z,A)\bigr).$$

Its parts $\mathrm{seg}(z,n)$ and $\beta(f,z,A)$ are predicative, so they apply no quantifier to a class variable, and it adds only an atomic formula, connectives and quantifiers over set variables; so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure, no quantifier being applied to a class variable, and its free variables are among $A$, $X$, $Y$ and $R$. Assign $\mathbb{N}_{0}$, $\mathbb{N}$ and $\le$ to $X$, $Y$ and $R$ and a set $C$ to $A$. If $C$ is finite, Finite Sets §finite gives $n\in\mathbb{N}_{0}$ and a bijection $g$ from $[n]$ onto $C$; its domain is the set $[n]$ by Functions, Values of a Function, and Functions from One Class to Another §map, so $g$ is a set by Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set §function-set, and the sets $n$, $[n]$ and $g$ witness $\mathrm{fin}(A)$, by the segment clause and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §bijective. Conversely, if $\mathrm{fin}(A)$ holds, there are sets $n\in\mathbb{N}_{0}$, $z$ and $g$ with $\mathrm{seg}(z,n)$ and $\beta(g,z,C)$; then $z=[n]$ by the segment clause and $g$ is a bijection from $[n]$ onto $C$ 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 §bijective, so $C$ is finite by Finite Sets §finite. This proves the clause predicative.

The class of the induction. Let $\varphi$ be as in the induction clause, fix values of its parameters, and assume its two hypotheses. Choose distinct set variables $n$, $z$, $f$, $w$ and distinct class variables $Y$, $R$, none of these six occurring in $\varphi$ (in particular each set variable among them differs from $A$); the two preceding paragraphs hold for this choice, giving $\mathrm{seg}(z,n)$ and $\beta(f,z,A)$. Let $\psi(n)$ be the formula

$$\forall z\,\forall f\,\forall A\,\bigl((\mathrm{seg}(z,n)\wedge\beta(f,z,A))\Rightarrow\varphi\bigr).$$

The formulas $\mathrm{seg}(z,n)$, $\beta(f,z,A)$ and $\varphi$ are predicative, so they apply no quantifier to a class variable, and $\psi(n)$ adds only connectives and quantifiers over set variables; so $\psi(n)$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure, no quantifier being applied to a class variable. The quantifier $\forall A$ binds the variable $A$ of $\varphi$; as $n$, $z$ and $f$ do not occur in $\varphi$, no other free variable of $\varphi$ is captured, and the free variables of $\psi(n)$ are among $n$, $Y$, $R$ and the parameters of $\varphi$. As $Y$ and $R$ do not occur in $\varphi$, they are not parameters of $\varphi$: assign $\mathbb{N}$ and $\le$ to $Y$ and $R$, and keep the fixed values of the parameters of $\varphi$. By Sets and Maps: Ordinary Notation §set-builder and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction there is the class $K=\{n:\psi(n)\}$, and a set $n$ lies in $K$ if and only if $\psi(n)$ holds. For $n\in\mathbb{N}_{0}$, by the segment clause and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §bijective, $\psi(n)$ says that $\varphi(D)$ holds for every set $D$ and every bijection from $[n]$ onto $D$ that is a set; and every bijection from $[n]$ onto $D$ is a set by Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set §function-set, its domain being the set $[n]$. So $n\in K$ if and only if $\varphi(D)$ holds for every set $D$ admitting a bijection from $[n]$ onto $D$.

Base. Let $g$ be a bijection from $[0]=\emptyset$ onto a set $D$. If $d\in D$, then by Injective, Surjective and Bijective Functions between Classes §surjective there is $u\in[0]$ with $g(u)=d$, which is impossible; so no set is an element of $D$, and $D=\emptyset$ by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §empty. Then $\varphi(D)$ is the hypothesis $\varphi(\emptyset)$. Hence $0\in K$.

Step. Let $n\in\mathbb{N}_{0}$ with $n\in K$, and let $g$ be a bijection from $[n+1]$ onto a set $D$. As $[n+1]=[n]\cup\{n+1\}$, $n+1\in[n+1]$ and $[n]\subseteq[n+1]$; put $a=g(n+1)\in D$ and let $D'=g[[n]]$ be the image, a set by Sets and Maps: Ordinary Notation §images. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction, $h=g|_{[n]}$ is a function with domain $[n]\cap[n+1]=[n]$ and $h(u)=g(u)$ for $u\in[n]$. By The Image and the Preimage of a Class under a Class §image, a set $v$ lies in $D'$ if and only if $v=g(u)$ for some $u\in[n]$; so every value of $h$ lies in $D'$, making $h$ a map $h:[n]\to D'$ by Functions, Values of a Function, and Functions from One Class to Another §map, and $h$ is surjective onto $D'$; it is injective because $g$ is. Thus $h$ is a bijection from $[n]$ onto $D'$, so $D'$ is finite by Finite Sets §finite, and $\varphi(D')$ holds because $n\in K$. If $a\in D'$, then $a=g(u)$ for some $u\in[n]$, and $u=n+1$ by injectivity of $g$, contradicting $n+1\notin[n]$; so $a\notin D'$. Every element of $D'$ is a value of $g$, hence lies in $D$, and $a\in D$; conversely every $d\in D$ is $g(u)$ for some $u\in[n+1]=[n]\cup\{n+1\}$ by surjectivity, so $d\in D'$ or $d=a$. Hence $D=D'\cup\{a\}$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality. The second hypothesis of the induction clause, applied to the finite set $D'$ with $\varphi(D')$ and to the set $a\notin D'$, gives $\varphi(D'\cup\{a\})$, that is, $\varphi(D)$. Hence $n+1\in K$.

Conclusion. By The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, $\mathbb{N}_{0}$ is the set $\omega$ of The Class Omega of Natural Numbers with Zero §omega, and the successor $S(n)$ of each $n\in\mathbb{N}_{0}$ is $n+1$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §plus-one; so $K$ satisfies the hypotheses of Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §induction, which gives $\mathbb{N}_{0}\subseteq K$. Finally, if $C$ is finite, Finite Sets §finite gives $n\in\mathbb{N}_{0}$ and a bijection from $[n]$ onto $C$; as $n\in K$, $\varphi(C)$ holds. This proves the induction clause.