Toolkit for AL1

In the setting of Groups: Standing Notation: for classes $D$ and $F$, $F|_{D}$ is the restriction of $F$ to $D$. For a binary operation $\cdot$ on a set $X$, $n\in\mathbb{N}$ and a map $a$ from a set containing $[n]$ to $X$, $\prod_{k=1}^{n}a(k)$ is as in Iterated Operations: Finite Sums and Finite Products (ii), and $\prod_{k=1}^{n}t$ for an expression $t$ in $k$ as in Iterated Operations: Finite Sums and Finite Products (i); for $x\in X$ and $n\in\mathbb{N}_{0}$, $x^{n}$ is the power of Powers with Exponents in the Natural Numbers with Zero (i) and, when $\cdot$ has a neutral element, of Powers with Exponents in the Natural Numbers with Zero (ii). $\mathbb{Z}$ is the set of integers, with the sum $+$ and the product $\cdot$ of The Integers (iii). In the four clauses on predicative conditions, a condition on a set variable $x_{0}$ is expressed by a predicative formula as in Conditions Expressed by a Predicative Formula, and Guards (i) with $k=1$, $x_{1}=x_{0}$ and no displayed variables, its parameters being $M$, the operation of $M$, the elements of $M$ and of $\mathbb{N}_{0}$ named in the clause, $\mathbb{N}_{0}$, the multiplication of $\mathbb{N}_{0}$, and the map $p:M\times\mathbb{N}_{0}\to M$, $p(x,m)=x^{m}$, of Powers with a Variable Base: a Predicative Formula and the Map (x, m) ↦ x^m (ii).

(i) Reflexivity of inclusion. Every set $A$ is a subset of itself: $A\subseteq A$.

(ii) A class with an element is not empty. If $g$ is an element of a class $H$, then $H\neq\emptyset$.

(iii) Disjoint classes. If $X$ and $Y$ are disjoint classes, then $X\cap Y=\emptyset$.

(iv) Restricted operations. Let $\ast$ be a binary operation on a set $M$, and let $S\subseteq M$ be a class with $u\ast v\in S$ for all $u,v\in S$. Then $\ast|_{S\times S}$ is a binary operation on $S$.

(v) Values of a restricted operation. Let $\ast$ be a binary operation on a set $M$, let $S\subseteq M$ be a class, and let $u,v\in S$. Then

$$(\ast|_{S\times S})((u,v))=u\ast v .$$

(vi) Associativity passes to a restriction. Let $\ast$ be an associative binary operation on a set $M$, and let $S\subseteq M$ be a class with $u\ast v\in S$ for all $u,v\in S$. Then $\ast|_{S\times S}$ is an associative binary operation on $S$.

(vii) Neutral elements pass to a restriction. Let $\ast$ be a binary operation on a set $M$ with a neutral element $e$, and let $S\subseteq M$ be a class with $e\in S$ and $u\ast v\in S$ for all $u,v\in S$. Then $\ast|_{S\times S}$ is a binary operation on $S$ with neutral element $e$.

(viii) Positive powers. Let $\cdot$ be a binary operation on a set $X$, let $x\in X$ and let $n\in\mathbb{N}$. Then

$$x^{n}=\prod_{k=1}^{n}x .$$

(ix) Positive powers as products of a constant list. Let $\cdot$ be a binary operation on a set $X$, let $x\in X$ and let $n\in\mathbb{N}$. Then $x^{n}$ is the iterated operation of the constant map $[n]\times\{x\}:[n]\to X$:

$$x^{n}=\prod_{k=1}^{n}\bigl([n]\times\{x\}\bigr)(k).$$

(x) The zeroth power. Let $\cdot$ be a binary operation on a set $X$ with a neutral element $e$, and let $x\in X$. Then $x^{0}=e$.

(xi) Restriction to a shorter segment. Let $\cdot$ be a binary operation on a set $X$, let $x\in X$ and let $n\in\mathbb{N}$. Then

$$\prod_{k=1}^{n}\bigl([n+1]\times\{x\}\bigr)(k)=\prod_{k=1}^{n}\bigl([n]\times\{x\}\bigr)(k).$$

(xii) Shifted segments. Let $\cdot$ be a binary operation on a set $X$, let $x\in X$ and let $n,m\in\mathbb{N}$. Then $([m]\times\{x\})(j)=([n+m]\times\{x\})(n+j)$ for every $j\in[m]$, and

$$\prod_{k=1}^{n}\bigl([n+m]\times\{x\}\bigr)(k)=\prod_{k=1}^{n}\bigl([n]\times\{x\}\bigr)(k).$$

(xiii) Powers lie in the monoid. Let $(M,\cdot)$ be a monoid, let $x\in M$ and let $n\in\mathbb{N}_{0}$. Then $x^{n}\in M$.

(xiv) The condition $w^{x_{0}}=u^{a x_{0}}$ is predicative. Let $(M,\cdot)$ be a monoid, let $u,w\in M$ and let $a\in\mathbb{N}_{0}$. Then the condition "if $x_{0}\in\mathbb{N}_{0}$, then $w^{x_{0}}=u^{a x_{0}}$" on $x_{0}$ is expressed by a predicative formula.

(xv) The condition $u^{x_{0}}=c$ is predicative. Let $(M,\cdot)$ be a monoid and let $u,c\in M$. Then the condition "if $x_{0}\in\mathbb{N}_{0}$, then $u^{x_{0}}=c$" on $x_{0}$ is expressed by a predicative formula.

(xvi) The condition $u^{x_{0}}v=vu^{x_{0}}$ is predicative. Let $(M,\cdot)$ be a monoid and let $u,v\in M$. Then the condition "if $x_{0}\in\mathbb{N}_{0}$, then $u^{x_{0}}v=vu^{x_{0}}$" on $x_{0}$ is expressed by a predicative formula.

(xvii) The condition $w^{x_{0}}=u^{x_{0}}v^{x_{0}}$ is predicative. Let $(M,\cdot)$ be a monoid and let $u,v,w\in M$. Then the condition "if $x_{0}\in\mathbb{N}_{0}$, then $w^{x_{0}}=u^{x_{0}}v^{x_{0}}$" on $x_{0}$ is expressed by a predicative formula.

(xviii) The class of remainders. Let $f:\mathbb{N}_{0}\to\mathbb{Z}$ be a map, let $c\in\mathbb{Z}$ and let $m$ be a class. Then there is a class $S$ such that, for every set $r$,

$$r\in S\iff r\in\mathbb{N}_{0}\ \text{and}\ m=q\cdot c+f(r)\ \text{for some}\ q\in\mathbb{Z}.$$

(xix) The relation of lying in a common left coset. Let $G$ be a group and let $H\le G$. Then there is a class $R$ such that, for every set $p$,

$$p\in R\iff p=(g,k)\ \text{for some}\ g,k\in G\ \text{with}\ g^{-1}k\in H.$$