Corollary 3.31: single-variable substitution preserves recognizability

Proved

MSKleene.rec_subst_single

by Cosme · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

formal-languagesmany-sorted-algebratree-automatauniversal-algebra

Single-variable substitution preserves recognizability (Corollary 3.31).

Assume $S$ and $X$ finite. Let $s,t\in S$ , $z\in X_{t}$ , $L\in\mathrm{Rec}_{t}(\mathbf{T}_{\Sigma}(X))$ , and $K\in\mathrm{Rec}_{s}(\mathbf{T}_{\Sigma}(X))$ . Then $\left(\!\begin{smallmatrix}z\\L\end{smallmatrix}\!\right)^{\sharp\mathsf{p}}_{s}(K)\in\mathrm{Rec}_{s}(\mathbf{T}_{\Sigma}(X))$ . (From CVCL20, Cor. 3.20.)

Preamble

import Definitions.Def_MSKleene_Recognizable
import Definitions.Def_MSKleene_Subst

Formal statement

namespace MSKleene

/-- **Single-variable substitution preserves recognizability** (Corollary 3.31;
from CVCL20).

With `S` and `X` finite: for `z ∈ X_t`, if `L ⊆ T_Σ(X)_t` and `K ⊆ T_Σ(X)_s`
are recognizable, then `⟨z/L⟩^♯ᵖ_s(K)` is `s`-recognizable. -/
theorem rec_subst_single {S : Type} [Finite S] (sig : Signature S) (X : SSet S)
    (hX : SFinite X) {s t : S} (z : X t) (L : Set (Term sig X t))
    (K : Set (Term sig X s)) (hL : sRecognizable (freeAlgebra sig X) t L)
    (hK : sRecognizable (freeAlgebra sig X) s K) :
    sRecognizable (freeAlgebra sig X) s (substP z L s K) := by
  sorry

end MSKleene

Source

Gong, Ruiz Mora, Sanmartín Vich, Cosme Llópez, "A Kleene theorem for free many-sorted algebras", 2026

Read-back

What the Lean code literally says, in plain math · claude-sonnet-5

Fix a type $S$ of sorts, assumed finite, and a signature $\Sigma$ that assigns to every finite list $w=(s_1,\dots,s_n)$ of sorts and every sort $s$ a type $\Sigma_{w,s}$ of operation symbols ( $\Sigma$ is not assumed finite); fix also an $S$ -indexed family $X=(X_r)_{r\in S}$ of variable types, with the standing assumption $hX$ that the disjoint union $\coprod_{r\in S}X_r$ is finite. For each sort $r$ write $T_r$ for the type $\mathrm{Term}\,\Sigma\,X\,r$ of well-sorted terms of sort $r$ , generated inductively by $\mathrm{var}\colon X_r\to T_r$ and, for each $\sigma\in\Sigma_{w,s}$ , a former $\mathrm{app}(\sigma;-)$ taking a vector of subterms of sorts $s_1,\dots,s_n$ to a term of sort $s$ ; let $F$ be the free $\Sigma$ -algebra on $X$ , whose carrier at $r$ is $T_r$ and whose $\sigma$ -operation is $\mathrm{app}(\sigma;-)$ , and let $\mathcal P F$ be its power algebra, whose carrier at $r$ is the powerset $\mathcal P(T_r)$ and whose operation, for $\sigma\in\Sigma_{w,s}$ and a tuple $(U_1,\dots,U_n)$ with $U_i\subseteq T_{s_i}$ , is

\big\{\,\mathrm{app}(\sigma;x_1,\dots,x_n)\;:\;x_i\in U_i\text{ for every }i\,\big\}\subseteq T_s.

The theorem takes two implicit sorts $s,t\in S$ (which may be equal), a variable $z\in X_t$ , a set of terms $L\subseteq T_t$ , and a set of terms $K\subseteq T_s$ . From these define the assignment $\alpha$ sending each sort $r$ and variable $y\in X_r$ to the subset of $T_r$

\alpha_r(y)=\begin{cases}L,&\text{if }r=t\text{ and }y=z,\\[2pt]\{\mathrm{var}(y)\},&\text{otherwise,}\end{cases}

(the equality tests use classical decidability), and let $h\colon F\to\mathcal P F$ be the homomorphism evaluating terms in $\mathcal P F$ under $\alpha$ , i.e. the map defined by recursion on terms with $h_r(\mathrm{var}(y))=\alpha_r(y)$ and $h_s(\mathrm{app}(\sigma;p_1,\dots,p_n))=\{\mathrm{app}(\sigma;x_1,\dots,x_n):x_i\in h_{s_i}(p_i)\}$ ; the object under discussion is

\mathrm{substP}(z,L,s,K)\;=\;\bigcup_{P\in K}h_s(P)\;\subseteq\;T_s,

the union over all terms $P$ lying in $K$ of the set $h_s(P)\subseteq T_s$ . The predicate $\mathrm{sRecognizable}(A,r,L')$ , for a $\Sigma$ -algebra $A$ , a sort $r$ , and a set $L'\subseteq A_r$ (the carrier of $A$ at $r$ ), asserts that

\exists\,B\ \Sigma\text{-algebra with }\textstyle\coprod_{q\in S}B_q\text{ finite},\ \ \exists\,f\colon A\to B\ \Sigma\text{-homomorphism},\ \ \exists\,M\subseteq B_r,\qquad f_r^{-1}(M)=L',

that is, $L'=\{a\in A_r: f_r(a)\in M\}$ exactly. Under the hypotheses $hL$ , that $\mathrm{sRecognizable}(F,t,L)$ holds (some $\Sigma$ -algebra with finite total carrier, a homomorphism from $F$ into it, and a subset of its sort- $t$ carrier whose preimage under the homomorphism's sort- $t$ component is precisely $L$ ), and $hK$ , that $\mathrm{sRecognizable}(F,s,K)$ holds (the analogous statement for $K$ at sort $s$ ), the theorem concludes $\mathrm{sRecognizable}\big(F,\,s,\,\mathrm{substP}(z,L,s,K)\big)$ : there exist a $\Sigma$ -algebra $B$ with $\coprod_{q\in S}B_q$ finite, a $\Sigma$ -homomorphism $f\colon F\to B$ , and a set $M\subseteq B_s$ such that

\big\{\,P\in T_s\;:\;f_s(P)\in M\,\big\}\;=\;\bigcup_{P\in K}h_s(P).

Degenerate cases silently included: if $K=\varnothing$ then $\mathrm{substP}(z,L,s,K)=\varnothing$ and the assertion is that the empty subset of $T_s$ is recognizable; if $L=\varnothing$ then $\alpha_t(z)=\varnothing$ , so under $h$ every term that mentions $z$ evaluates to $\varnothing$ while every term not mentioning $z$ evaluates to its own singleton; $s$ and $t$ range over all sorts and may coincide; $S$ is finite and $\coprod_r X_r$ is finite, but no finiteness is imposed on $\Sigma$ ; and the hypotheses $hL$ and $hK$ are assumptions whose satisfiability is not addressed here.

Human review

Endorsed by Shuze Chen · Sep 9, 2026
Endorsed by Cosme · Sep 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph