Defining substitution by structural recursion

Question

For a term u, let $u{x\atop t}$ be the expression obtained from $u$ by replacing the variable $x$ by the term $t$. Define $u{x\atop t}$ by recursion on $u$.

Not really sure how to start this one. I'd appreciate any help.

Answer 1

Begin by defining $u[{x\atop t}]$ when $u$ is a variable or a constant. The first clause will be $x[{x\atop t}]=t$; there will be two more clauses, one for the case where $u$ is a variable other than $x$, and one for the case where $u$ is a constant. After that comes the recursion clause, where you'll define $f(t_1,\dots,t_n)[{x\atop t}]$ in terms of the $t_i[{x\atop t}]$, where $f$ is an $n$-ary function symbol and $t_1,\dots,t_n$ are terms. Every clause here can be found by just thinking about what substitution of $t$ for $x$ should do to variables, to constants, and to compound terms.

(If you or your teacher or your textbook had the good taste to treat constants as $0$-ary function symbols, then you don't need a separate clause for the case where $u$ is a constant; it will be covered by the $n=0$ case of the recursion clause.)