＞ゲーデルの論文では、定義とは、省略記号なのだということで通してあります。
＞しかし、さすがゲーデルというか、そういう定義を完全に展開してしまうと
＞扱っている論理式が非常に大きくなるだろうとか、Principia Mathematica のよう、
＞定義のメカニズムが入っていれば、短くなるが、などの証明工学的な話もちゃんと議論しています。
＞前原先生がイオタ記号を使われたのは、ここら変を曖昧にしておくのが嫌だったからでしょう。

ここらへんのことです
論理式の長さ、でしたね、失礼
まあ証明の長さにも同じことは言えると思いますが