Equational logic

Definition

Let $\sigma$ be a signature with only function symbols and let $X$ be a set of variables. Let $\Sigma$ be a set of identities over $\sigma$ and $X$. The identities derivable from $\Sigma$ in equational logic, written $\Sigma \vdash s \approx t$, form the smallest set of identities that satisfies the following rules, for all terms $s, t, u, s_i, t_i$:

1. (axioms) every identity in $\Sigma$ is derivable;
2. (reflexivity) $t \approx t$ is derivable;
3. (symmetry) if $s \approx t$ is derivable, so is $t \approx s$;
4. (transitivity) if $s \approx t$ and $t \approx u$ are derivable, so is $s \approx u$;
5. (replacement) if $s_i \approx t_i$ is derivable for $i = 1, \ldots, n$ and $f$ is a function symbol of arity $n$, then $f(s_1, \ldots, s_n) \approx f(t_1, \ldots, t_n)$ is derivable;
6. (substitution) if $s \approx t$ is derivable and $\theta$ is a substitution, then $s\theta \approx t\theta$ is derivable.