Proof of Predicative Formulas for the Vocabulary of Finite Combinatorics, at Any Variable Positions

Throughout, "predicative" is meant as in the statement. Predicative conditions are closed under negation, conjunction, disjunction and quantification over a further set variable, and a condition equivalent to a predicative one under every assignment of sets is predicative. Each condition is first shown predicative with $x_{0},x_{1},x_{2}$ in place of $x_{i},x_{j},x_{k}$, auxiliary set variables $x_{3},x_{4},\dots$ being bound; the condition at $x_{i},x_{j},x_{k}$ then follows by Renaming and Substituting Variables in Predicative Formulas (i), with $\sigma(0)=i$, $\sigma(1)=j$, $\sigma(2)=k$, whether or not $i,j,k$ are distinct. A class $T$ is determined by its elements (Axiom of Extensionality for Classes), so "$x_{0}=T$" is equivalent to $\forall u\,(u\in x_{0}\Leftrightarrow u\in T)$ and is predicative once "$u\in T$" is. Formulas for pairs are those 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 (ii), 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) 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 (iv), and $\mu(F,A,B)$ 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 (vii).

Every element of a class is a set (Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i)); in particular the parameter $1$, the successor of $0$, is a set, as an element of $\mathbb{N}_{0}$. Segments and intervals are subsets of the set $\mathbb{N}_{0}$, and maps with a set as domain are sets (Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i), Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set (ii)), so the quantifiers below range over sets.

Complements ((xii)). By The Boolean Operations on Classes, Disjointness, and the Universal Class (i), $x_{0}=A\setminus x_{1}$ if and only if $\forall u\,(u\in x_{0}\Leftrightarrow(u\in A\wedge u\notin x_{1}))$, with the parameter $A$.

Images ((xi)). By The Image and the Preimage of a Class under a Class (i), $x_{0}=f[x_{1}]$ if and only if $\forall y\,(y\in x_{0}\Leftrightarrow\exists u\,(u\in x_{1}\wedge(u,y)\in f))$, with the parameter $f$.

Segments and intervals ((ii)). By the notation of the statement, $x_{0}=\{x_{1},\dots,x_{2}\}$ if and only if

$$\forall u\,\bigl(u\in x_{0}\Leftrightarrow(u\in\mathbb{N}_{0}\wedge(x_{1},u)\in{\le}\wedge(u,x_{2})\in{\le})\bigr),$$

with the parameters $\mathbb{N}_{0}$ and $\le$. Since $[m]=\{1,\dots,m\}$, the condition $x_{0}=[x_{1}]$ arises from this one by substituting the parameter $1$ for $x_{1}$ and $x_{1}$ for $x_{2}$; as $1$ is a set, it is predicative by Renaming and Substituting Variables in Predicative Formulas (iii).

Maps and bijections ((iv), (v)). $x_{0}:[x_{1}]\to x_{2}$ holds if and only if $\exists s\,(s=[x_{1}]\wedge\mu(x_{0},s,x_{2}))$, 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) and (ii); for a class $B$, the same with $\mu(x_{0},s,B)$ and the parameter $B$. Replacing $\mu(x_{0},s,x_{2})$ by 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 (x) gives the bijections.

Tuples ((iii)). By the description of $X^{m}$ in the statement, $x_{0}=X^{x_{1}}$ if and only if $\forall u\,(u\in x_{0}\Leftrightarrow u:[x_{1}]\to X)$, which is predicative by the second condition of (iv).

Finiteness and number of elements ((i)). "$x_{0}$ is finite" is predicative by Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (ii), with the parameters $\mathbb{N}_{0}$, $\mathbb{N}$ and $\le$. By Finite Sets (i) and The Number of Elements of a Finite Set (i), "$x_{1}$ is finite and $x_{0}=\#x_{1}$" holds if and only if $x_{0}\in\mathbb{N}_{0}$ and there is a bijection $F$ from $[x_{0}]$ onto $x_{1}$: such an $F$ makes $x_{1}$ finite, and $\#x_{1}$ is the only $m\in\mathbb{N}_{0}$ with a bijection from $[m]$ onto $x_{1}$. This is $x_{0}\in\mathbb{N}_{0}\wedge\exists x_{3}\,\beta$, with $\beta$ the predicative formula for "$x_{3}$ is a bijection from $[x_{0}]$ onto $x_{1}$" given by (v).

Iterated operations ((vi)). Let $\mathrm{it}(w,m,a)$ be the formula of Iterated Operations Are Given by a Predicative Formula (i) for $X$ and $\ast$, with the parameters $X$, $\ast$, $\mathbb{N}$, $\le$ and the addition of $\mathbb{N}_{0}$. For $x_{1}\in\mathbb{N}$ and a map $x_{2}:[x_{1}]\to X$, the restriction of $x_{2}$ to $[x_{1}]$ is $x_{2}$, so $\mathrm{it}(x_{0},x_{1},x_{2})$ holds if and only if $x_{0}=\mathop{\ast}\limits_{l=1}^{x_{1}}(x_{2})_{l}$; hence the first condition is equivalent to $x_{1}\in\mathbb{N}\wedge x_{2}:[x_{1}]\to X\wedge\mathrm{it}(x_{0},x_{1},x_{2})$, predicative by (iv). For the second, let $\mathrm{fop}(w,C,g)$ be the formula of Iterated Operations over Finite Sets Are Given by a Predicative Formula (i) for $X$ and $\ast$, with the same parameters. The map $a$, with domain the set $\mathbb{N}_{0}$, is a set, so by Renaming and Substituting Variables in Predicative Formulas (iii) the condition $\mathrm{fop}(x_{0},x_{3},a)$ with the parameter $a$ is predicative. For $x_{1},x_{2}\in\mathbb{N}_{0}$ the interval $\{x_{1},\dots,x_{2}\}$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (vii) and contained in the domain of $a$, so by Sums and Products over a Finite Set and over an Interval (iv) the condition is equivalent to

$$x_{1}\in\mathbb{N}_{0}\wedge x_{2}\in\mathbb{N}_{0}\wedge\exists x_{3}\,\bigl(x_{3}=\{x_{1},\dots,x_{2}\}\wedge\mathrm{fop}(x_{0},x_{3},a)\bigr),$$

predicative by (ii).

Operations over a finite set ((vii)). With $\mathrm{fop}$ as above, and $f$ a set as a map with the set $D$ as domain, the first condition is equivalent to "$x_{1}$ is finite" $\wedge\,\forall u\,(u\in x_{1}\Rightarrow u\in D)\wedge\mathrm{fop}(x_{0},x_{1},f)$, and the second to "$x_{1}$ is finite" $\wedge\,\mu(x_{2},x_{1},X)\wedge\mathrm{fop}(x_{0},x_{1},x_{2})$; both are predicative by (i) and Renaming and Substituting Variables in Predicative Formulas (iii).

Powers ((viii)). Let $R$ have multiplication $\cdot$ and one $1_{R}$, the neutral element of $\cdot$, and let $0_{\mathbb{N}_{0}}$ be the zero of $\mathbb{N}_{0}$. By Powers with Exponents in the Natural Numbers with Zero (ii), $x^{0_{\mathbb{N}_{0}}}=1_{R}$ for $x\in R$. For $m\in\mathbb{N}$, by Powers with Exponents in the Natural Numbers with Zero (i) and Iterated Operations: Finite Sums and Finite Products (i), $x^{m}=\prod_{l=1}^{m}x$ is the iterated operation of $\cdot$ along the map $c:[m]\to R$, $l\mapsto x$, whose elements are the pairs $(l,x)$ with $l\in[m]$. With $\mathrm{it}$ as above for $R$ and $\cdot$, and since an element of $\mathbb{N}_{0}$ other than $0_{\mathbb{N}_{0}}$ lies in $\mathbb{N}$ (The Set of Natural Numbers and the Number One (i)), the condition is therefore equivalent to $x_{1}\in R\wedge x_{2}\in\mathbb{N}_{0}$ and

$$(x_{2}=0_{\mathbb{N}_{0}}\wedge x_{0}=1_{R})\vee\Bigl(x_{2}\neq0_{\mathbb{N}_{0}}\wedge\exists c\,\bigl(\forall p\,(p\in c\Leftrightarrow\exists l\,(l\in[x_{2}]\wedge p=(l,x_{1})))\wedge\mathrm{it}(x_{0},x_{2},c)\bigr)\Bigr),$$

with the parameters $R$, $\cdot$, $0_{\mathbb{N}_{0}}$, $1_{R}$ and those of $\mathrm{it}$; it is predicative by (ii).

Binomial coefficients ((ix)). Let $C$ be the map named in The Binomial Coefficient (i), so that $\binom{m}{l}=C(m,l)$ for $m,l\in\mathbb{N}_{0}$. By Functions, Values of a Function, and Functions from One Class to Another (ii), the condition is equivalent to $x_{1}\in\mathbb{N}_{0}\wedge x_{2}\in\mathbb{N}_{0}\wedge((x_{1},x_{2}),x_{0})\in C$, with the parameters $\mathbb{N}_{0}$ and $C$.

Multinomial coefficients ((x)). Let $F:\mathbb{N}_{0}\to\mathbb{N}_{0}$ be the map $m\mapsto m!$. For $m\in\mathbb{N}$ and a map $q:[m]\to\mathbb{N}_{0}$, the class $g$ of pairs $(l,e)$ for which some $d$ has $(l,d)\in q$ and $(d,e)\in F$ is the map $[m]\to\mathbb{N}_{0}$, $l\mapsto q_{l}!$. By The Multinomial Coefficient (i), for $x_{1}\in\mathbb{N}$ and $x_{2}\in\mathbb{N}_{0}^{x_{1}}$, the set $x_{0}$ is the multinomial coefficient of $x_{2}$ if and only if $x_{0}\in\mathbb{N}_{0}$ and

$$x_{0}\cdot\prod_{l=1}^{x_{1}}(x_{2})_{l}!=\Bigl(\sum_{l=1}^{x_{1}}(x_{2})_{l}\Bigr)!.$$

Let $\mathrm{it}_{\cdot}$ and $\mathrm{it}_{+}$ be the formulas $\mathrm{it}$ for the multiplication and the addition of $\mathbb{N}_{0}$. The condition is then equivalent to $x_{1}\in\mathbb{N}\wedge x_{2}:[x_{1}]\to\mathbb{N}_{0}\wedge x_{0}\in\mathbb{N}_{0}$ (by Tuples in a Set: the Set of n-Tuples and Their Components (ii)) together with

$$\exists g\,\exists P\,\exists S\,\exists e\,\bigl(g=\{(l,e'):\exists d\,((l,d)\in x_{2}\wedge(d,e')\in F)\}\wedge\mathrm{it}_{\cdot}(P,x_{1},g)\wedge\mathrm{it}_{+}(S,x_{1},x_{2})\wedge(S,e)\in F\wedge((x_{0},P),e)\in{\cdot}\bigr),$$

where $P$ is the product, $S$ the sum and $e=S!$, by Functions, Values of a Function, and Functions from One Class to Another (ii); the equation for $g$ is handled through its elements as above. With the parameters $\mathbb{N}$, $\mathbb{N}_{0}$, $F$, the multiplication, the addition and $\le$, this is predicative by (iv).