Proposition 3.29: basic terms are recognizable

Fix a type $S$ carrying a Finite instance (so $S$ has only finitely many elements), a signature $\Sigma$ over $S$ — that is, an assignment of a type $\Sigma(w,s)$ of operation symbols to each pair consisting of a word $w\in\operatorname{List}(S)$ (the input profile) and a sort $s\in S$ (the output sort) — an $S$‑sorted family of variable types $X=(X_{s'})_{s'\in S}$, and a distinguished sort $s\in S$. Let $T_{\Sigma,X}=(T_{\Sigma,X,s'})_{s'\in S}$ be the $S$‑sorted set of terms: $T_{\Sigma,X,s'}$ is inductively generated by term‑variables $\operatorname{var}(x)$ for $x\in X_{s'}$ and by applications $\operatorname{app}(\sigma,\vec t)$ where, for some word $w=[w_1,\dots,w_n]$, $\sigma\in\Sigma(w,s')$ and $\vec t$ is a vector holding one term of sort $w_i$ in position $i$. Let $F$ be the term (free) algebra on $\Sigma$ and $X$: its carrier at sort $s'$ is $T_{\Sigma,X,s'}$, and its interpretation of a symbol $\sigma\in\Sigma(w,s')$ maps an argument vector $\vec t$ to the term $\operatorname{app}(\sigma,\vec t)$. For a $\Sigma$‑algebra $A$, a sort $s'$, and a set $L\subseteq A_{s'}$, call $L$ $s'$‑recognizable in $A$ when there exist (i) a $\Sigma$‑algebra $B$ whose total carrier $\sum_{s''\in S} B_{s''}$ is a finite type, (ii) a $\Sigma$‑homomorphism $f\colon A\to B$, i.e. a family of maps $f_{s''}\colon A_{s''}\to B_{s''}$ such that for every $w$, every $s''$, every $\sigma\in\Sigma(w,s'')$ and every argument vector $\vec a$ one has $f_{s''}\!\big(\sigma^{A}(\vec a)\big)=\sigma^{B}\!\big(f\text{ applied componentwise to }\vec a\big)$, and (iii) a set $M\subseteq B_{s'}$, such that $f_{s'}^{-1}(M)=L$ exactly (equality of sets, not mere inclusion). The theorem asserts the conjunction of the following two statements, in which the algebra $B$, the homomorphism $f$ and the set $M$ witnessing recognizability may be chosen independently for each instance:

where in (2) the single term named is the application of $\sigma$ directly to the variable terms $\operatorname{var}(x_i)$ as its immediate subterms. Edge cases folded into the quantifiers: in (1), if $X_s$ is empty the claim is vacuous; in (2), the quantifier over $(x_1,\dots,x_n)$ ranges over the sorted tuple type $X_{w_1}\times\cdots\times X_{w_n}$, which is empty (making that instance vacuous) whenever $w$ is nonempty and some $X_{w_i}$ is empty, and the quantifier over $\sigma$ contributes nothing when $\Sigma(w,s)$ is empty; when $w=[\,]$ the symbol $\sigma\in\Sigma([\,],s)$ is a constant, the tuple $(x_1,\dots,x_n)$ is the unique element of a one‑point type, and (2) asserts that the singleton $\{\operatorname{app}(\sigma,(\,))\}$ containing the constant term is $s$‑recognizable in $F$. No finiteness is assumed of the signature $\Sigma$ or of the variable family $X$; the only finiteness hypotheses are that $S$ is finite and that each recognizing algebra $B$ has finite total carrier.