4.The definition of canonical structure $\mathbf{\alpha}$ for $\mathbf{T}$

$\left\{

|α|={a°1,...,a°n,...}fα(a°1,...,a°n)=(fa1...an)°pα(a°1,...,a°n)iff?Tpa1...an

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\{

a～aa～b→(a～c?b～c)a～b→b～a

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}$