Proposition 3.30: recognizability closed under substitution

Read-back of MSKleene.rec_subst

Setting and fixed data. Let $S$ be a type (of sorts) that is assumed to be finite. A signature over $S$ is a family $sig$ that assigns to every finite list $w = (s_1,\dots,s_k)$ of sorts and every sort $s$ a type $sig(w,s)$ of operation symbols of arity $w$ and result sort $s$. Fix such a signature $sig$. Let $X$ be a sorted set of variables, i.e. a family assigning to each sort $s$ a type $X_s$; assume $X$ is sort-finite, meaning the dependent sum $\sum_{s : S} X_s$ (the type of all variables of all sorts together) is a finite type. Fix a sort $s$ (an implicit argument).

For each sort $t$, let $T_t := \mathrm{Term}(sig, X, t)$ be the inductively generated type of well-sorted terms of sort $t$: a term is either $\mathrm{var}(x)$ for a variable $x : X_t$, or $\sigma(t_1,\dots,t_k)$ for an operation symbol $\sigma : sig(w,t)$ with $w = (s_1,\dots,s_k)$ and terms $t_i : T_{s_i}$. Let $F := \mathrm{freeAlgebra}(sig, X)$ be the $sig$-algebra whose carrier at sort $t$ is $T_t$ and whose interpretation of an operation symbol $\sigma : sig(w,t)$ sends an argument tuple $\vec t$ to the formal term $\sigma(\vec t)$.

The recognizability predicate. For a $sig$-algebra $A$, a sort $t$, and a set $L \subseteq A_t$ (subset of the carrier of $A$ at sort $t$), the statement "$L$ is $t$-recognizable in $A$" means:

$$\exists\, B \text{ a } sig\text{-algebra},\quad \Big(\textstyle\sum_{s' : S} B_{s'} \text{ is a finite type}\Big) \;\wedge\; \exists\, f : A \to B,\ \exists\, M \subseteq B_t,\quad f_t^{-1}(M) = L,$$

where $f : A \to B$ is a homomorphism, that is, a sort-indexed family of maps $f_{s'} : A_{s'} \to B_{s'}$ satisfying $f_t\big(\mathrm{op}_A(\sigma)(\vec a)\big) = \mathrm{op}_B(\sigma)\big(f(\vec a)\big)$ for every operation symbol $\sigma$ and every argument tuple $\vec a$, and $f_t^{-1}(M)$ is the preimage of $M$ under $f_t$ at the single sort $t$. The equality $f_t^{-1}(M) = L$ is exact set equality. (Since $S$ is finite, finiteness of $\sum_{s'} B_{s'}$ forces each $B_{s'}$ to be finite.)

The power algebra and global substitution. Let $\mathcal{P}(F)$ be the $sig$-algebra whose carrier at sort $t$ is the powerset $\{\,L : L \subseteq T_t\,\}$, and whose interpretation of an operation symbol $\sigma : sig(w,t)$ with $w=(s_1,\dots,s_k)$ acts on a tuple of sets $(L_1,\dots,L_k)$ with $L_i \subseteq T_{s_i}$ by

$$\mathrm{op}_{\mathcal{P}(F)}(\sigma)(L_1,\dots,L_k) \;=\; \big\{\, \sigma(u_1,\dots,u_k) \;:\; u_i \in L_i \text{ for each } i \,\big\} \;\subseteq\; T_t .$$

Let $\rho$ be a sort-indexed family that assigns to each sort $t$ and each variable $x : X_t$ a set of terms $\rho_t(x) \subseteq T_t$. Let $\widehat{\rho} : F \to \mathcal{P}(F)$ be the evaluation homomorphism induced by $\rho$: it is the (structurally recursive) homomorphism determined by

$$\widehat{\rho}_t(\mathrm{var}(x)) = \rho_t(x), \qquad \widehat{\rho}_t\big(\sigma(t_1,\dots,t_k)\big) = \big\{\, \sigma(u_1,\dots,u_k) : u_i \in \widehat{\rho}_{s_i}(t_i) \,\big\}.$$

Thus for a single term $P : T_s$, $\widehat{\rho}_s(P) \subseteq T_s$ is the set of all terms obtained from $P$ by replacing each occurrence of each variable $x$ (of sort $t$) independently by some element of $\rho_t(x)$. For a set $K \subseteq T_s$, the global substitution is

$$\mathrm{substGlobalP}(\rho, s, K) \;=\; \bigcup_{P \in K} \widehat{\rho}_s(P) \;\subseteq\; T_s .$$

The assertion. Given:

• $K \subseteq T_s$, an arbitrary set of terms of sort $s$;
• a hypothesis $hK$ that $K$ is $s$-recognizable in $F$ (in the sense above, with $A := F$, $t := s$, $L := K$);
• the substitution family $\rho$ as above;
• a hypothesis $h\rho$ that for every sort $t : S$ and every variable $x : X_t$, the set $\rho_t(x) \subseteq T_t$ is $t$-recognizable in $F$;

the theorem concludes:

$$\mathrm{substGlobalP}(\rho, s, K) \text{ is } s\text{-recognizable in } F,$$

i.e. there exist a $sig$-algebra $B$ with $\sum_{s'} B_{s'}$ finite, a homomorphism $f : F \to B$, and a set $M \subseteq B_s$ such that $f_s^{-1}(M) = \bigcup_{P \in K} \widehat{\rho}_s(P)$. The algebra, homomorphism, and mask witnessing the conclusion are quantified anew and need not relate to those witnessing $hK$ or $h\rho$.

Edge cases. If $K = \varnothing$ the union is empty, so $\mathrm{substGlobalP}(\rho, s, K) = \varnothing$ and the conclusion holds trivially. If some $\rho_t(x) = \varnothing$, then any $P \in K$ in which the variable $x$ occurs contributes $\widehat{\rho}_s(P) = \varnothing$. The quantifier in $h\rho$ ranges over all sorts $t$, including those with $X_t$ empty (for which it is vacuous); if $X$ has no variables at all, $h\rho$ is vacuous, each $\widehat{\rho}_s(P) = \{P\}$, and the statement reduces to $hK$. The recognizability hypotheses $hK$ and $h\rho$ are genuine restrictions (not every subset of $T_t$ is $t$-recognizable). No finiteness assumption is placed on the signature $sig$; the standing assumptions are that $S$ is finite and that $\sum_{s} X_s$ is finite.