Additive number theory - kururu

ゲーデルの不完全性定理について少し補足 - くるるの数学ノートの続報。かがみさんにコメントで質問された件に関して。

Keisler-Changの"Model Theory"を見ると、以下のように書いてあります。言語L''={+, S, 0}上で、以下の公理を持つ体系をadditive number theoryといいます。

$0\neq Sx$
$Sx=Sy \Rightarrow x=y$
$x+0=x$
$x+Sy=S(x+y)$
for each formula $\varphi(v_0, \ldots, v_n)$ , $\varphi(0, v_1, \ldots, v_n)\wedge(\forall v_0)(\varphi(v_0, v_1, \ldots, v_n)\Rightarrow\varphi(S v_0, v_1, \ldots, v_n)\rightarrow(\forall v_0)\varphi(v_0, \ldots, v_n)$

このとき、additive number theoryは完全であることがPresburgerにより1929年に証明されているそうです。というわけで、回りくどいですが帰納法は含まれています。
なぜ不完全性定理が証明できないかということは明示的には書いてありませんが、やはりコーディングおよびデコーディングをするのに乗法が不可欠ということなのだろうと思います。加法と乗法だけを用いた論理式でべき乗を表現できるというのはけっこうnon-trivialなのではないかと。

つまり、「n×mっていうのはnをm回足せば求められるんですよ」という記述はすでに十分な複雑さを持っているってことになるのでしょうか。