首页 > 代码库 > 4.2 THE COMPLETENESS THEOREM: (5) The right-hand sides depend only on the $\mathbf{a_i^{\circ}}$ and not on the $\mathbf{a_i}$

4.2 THE COMPLETENESS THEOREM: (5) The right-hand sides depend only on the $\mathbf{a_i^{\circ}}$ and not on the $\mathbf{a_i}$

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