5.The right-hand sides of n-ary function and predicate definition in canonical structure depend only on the $\mathbf{a_i^{\circ}}$ and not on the $\mathbf{a_i}$
Proof.
Suppose that $\mathbf{a_i^{\circ}=b_i^{\circ}}$ for i=1,...,n. Then $\mathbf{\vdash_{T}a_i=b_i}$ by the definition of canonical structure,$\mathbf{=_\alpha(a_i^{\circ},b_i^{\circ}) \quad \text{iff} \quad \vdash_{T}=(a_i,b_i)}$. By equality theorem,
$\mathbf{\vdash_{T}fa_1...a_n=fb_1...b_n}$
$\mathbf{\vdash_{T}pa_1...a_n \leftrightarrow pb_1...b_n}$
Hence
$\mathbf{(fa_1...a_n)^{\circ}=(fb_1...b_n)^{\circ}}$, by $\mathbf{=_\alpha(a_i^{\circ},b_i^{\circ}) \quad \text{iff} \quad \vdash_{T}=(a_i,b_i)}$
and
$\mathbf{\vdash_{T}pa_1...a_n \quad \text{iff} \quad \vdash_{T}pb_1...b_n}$, by tautology theorem(P30 i).
that is,
$\mathbf{f_\alpha(a_1^{\circ},...,a_n^{\circ})\\ =(fa_1...a_n)^{\circ}\\ =(fb_1...b_n)^{\circ}}$
$\mathbf{p_\alpha(a_1^{\circ},...,a_n^{\circ}) \\ \quad \text{iff} \quad \vdash_{T}pa_1...a_n \\ \quad \text{iff} \quad \vdash_{T}pb_1...b_n}$
Thus,the right-hand sides of n-ary function and predicate definition in canonical structure depend only on the $\mathbf{a_i^{\circ}}$ and not on the $\mathbf{a_i}$
原文：http://www.cnblogs.com/mathematicallogic/p/3764803.html