Proposition 3.33: recognizability closed under iteration

Read-back of MSKleene.rec_iter

Fix a type $S$ of sorts that is assumed to be a finite type, together with an $S$-sorted signature $\mathrm{sig}$ — a family assigning to every finite list of sorts $w\in\mathrm{List}(S)$ and every sort $s'\in S$ a type $\mathrm{sig}\,w\,s'$ of operation symbols of arity $w$ and result sort $s'$ (this family is not assumed finite) — and an $S$-sorted set of variables $X$, i.e. a family assigning to each sort $s'$ a type $X\,s'$ (also not assumed finite). Let $\mathrm{Term}(\mathrm{sig},X)$ be the $S$-sorted set of well-sorted first-order terms: for each $s'$, $\mathrm{Term}(\mathrm{sig},X)\,s'$ is generated by $\mathrm{var}(x)$ for $x\in X\,s'$ and by $\mathrm{app}(\sigma,\vec t\,)$ for $\sigma\in\mathrm{sig}\,w\,s'$ and $\vec t$ a vector of terms whose sorts match $w$. Let $\mathcal F:=\mathrm{freeAlgebra}(\mathrm{sig},X)$ be the algebra over $\mathrm{sig}$ whose carrier at each sort $s'$ is $\mathrm{Term}(\mathrm{sig},X)\,s'$ and whose interpretation of a symbol $\sigma$ is the term-forming map $\vec t\mapsto\mathrm{app}(\sigma,\vec t\,)$.

The theorem takes an implicit sort $s\in S$, an explicit distinguished variable $z\in X\,s$ (so $X\,s$ is inhabited), and an explicit set $L\subseteq\mathrm{Term}(\mathrm{sig},X)\,s$ of terms of sort $s$. Call a set $K$ of elements of $A_{\mathrm{carrier}}\,s'$ $s'$-recognizable in an algebra $A$ over $\mathrm{sig}$ when there exists an algebra $B$ over the same signature $\mathrm{sig}$ such that the dependent sum $\sum_{t\in S}B_{\mathrm{carrier}}\,t$ (the disjoint union of all its carrier sets over all sorts) is a finite type, and there exist a homomorphism $f:A\to B$ — a sort-indexed family of maps $f_t:A_{\mathrm{carrier}}\,t\to B_{\mathrm{carrier}}\,t$ satisfying $f_{s'}\big(A.\mathrm{op}(\sigma,\vec a\,)\big)=B.\mathrm{op}\big(\sigma,(f\text{ applied componentwise to }\vec a)\big)$ for every symbol $\sigma$ — and a subset $M\subseteq B_{\mathrm{carrier}}\,s'$, such that

The single hypothesis $hL$ states that $L$ is $s$-recognizable in $\mathcal F$ in precisely this sense; if no such $B,f,M$ exist for $L$, the hypothesis is false and the theorem asserts nothing about that $L$.

Next, let $\mathcal P(\mathcal F)$ be the power algebra: the algebra over $\mathrm{sig}$ whose carrier at sort $t$ is the powerset $\mathcal P\big(\mathrm{Term}(\mathrm{sig},X)\,t\big)$ and whose interpretation of a symbol $\sigma\in\mathrm{sig}\,w\,t$ sends a tuple of argument-sets $(K_1,\dots,K_n)$ to $\{\,\mathrm{app}(\sigma,(u_1,\dots,u_n)) : u_j\in K_j\text{ for every }j\,\}$. Let $h:=\mathrm{substHom}(z,L)$ be the homomorphism $\mathcal F\to\mathcal P(\mathcal F)$ obtained as the evaluation homomorphism induced by the variable assignment $\rho$ that sends the distinguished variable $z$ to the set $L$ and sends every other variable $y$ (every $y\in X\,s$ with $y\ne z$, and every variable of every sort $t\ne s$) to the singleton $\{\mathrm{var}(y)\}$. Unfolding term evaluation, for a term $P$ of sort $t$ the set $h_t(P)\subseteq\mathrm{Term}(\mathrm{sig},X)\,t$ is computed by structural recursion: $h_s(\mathrm{var}(z))=L$; $h_t(\mathrm{var}(y))=\{\mathrm{var}(y)\}$ for any other variable $y$; and $h_t(\mathrm{app}(\sigma,(P_1,\dots,P_n)))=\{\,\mathrm{app}(\sigma,(u_1,\dots,u_n)) : u_j\in h_{s_j}(P_j)\,\}$. Equivalently, $h_t(P)$ is the set of all terms obtained from $P$ by replacing each occurrence of $z$, independently, by some term of $L$; in particular if $z$ does not occur in $P$ then $h_t(P)=\{P\}$, and if $L=\varnothing$ then $h_s(\mathrm{var}(z))=\varnothing$. For a set $K$ of terms of sort $s$ define

Define the iteration stages by recursion on $i\in\mathbb N$:

and set

Thus stage $0$ is the singleton $\{\mathrm{var}(z)\}$; each next stage keeps everything from the previous stage and adds every term obtained by substituting members of $L$ for occurrences of $z$ in terms already present; and $\mathrm{iterate}(z,L)$ is the union of all these (nondecreasing) stages over every natural number $i$, including $i=0$ (so $\mathrm{var}(z)\in\mathrm{iterate}(z,L)$ always, and $\mathrm{iterate}(z,\varnothing)=\{\mathrm{var}(z)\}$).

Conclusion. Under all of the above, $\mathrm{iterate}(z,L)$ is $s$-recognizable in $\mathcal F$: there exist an algebra $B$ over the signature $\mathrm{sig}$ whose total carrier $\sum_{t\in S}B_{\mathrm{carrier}}\,t$ is a finite type, a homomorphism $f:\mathcal F\to B$, and a subset $M\subseteq B_{\mathrm{carrier}}\,s$ such that

The witnessing algebra $B$ is constrained only to be over the same signature $\mathrm{sig}$ and to have finite total carrier; it need not be related to $X$, to $\mathcal F$, or to the algebra witnessing $hL$ in any other way.