码迷,mamicode.com
首页 > 其他好文 > 详细

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

时间:2014-06-04 15:49:48      阅读:179      评论:0      收藏:0      [点我收藏+]

标签:des   c   a   tar   ext   com   

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

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}$,布布扣,bubuko.com

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

标签:des   c   a   tar   ext   com   

原文地址:http://www.cnblogs.com/mathematicallogic/p/3764803.html

(0)
(0)
   
举报
评论 一句话评论(0
登录后才能评论!
© 2014 mamicode.com 版权所有  联系我们:gaon5@hotmail.com
迷上了代码!