再帰的定義と体系の強さ

質問

再質問になります、ご容赦ください。
［ゲーデルに挑む 田中一之］のp152の記述に、形式的な定義は略記に限るものとし
x^0=1 x^(y+1)=x^y・x
のような再帰的な(略記でない)定義で論理式を形式体系に付け加えることは公理を増やすことに他ならず体系の強さが変わってしまう可能性がある
とあるのですが、これはどういうことでしょうか。
つまり、再帰的定義は記号の使い方を定めているだけであり(上の例であれば、関数記号^の記号としての使い方)、この定義によって初めてその記号が登場してくるならば、それによって体系内で何か新しいことができるようになったりはしないと思うですが...。すなわち定義を追加するだけでは、公理を増やすことにはならず体系の強さも変わらないと思うのです(もちろん、定義するだけでなく、定義した記号に関する公理を追加すれば話は別ですが)。
この方面に詳しい方いらっしゃいましたらお助け下さい、よろしくお願いします。

回答No.1

jcpmutura

x^0=1
は
xと0の演算^の結果x^0を1と定義するのだけれども
それ以前にxが定義されていないので
xをある数とします

x^(y+1)=x^y・x
は
xとyの演算^の結果x^yが定義されているとき
に限り
xとy+1の演算^の結果x^(y+1)をx^yとxの積x^y・xと定義する
のだから
それ以前にx,y,x^yの3つがともに定義されていなければなりません
それ以前に定義されているのは
xはある数
x^0=1
なので
y=0
となるので
x^(y+1)=x^y・x
は
x^1=x^0・x=1・x=x
となりますが
形式上再度
x^(y+1)=x^y・x
を繰り返す指定が省略されているとはいえないので
x^0=1
x^1=x
の2つを定義しただけで定義終了となって
再帰的定義とならないと思います。

x^0=1
for(k=0～y-1)x^(k+1)=x^k・x
のように
繰り返し指定記号for()とその意味を
追加すれば
xとyの演算^の結果x^yの
再帰的定義となると思います。

お礼

ありがとうございます、本当に遅くなってしまい申し訳ありません。
x^(y+1)をX^y+xに書き換えてよいということなら新しい公理をいれていることになるのですね。