TITLE: Converse of renaming substitutions
QUESTION [0 upvotes]: In the paper Theory Unification in Abstract Clause Graphs, Hans Jorgen Ohlbach states that, given the renaming substitution $\sigma$, the converse substitution $\sigma^{c}$ is defined as $x=\sigma(y) \leftrightarrow y=\sigma^{c}(x)$, for all variables $x$ in the set of variables $V$. Example: if $\sigma = \{x \mapsto x', y\mapsto y'\}$, then the converse $\sigma_{c} = \{x' \mapsto x, y'\mapsto y\}$. The author concludes that, if $\sigma$ is a renaming substitution, then $\sigma\sigma^{c} = \sigma$ and $\sigma^{c}\sigma = \sigma^{c}$. This conclusion is not clear to me, since, as far as I can tell, $\sigma\sigma^{c} = \sigma^{c}$ and $\sigma^{c}\sigma = \sigma$. For instance, using the same example above, considering $\sigma = \{x \mapsto x', y\mapsto y'\}$, then
$\sigma\sigma^{c} = $
$\{x \mapsto x', y\mapsto y'\}\{x' \mapsto x, y'\mapsto y\} = $
$\{x \mapsto x, y \mapsto y, x' \mapsto x, y'\mapsto y\} =$
$\{x' \mapsto x, y'\mapsto y\} =$
$\sigma^{c}$.
Could someone help me understand how the author concludes that $\sigma\sigma^{c} = \sigma$ and $\sigma^{c}\sigma = \sigma^{c}$?

REPLY [1 votes]: Assume that we are speaking of "repeated substitution".
Then, with term $t(x,y)$ and the above substitutions we have:

$\sigma(t(x,y))=t(x',y')$ and thus: $\sigma^c[\sigma(t(x,y))]=\sigma^c[t(x',y')]=t(x,y)$.

But $\sigma^c(t(x,y))=t(x,y)$, because there are no $x',y'$ in $t$, and thus: $\sigma^c\sigma=\sigma^c$.
In the same way:

$\sigma^c(t(x,y))=t(x,y)$ and thus: $\sigma[\sigma^c(t(x,y))]=\sigma[t(x,y)]=t(x',y')$ which is $\sigma(t)$.

Thus: $\sigma\sigma^c=\sigma$
{"set_name": "stack_exchange", "score": 0, "question_id": 4439025}