In my book we have this definition about a term:
If $\mathcal{L}$ us a language, a term of $\mathcal{L}$ is a nontempty finite string t of symbols from $\mathcal{L}$ such that either:
- t is a variable
- t is a constant symbol
- t:= $ft_1t_2\ldots t_n$ where f is an n-ary function symbol of $\mathcal{L}$ and each of the $t_i$ is a term of $\mathcal{L}$.
The logical axioms about equality are:
- $x=x$ for each variable x.
- Assume that $x_1,x_2,\ldots,x_n$, $y_1,y_2,\ldots,y_n$ are variables, and f is an n-ary function symbol then:
$[(x_1=y_1)\land(x_2=y_2)\ldots(x_n=y_n)]\rightarrow (f(x_1,x_2,\ldots,x_n)=f(y_1,y_2,\ldots,y_n))$
- Assume that $x_1,x_2,\ldots,x_n$, $y_1,y_2,\ldots,y_n$ are variables, and R is an n-ary relation symbol then:
$[(x_1=y_1)\land(x_2=y_2)\ldots(x_n=y_n)]\rightarrow (R(x_1,x_2,\ldots,x_n)\rightarrow R(y_1,y_2,\ldots,y_n))$
Why are the equality axioms only about variables($x_i,y_i$), and not about terms? Couldn't we for example have $t=t$ for each term?
Update:
The book I am reading is "A Friendly Introduction to Mathematical Logic. it can be downloaded from free here: https://knightscholar.geneseo.edu/geneseo-authors/6/ The equality axioms are on page 48-49.
At least for pedagogical reasons, in my opinion the equality axioms should indeed talk about arbitrary terms rather than just variables. For instance, from the given rules alone there's no way to conclude $$f(f(u))=f(f(u))$$ if $f$ is a unary function symbol and $u$ is a variable.
However, additional inference rules may come to the rescue here. For instance, universal generalization will give us $\forall x,y(x=y\rightarrow f(x)=f(y))$, and then universal instantiation (setting $x=y=f(u)$) gives us $$f(u)=f(u)\rightarrow f(f(u))=f(f(u)),$$ which in turn will give us $f(f(u))=f(f(u))$.
But just because something is mathematically acceptable doesn't mean it's a good idea. Having the equality axioms be so "fragile" in my opinion makes them, and the whole logical apparatus being introduced, harder to think about.