4.The definition of canonical structure $\mathbf{\alpha}$ for $\mathbf{T}$
$\left\{
where,the equivalence class of $\mathbf{a}$ is designated by $\mathbf{a^{\circ}}$,i.e.,all the equivalence $\mathbf{a_1,b_1,...}$ is designated by $\mathbf{a^{\circ}}$, that is,
$\mathbf{a_1^{\circ} \sim a_1 ,..., a_n^{\circ} \sim a_n}$
$\mathbf{a_1^{\circ} \sim b_1 ,..., a_n^{\circ} \sim b_n}$
...
We define $\mathbf{a \sim b}$ to mean $\mathbf{\vdash_{T}a=b}$.Then $\mathbf{a \sim b}$ is an equivalence relation,that is,
$ \left\{
Proof.
By the identity axioms, $\mathbf{\vdash_{T}a=a}$, we get $\mathbf{a \sim a}$.
By the equality theorem, let $\mathbf{A‘}$ be obtained from $\mathbf{A}$ which means $\mathbf{a=c}$ by replacing $\mathbf{a}$ by $\mathbf{b}$. So if $\mathbf{\vdash_{T}a=b}$, then $\mathbf{\vdash_{T}A \leftrightarrow A‘}$, i.e., $\mathbf{\vdash_{T}a=c \leftrightarrow b=c}$. $\mathbf{a=b \rightarrow (a=c \leftrightarrow b=c)}$ is tautological consequence of $\mathbf{a=c \leftrightarrow b=c}$, and $\mathbf{\vdash_{T}a=c \leftrightarrow b=c}$, then $\mathbf{\vdash_{T}a=b \rightarrow (a=c \leftrightarrow b=c)}$ by tautology theorem. That is,$\mathbf{a \sim b \rightarrow (a \sim c \leftrightarrow b \sim c )}$
$\mathbf{\vdash_{T}a=b \rightarrow (a=c \leftrightarrow b=c)}\\ \Rightarrow \mathbf{\vdash_{T}a=b \rightarrow (a=a \leftrightarrow b=a)}\\ \Rightarrow \mathbf{\vdash_{T[a=b]} a=a \leftrightarrow b=a} \ \text{by deduction theorem}\\ \Rightarrow \mathbf{\vdash_{T[a=b]} b=c \quad \text{iff} \quad \vdash_{T[a=b]} a=a} \ \text{by tautology theorem}\\ \Rightarrow \mathbf{\vdash_{T} a=b \leftrightarrow b=c} \ \text{by deduction theorem}$
That is, $\mathbf{a \sim b \rightarrow b \sim a}$
原文：http://www.cnblogs.com/mathematicallogic/p/3764766.html