Formal term substitutions do correspond to actual function substitutions

Question

Let $t(x_{1},...,x_{m})$ and $\tau_{1} (y_{1},...y_{n}),...,\tau _{m}(y_{1},...y_{n})$ be L-terms. Then the L-term $ t^{*}(y_{1},...y_{n}):=t(\tau_{1} (y_{1},...y_{n}),...,\tau _{m}(y_{1},...y_{n}))$ has the property that if $\mathcal A$ is an L-structure and $a=(a_{1},...,a_{n})\in A^{n}$, then
$(t^{*})^{\mathcal A}(a)=t^{\mathcal A}(\tau_{1}^{\mathcal A}(a),...,\tau_{m}^{\mathcal A}(a))$.

For solving this problem I had this following approach.
Let $t=t(x_{1},...,x_{m})=Fs_{1}(x_{1},...x_{m})...s_{k}(x_{1},...x_{m})$, then $t^{\mathcal A}(b_{1},...,b_{m})=F^{\mathcal A}(s_{1}^{\mathcal A}(b_{1},...b_{m})...s_{k}^{\mathcal A}(b_{1},...b_{m}))$ for all $(b_{1},...b_{m})\in A^m$. Now we substitute $\tau _{i}^{\mathcal A}(a)$ in $b_{i}$ for all $i$, where $a\in A^{n}$. So we have
$a_{0}:=t^{\mathcal A}(\tau _{1}^{\mathcal A}(a),...,\tau _{m}^{\mathcal A}(a))=F^{\mathcal A}(s_{1}^{\mathcal A}(\tau _{1}^{\mathcal A}(a),...,\tau _{m}^{\mathcal A}(a)),...,s_{k}^{\mathcal A}(\tau _{1}^{\mathcal A}(a),...,\tau _{m}^{\mathcal A}(a))$
but if we have used induction on the complexity of the terms we could say $s_{i}^{\mathcal A}(\tau _{1}^{\mathcal A}(a),...,\tau _{m}^{\mathcal A}(a))=(s_{i}^{*})^{\mathcal A}(a)$ because $s_{i}^{*}(a)=s_{i}(\tau_{1}(a),...,\tau_{m}(a))$ for $1\leq i\leq k$.
Now we have $a_{0}=F^{\mathcal A}((s_{1}^{*})^{\mathcal A}(a),...,(s_{k}^{*})^{\mathcal A}(a))$.

after this point I can't reach anything practical to obtain the goal of the problem, and maybe my strategy is wrong, so please help if you could to further this solution.

Regards

Answer 1

Yes, the proof needs induction on the complexity of the terms, where by the degree of complexity of a term $t$ we mean the number $n$ of occurrences of function symbols in $t$.

We will consider a simple case, with only one $\tau_i$; thus, we have to show that :

$$(t^∗)^{\mathcal A}(a) = t^{\mathcal A}(\tau^{\mathcal A}(a)).$$

The base case ($n=0$) is easy : if $t := x$ then $t(x/ \tau) := \tau$.

We are left with the case when $t := f_n s_1 \ldots s_n$, where $f_n$ is an $n$-ary function symbol and $s_1, \ldots, s_n$ are terms, with complexity less than $n$.

Then $t^∗ = t(x/ \tau) := f_n s_1(x/ \tau) \ldots s_n(x/ \tau)$.

We have that :

$$(t^∗)^{\mathcal A}(a) = f_n^{\mathcal A}(s_1(x/ \tau)^{\mathcal A}(a), \ldots, s_n(x/ \tau)^{\mathcal A}(a))$$

where the equlity holds by the semantical specifications; this is, using the "abbreviation" $s^*$ :

$$=f_n^{\mathcal A}((s_1^∗)^{\mathcal A}(a), \ldots, (s_n^∗)^{\mathcal A}(a)).$$

Now we apply the induction hypotheses to get :

$$=f_n^{\mathcal A}(s_1^{\mathcal A}(\tau^{\mathcal A}(a)), \ldots, s_n^{\mathcal A}(\tau^{\mathcal A}(a)))$$

but this in turn is :

$$t^{\mathcal A}(\tau^{\mathcal A}(a)).$$