自然数論の無矛盾性証明では証明図に順序数を与えて、その下で超限帰納法で証明してるじゃないですか。
なんで証明図に順序数を対応させなきゃいけないんですか？
ゲーデル数のアイデア流用して証明図に自然数を対応させるんじゃダメなんですか？
ゲーデル数の定義を巧妙にしたら、
　記号列(論理式)の有限列(=シーケント)　の有限列(=”糸”みたいな奴←カット除去定理の時に定義されてた奴)
　　　の有限列(=証明図)
を一意に自然数に対応させることって出来るような気がするんですが？(漠然とした感想)