Proof of Iterated Operations over Finite Sets Are Given by a Predicative Formula

Each result cited is universally quantified over the data in its own statement.

Conventions. 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, as The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §numbers-only requires. Let $w$, $C$, $g$, $X$, $F$, $Y$, $R$ and $P$ be as in the predicative clause, and let $t$, $n$, $z$, $d$, $a$, $k$, $u$ and $v$ be distinct set variables other than $w$, $C$ and $g$. 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 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 §operation-membership, each formula of the form $(s_{1},s_{2})\in s_{3}$ or $((s_{1},s_{2}),s_{3})\in s_{4}$ written below is predicative and, for sets assigned to the variables inside the pairs, holds if and only if the corresponding ordered pair is an element of the value of the variable to the right of $\in$; the elimination of the pairs introduces only bound variables, so its free variables are among the displayed ones. Here $s_{1}$, $s_{2}$, $s_{3}$ and $s_{4}$ are metavariables standing for variables of the formulas below, not themselves variables: in these formulas the variables inside the pairs are among the set variables $w$, $k$, $u$ and $v$, and the variable to the right of $\in$ ($s_{3}$ in the first form, $s_{4}$ in the second) is one of the set variables $d$, $g$ and $a$ or the class variable $F$.

The formula. Let $\varepsilon$ be $\forall t\,(t\notin C)$, and let $\nu$ be

$$w\in X\wedge\forall u\,\bigl(u\in X\Rightarrow(((w,u),u)\in F\wedge((u,w),u)\in F)\bigr).$$

Let $\mathrm{seg}(z,n)$ be a formula given by Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §segment for the set variables $z$, $n$ and the class variables $Y$, $R$; it is predicative with free variables among $z$, $n$, $Y$ and $R$. Let $\beta(d,z,C)$ 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 $d$, $z$ and $C$ in place of its variables $F$, $A$ and $B$, and let $\mu(a,z,X)$ 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 §map with $a$, $z$ and $X$ in place of $F$, $A$ and $B$, their bound set variables $p$, $u$, $u'$, $v$, $v'$ being chosen distinct from $w$, $C$, $g$, $n$, $z$, $d$ and $a$; by those clauses they are predicative, with free variables $d$, $z$, $C$ and $a$, $z$, $X$, respectively. Let $\mathrm{it}(w,n,a)$ be a formula given by Iterated Operations Are Given by a Predicative Formula §predicative for the set variables $w$, $n$, $a$ and the class variables $X$, $F$, $Y$, $R$, $P$; it is predicative with free variables among $w$, $n$, $a$, $X$, $F$, $Y$, $R$ and $P$. Let $\kappa$ be

$$\forall k\,\forall u\,\forall v\,\bigl(((k,u)\in d\wedge(u,v)\in g)\Rightarrow(k,v)\in a\bigr),$$

and let $\mathrm{fop}(w,C,g)$ be

$$(\varepsilon\wedge\nu)\vee\exists n\,\exists z\,\exists d\,\exists a\,\bigl(n\in Y\wedge\mathrm{seg}(z,n)\wedge\beta(d,z,C)\wedge\mu(a,z,X)\wedge\kappa\wedge\mathrm{it}(w,n,a)\bigr).$$

The parts $\mathrm{seg}(z,n)$, $\beta(d,z,C)$, $\mu(a,z,X)$, $\mathrm{it}(w,n,a)$ and the pair formulas are predicative, so they apply no quantifier to a class variable, and the rest adds only atomic formulas, connectives and quantifiers over set variables; so $\varepsilon$, $\nu$, $\kappa$ and $\mathrm{fop}(w,C,g)$ are 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 free variables of $\varepsilon$ are among $C$; those of $\nu$ among $w$, $X$ and $F$; those of $\kappa$ among $d$, $g$ and $a$; and so those of $\mathrm{fop}(w,C,g)$, in which $n$, $z$, $d$ and $a$ are bound, are among $w$, $C$, $g$, $X$, $F$, $Y$, $R$ and $P$.

Reading the parts. Now assign a set $X$, an associative and commutative binary operation $\ast$ on $X$ that has a neutral element, $\mathbb{N}$, $\le$ and $+$ to $X$, $F$, $Y$, $R$ and $P$; let $C$ be a finite set, let $g$ be a map from a set $E$ including $C$ to $X$, so that $\operatorname{dom}g=E$ by Functions, Values of a Function, and Functions from One Class to Another §map, $g$ 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 $E$ being a set, and every element of $C$ lies in $E$ by Subclasses and Subsets §subclass; and let $w$ be a set. Six facts are used.

(i) $\nu$ holds if and only if $w$ is a neutral element of $\ast$; and $\ast$ has exactly one neutral element $e$, by A Binary Operation Has at Most One Neutral Element §unique. Indeed, for $w,u\in X$, $((w,u),u)\in{\ast}$ if and only if $u=w\ast u$, and $((u,w),u)\in{\ast}$ if and only if $u=u\ast w$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §operation with $X$ and $\ast$ in place of $a$ and $\ast$; so $\nu$ says that $w\in X$ and $w\ast u=u=u\ast w$ for every $u\in X$, which is Associative and Commutative Binary Operations, and Neutral Elements §neutral.

(ii) $\varepsilon$ holds if and only if $C=\emptyset$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §empty.

(iii) For $n\in\mathbb{N}$ and all sets $z$, $d$ and $a$: $\mathrm{seg}(z,n)$ holds if and only if $z=[n]$, by Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §segment, as $n\in\mathbb{N}\subseteq\mathbb{N}_{0}$; $\beta(d,z,C)$ holds if and only if $d$ is a bijection from $z$ 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; and $\mu(a,z,X)$ holds if and only if $a$ is a map $a:z\to X$, 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 §map.

(iv) For $n\in\mathbb{N}$, $[n]$ is a set and $1\in[n]$. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment, $[n]=\{k\in\mathbb{N}:k\le n\}$, a set by Sets and Maps: Ordinary Notation §set-builder, and 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 lies in $[n]$ if and only if it lies in $\mathbb{N}$ and is $\le n$; here $1\in\mathbb{N}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets and $1\le n$ by Arithmetic and Order of the Natural Numbers §least.

(v) Let $n\in\mathbb{N}$, let $d$ be a map $d:[n]\to C$ and $a$ a map $a:[n]\to X$. Then $\kappa$ holds if and only if $a(k)=g(d(k))$ for every $k\in[n]$. By Functions, Values of a Function, and Functions from One Class to Another §map, $\operatorname{dom}d=\operatorname{dom}a=[n]$; so by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value, for all sets $k$, $u$ and $v$: $(k,u)\in d$ if and only if $k\in[n]$ and $u=d(k)$; $(k,v)\in a$ if and only if $k\in[n]$ and $v=a(k)$; and $(u,v)\in g$ if and only if $u\in E$ and $v=g(u)$. Moreover, for $k\in[n]$, $d(k)\in\operatorname{ran}d\subseteq C$ by Relations, Domain, Range, Inverse and Composition §range, Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction and Functions, Values of a Function, and Functions from One Class to Another §map, so $d(k)\in E$. If $\kappa$ holds and $k\in[n]$, put $u=d(k)$ and $v=g(u)$; then $(k,u)\in d$ and $(u,v)\in g$, so $(k,v)\in a$, that is, $a(k)=g(d(k))$. Conversely, if $a(k)=g(d(k))$ for every $k\in[n]$, and $(k,u)\in d$ and $(u,v)\in g$, then $k\in[n]$, $u=d(k)$ and $v=g(u)=a(k)$, so $(k,v)\in a$; thus $\kappa$ holds.

(vi) The restriction $g'=g|_{C}$ is a map $g':C\to X$ with $g'(x)=g(x)$ for every $x\in C$, and $\mathop{\ast}\limits_{x\in C}g(x)$ is the iterated operation of $g'$ over $C$ by Sums and Products over a Finite Set and over an Interval §subsets, $\ast$ having a neutral element. Indeed, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction, $g'$ is a function with domain $C\cap E$ and $g'(x)=g(x)$ for every $x\in C\cap E$; by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction a set lies in $C\cap E$ if and only if it lies in $C$ and in $E$, that is, if and only if it lies in $C$, so $C\cap E=C$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality. If a set $v$ lies in the range of $g'$, then $(x,v)\in g'$ for some set $x$ by Relations, Domain, Range, Inverse and Composition §range and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, so $x\in C$ and $v=g'(x)=g(x)$ by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value, and $g(x)\in\operatorname{ran}g\subseteq X$ by Relations, Domain, Range, Inverse and Composition §range, Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction and Functions, Values of a Function, and Functions from One Class to Another §map; so the range of $g'$ is included in $X$ by Subclasses and Subsets §subclass, and $g':C\to X$ by Functions, Values of a Function, and Functions from One Class to Another §map.

The case $C=\emptyset$. Then $\varepsilon$ holds by (ii), and $\mathop{\ast}\limits_{x\in C}g(x)=e$ by (vi) and Sums and Products over a Finite Set and over an Interval §empty. The second disjunct of $\mathrm{fop}(w,C,g)$ fails: otherwise there are sets $n$, $z$ and $d$ with $n\in\mathbb{N}$, $z=[n]$ and $d$ a bijection from $[n]$ onto $C$, by (iii); then $1\in[n]$ by (iv), and $d(1)\in C$ as in (v), contradicting $\varepsilon$. Hence $\mathrm{fop}(w,C,g)$ holds if and only if $\nu$ holds, that is, by (i), if and only if $w=e=\mathop{\ast}\limits_{x\in C}g(x)$.

The case $C\neq\emptyset$. Then $\varepsilon$ fails by (ii), so $\mathrm{fop}(w,C,g)$ holds if and only if its second disjunct does. Let $m=\#C$ be as in The Number of Elements of a Finite Set §cardinality; then $m\in\mathbb{N}$ by The Iterated Operation over a Finite Set Does Not Depend on the Enumeration §nonempty, and by (vi) and Sums and Products over a Finite Set and over an Interval §operation,

$$\mathop{\ast}\limits_{x\in C}g(x)=\mathop{\ast}\limits_{k=1}^{m}g'(\varphi(k))\qquad(1)$$

for every bijection $\varphi$ from $[m]$ onto $C$. Let $d$ be a bijection from $[m]$ onto $C$ and $a$ a map $a:[m]\to X$ with $a(k)=g(d(k))$ for every $k\in[m]$. Then $a(k)=g'(d(k))$ for $k\in[m]$, as $d(k)\in C$ (see (v)), so $a$ is the map $k\mapsto g'(d(k))$ on $[m]$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality, and $\mathop{\ast}\limits_{k=1}^{m}g'(d(k))$ is the iterated operation of $a$ by Iterated Operations: Finite Sums and Finite Products §iterated. Moreover $a|_{[m]}=a$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality, its domain being $[m]\cap[m]=[m]$ by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations and Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, so $\mathop{\ast}\limits_{k=1}^{m}a_{k}$ in the sense of Iterated Operations: Finite Sums and Finite Products §restriction is the same iterated operation. By Iterated Operations Are Given by a Predicative Formula §predicative, applied to $m$ and $a$, and by (1),

$$\mathrm{it}(w,m,a)\iff w=\mathop{\ast}\limits_{k=1}^{m}a_{k}=\mathop{\ast}\limits_{k=1}^{m}g'(d(k))=\mathop{\ast}\limits_{x\in C}g(x).\qquad(2)$$

If the second disjunct holds, there are sets $n$, $z$, $d$ and $a$ satisfying its six conjuncts. Then $n\in\mathbb{N}$, and by (iii) $z=[n]$, $d$ is a bijection from $[n]$ onto $C$ and $a$ is a map $a:[n]\to X$; by The Number of Elements of a Finite Set §cardinality, $n=m$, as $n\in\mathbb{N}_{0}$. By $\kappa$ and (v), $a(k)=g(d(k))$ for every $k\in[m]$; and $\mathrm{it}(w,m,a)$ holds, so $w=\mathop{\ast}\limits_{x\in C}g(x)$ by (2).

Conversely, let $w=\mathop{\ast}\limits_{x\in C}g(x)$. By The Number of Elements of a Finite Set §cardinality there is a bijection $d$ from $[m]$ onto $C$, and by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition and (vi) $a=g'\circ d$ is a map $a:[m]\to X$ with $a(k)=g'(d(k))=g(d(k))$ for every $k\in[m]$. Both $d$ and $a$ are functions whose domain is the set $[m]$, by Functions, Values of a Function, and Functions from One Class to Another §map and (iv), so they are sets by Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set §function-set. Take $m$, $[m]$, $d$ and $a$ for $n$, $z$, $d$ and $a$. Then $m\in\mathbb{N}$; $\mathrm{seg}([m],m)$, $\beta(d,[m],C)$ and $\mu(a,[m],X)$ hold by (iii); $\kappa$ holds by (v); and $\mathrm{it}(w,m,a)$ holds by (2). So the second disjunct, and hence $\mathrm{fop}(w,C,g)$, holds.

This proves the clause predicative.