>>456
自然数論単体は矛盾するか矛盾しないかのどちらかであり、1階述語論理の完全性と健全性
により矛盾すればモデルは存在せず、無矛盾であれば存在する

無矛盾であれば、たとえばPA+TとPA+SでBB(x)が取る値が異なることが考えられるのではないか、
ということになるが、どちらの理論も自然数論を含む以上自然数型を部分集合としてもっており、
自然数型をもっていれば異なるモデルに属していても大きさを比べることができ、それなら同じ文字数制限で
出力される最大の数でどちらが大きいかを比べることができ、BB(x)の値が一意に定まる。

自然数型のすべてを持っている必要もない

でいいだろうか