Corollary 3.32: operation symbols preserve recognizability

Fix a type $S$ of sorts together with an instance witnessing that $S$ is a finite type. Let $\mathrm{sig}$ be a signature over $S$: for every list of sorts $w\in\mathrm{List}\,S$ and every sort $s\in S$, $\mathrm{sig}(w,s)$ is a type whose elements are the operation symbols of input profile $w$ and output sort $s$. (No hypothesis asserts that the total collection of operation symbols is finite.) Let $X$ be a sorted set of variables, i.e. a family $(X_s)_{s\in S}$ of types, and assume $hX:\mathrm{SFinite}\,X$, meaning the dependent sum $\sum_{s\in S}X_s$ is a finite type (finitely many variables in total).

Write $T=\mathrm{freeAlgebra}\,\mathrm{sig}\,X$ for the term algebra: its carrier at sort $s$ is the inductive type $\mathrm{Term}(\mathrm{sig},X)_s$ of well-sorted terms, each of which is either a variable $\mathrm{var}(x)$ with $x\in X_s$ or an application $\mathrm{app}\,\tau\,(t_1,\dots,t_k)$ with $\tau\in\mathrm{sig}(v,s)$ and the $t_j$ terms of the sorts listed in $v$; the operation of $T$ interpreting a symbol $\tau$ on an argument tuple is the formal term $\mathrm{app}\,\tau$ applied to that tuple.

Fix an implicit list of sorts $w=[s_1,\dots,s_n]$ and an implicit sort $s$, and let $\sigma\in\mathrm{sig}(w,s)$ be an operation symbol. Let $Ls=(L_1,\dots,L_n)$ be a tuple indexed by $w$ whose $i$-th component is a set of terms of sort $s_i$, i.e. $L_i\subseteq\mathrm{Term}(\mathrm{sig},X)_{s_i}$; when $n=0$ this tuple is empty.

The hypothesis $hLs$ states that every component is recognizable in $T$: for each $i\in\{1,\dots,n\}$, $\mathrm{sRecognizable}\,T\,s_i\,L_i$ holds (for $n=0$ this hypothesis is the vacuously true empty conjunction). Here $\mathrm{sRecognizable}\,A\,\hat s\,L$ means that there exists a $\mathrm{sig}$-algebra $B$ such that:

• $B$ is finite, i.e. $\sum_{s'\in S}B.\mathrm{carrier}_{s'}$ is a finite type; and
• there exist an algebra homomorphism $f:A\to B$ — a sortwise family of maps $f_{s'}:A.\mathrm{carrier}_{s'}\to B.\mathrm{carrier}_{s'}$ satisfying, for all $v,s',\tau\in\mathrm{sig}(v,s')$ and all argument tuples $a$, the equation $f_{s'}\big(A.\mathrm{op}\,\tau\,a\big)=B.\mathrm{op}\,\tau\,\big(a\text{ with }f\text{ applied componentwise}\big)$ — together with a subset $M\subseteq B.\mathrm{carrier}_{\hat s}$;
• such that $f_{\hat s}^{-1}(M)=L$ as sets, i.e. for every $x\in A.\mathrm{carrier}_{\hat s}$ one has $x\in L\iff f_{\hat s}(x)\in M$.

The conclusion is $\mathrm{sRecognizable}\,T\,s\,\big(\mathrm{powerOp}\,T\,\sigma\,Ls\big)$, where

that is, the set of all terms of sort $s$ of the form $\sigma(t_1,\dots,t_n)$ obtained by choosing one term $t_i\in L_i$ from each component.

In words: assuming $S$ is finite, the variable family $X$ has finitely many elements in total, and every $L_i$ is recognizable in the term algebra $T$, the theorem asserts that the "elementwise $\sigma$-application" set $\{\sigma(t_1,\dots,t_n)\mid t_i\in L_i\text{ for all }i\}$ is again recognizable in $T$ — i.e. there exist a finite $\mathrm{sig}$-algebra $B$, a homomorphism $f:T\to B$, and a subset $M\subseteq B.\mathrm{carrier}_s$ whose preimage under $f_s$ is exactly that set. In the degenerate case $n=0$, $\sigma$ is a constant symbol, the hypothesis $hLs$ carries no content, and the claim reduces to: the singleton set $\{\mathrm{app}\,\sigma\,()\}$ consisting of the single constant term is recognizable in $T$.