I am currently learning about first-order logic and various resolution techniques.
When applying a substitution $\theta$ to two sentences $\alpha$ and $\beta$, for unification purposes, aside from SUBST($\theta$, $\alpha$) = SUBST($\theta$, $\beta$), does the resulting substitution have to be unique?
What I mean is, when unifying, when we check if SUBST($\theta$, $\alpha$) = SUBST($\theta$, $\beta$), is it OK if SUBST($\theta$, $\beta$) = $\beta$ ?
Thank you.
The most general unifier $\theta$ is unique in the sense that given any other unifier $\phi$, $\alpha \phi$ can be got from $\alpha \theta$ by a subtitution, and the same for $\beta$.