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

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $n\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{n-1}$ be distinct set variables, and let $i,j,k<n$, not necessarily distinct. Each clause states that one or two conditions on $x_{0},\dots,x_{n-1}$ are predicative: expressed by a predicative formula, with $x_{0},\dots,x_{n-1}$ in place of the variables $x_{1},\dots,x_{N}$ of Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables. For sets $m$ and $m'$ we write

$$[m]=\{l\in\mathbb{N}_{0}:1\le l\le m\},\qquad\{m,\dots,m'\}=\{l\in\mathbb{N}_{0}:m\le l\le m'\},$$

with $\le$ the order of $\mathbb{N}_{0}$, and, for a class $X$, $X^{m}$ for the class of maps $u:[m]\to X$.

(i) Finiteness and number of elements. "$x_{i}$ is finite", and "$x_{j}$ is finite and $x_{i}=\#x_{j}$", with $\#$ the number of elements (the first condition restates Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (ii) at an arbitrary position).

(ii) Segments and intervals. "$x_{i}=[x_{j}]$", and "$x_{i}=\{x_{j},\dots,x_{k}\}$" (for $x_{j}\in\mathbb{N}_{0}$ the first condition restates Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (i) at arbitrary positions).

(iii) Tuples. For a class $X$: "$x_{i}=X^{x_{j}}$".

(iv) Maps from a segment. "$x_{i}$ is a map $x_{i}:[x_{j}]\to x_{k}$", and, for a class $B$, "$x_{i}$ is a map $x_{i}:[x_{j}]\to B$".

(v) Bijections from a segment. "$x_{i}$ is a bijection from $[x_{j}]$ onto $x_{k}$" (for $x_{j}\in\mathbb{N}_{0}$ this restates Predicative Formulas for Bijections from a Segment [n] and for Increasing Listings (i) at arbitrary positions).

(vi) Iterated operations. For a binary operation $\ast$ on a set $X$: "$x_{j}\in\mathbb{N}$, $x_{k}$ is a map $x_{k}:[x_{j}]\to X$, and $x_{i}$ is the iterated operation $\mathop{\ast}\limits_{l=1}^{x_{j}}(x_{k})_{l}$". If moreover $\ast$ is associative and commutative with a neutral element, then for a map $a:\mathbb{N}_{0}\to X$: "$x_{j},x_{k}\in\mathbb{N}_{0}$ and $x_{i}$ is the iterated operation over the interval $\mathop{\ast}\limits_{l=x_{j}}^{x_{k}}a_{l}$".

(vii) Operations over a finite set. Let $\ast$ be an associative and commutative binary operation on a set $X$ with a neutral element. For a map $f:D\to X$ on a set $D$: "$x_{j}$ is a finite subset of $D$ and $x_{i}$ is the iterated operation $\mathop{\ast}\limits_{y\in x_{j}}f(y)$"; and "$x_{j}$ is finite, $x_{k}$ is a map $x_{k}:x_{j}\to X$, and $x_{i}=\mathop{\ast}\limits_{y\in x_{j}}x_{k}(y)$".

(viii) Powers. For a commutative ring $R$: "$x_{j}\in R$, $x_{k}\in\mathbb{N}_{0}$ and $x_{i}=x_{j}^{x_{k}}$", the power for the multiplication of $R$ (this restates Powers with a Variable Base: a Predicative Formula and the Map (x, m) ↦ x^m (i) for that multiplication, at arbitrary positions).

(ix) Binomial coefficients. "$x_{j},x_{k}\in\mathbb{N}_{0}$ and $x_{i}$ is the binomial coefficient $\binom{x_{j}}{x_{k}}$".

(x) Multinomial coefficients. "$x_{j}\in\mathbb{N}$, $x_{k}\in\mathbb{N}_{0}^{x_{j}}$ and $x_{i}$ is the multinomial coefficient of the tuple $x_{k}$".

(xi) Images. For a class $f$: "$x_{i}=f[x_{j}]$", the image of $x_{j}$ under $f$.

(xii) Complements. For a class $A$: "$x_{i}=A\setminus x_{j}$", the difference.