把皮亚诺第五公设纳入TNT里来的努力最多也就能做到这个地步.现在让我们用它来证明∀
a:(0+a)=a的确是一个TNT定理.我们先用幻想规则从上面推导中的那个幻想里出来,得到:
⑽
<(0+b)=b→(0+Sb)=Sb>
幻想规则
⑾
∀
b:<(0+b)=b→(0+Sb)-Sb>
概括
这是归纳规则要求输入的两个定理之中的一个.另一个所要求的是金字塔的第一行,这是我们已经有了的.因此,我们可以应用归纳规则,去推演我们所想要的东西:
∀
b:(0+b)=b
特称和概括将允许我们把变元从b改为a,于是∀
a:(0+a)=a就不再是TNT的一个不可判定串了.
一个长推导
现在我想介绍一个TNT中较长的推导,以便你能够看到