Let $F$ be a ranked alphabet of function symbols.
And let $X$ be an alphabet of variables.
The set of terms $T$ , built over $F$ and $X$ , is inductively defined as follows:
- If $x\in X$, then $x\in T$.
- If $c\in F$ is of arity $0$, then $c\in T$.
- If $f \in F$ is of arity $n$, and $t_1,\dots,t_n \in T$, then $f(t_1,\dots,t_n)\in T$.
Let $M = ⟨D, I⟩$ be a model, and $\rho : X\to D$ be a valuation.
The interpretation of a term t is inductively defined as follows:
- $[\![x]\!]_ρ = ρ(x)$, for $x \in X$.
- $[\![c]\!]_ρ = I(c)$, for $c \in F$ of arity $0$.
- $[\![f(t_1,...,t_n)]\!]_ρ = I(f)([\![t_1]\!]_ρ,...,[\![t_n]\!]_ρ)$, for $f \in F$ of arity $n$.
Let $\rho$ be a valuation, and let $a \in D$ and $x \in X$. The valuation $\rho[x:=a]$ is defined as follows:
$$\rho[x:=a](y)=\left\{\begin{matrix} a\ &if\ x = y \\ \rho(y)\ &if\ x \neq y \end{matrix}\right.$$
Finally, let $t$ and $u$ be terms, and $x$ be a variable. The substitution of $x$ by $u$ in $t$, in notation $t[u/x]$, is inductively defined as follows:
- $x[u/x] = u$.
- $y[u/x] = y$, for $y \in X$ and $y\neq x$.
- $c[u/x] = c$, for $c \in F$ of arity $0$.
- $f(t_1,...,t_n)[u/x] = f(t_1[u/x],...,t_n[u/x])$, for $f \in F$ of arity $n$.
Let $x$ be a variable, $u$ be a term, and $\rho$ be a valuation.
Show that for every term $t: [\![t[u/x]]\!]_\rho = [\![t]\!]_{ρ[x:=[\![u]\!]_ρ]}$
Hint: proceed by induction on the structure of $t$.
I'm not used to do such this proofs so any help would be appreciated !