ゲーデル数と自然数の有限列について

質問

ピンポイントな質問で申し訳ないのですが、もし答えられる方がいらっしゃればお願いします。

　田中一之著「ゲーデルに挑む」の原論文第一節　p29に論理式は自然数の有限列で表されるとあって、その下の脚注8に「この有限列というは自然数の始切片で定義される数論的関数であって数が隙間を空けて並んでいるのではない」とありますが、ただ数が隙間を空けているものとすると、どのようにまずいのでしょうか（扱いにくくなってとても不便ことはわかりますが）。

　このあとにゲーデル数を実際導入する際は素数を使って定義していますが、これは「自然数の始切片で定義される数論的関数」となっているのでしょうか（数論的関数なるものがどういうものなのかがよくわかっていないのです）。

　またゲーデルが行ったのは、ある種の自然数がある性質をもつかどうか調べることが、体系内である論理式が証明できるかどうかを調べることになるということを、正確に定式化することだと考えているのですが、
前者の自然数の性質がどういった内容をあらわすか、つまりある自然数がどの論理式の証明可能性をあらわしているかは、数学は教えてくれず（解釈自体は体系内で行われることでなく）、人間が解釈を行う必要があるということでしょうか（もちろんゲーデル数の性質と記号変形としての証明の手順の間には対応があるので恣意的に解釈することは全く不可能ですが）。
変な質問になってしまって、恐縮ですが、お詳しい方お時間あればよろしくお願いします。

回答No.1

stomachman

ご質問の前半は田中一之著「ゲーデルに挑む」が手元にないので、なんとも。
　「数論的関数」は（一般には結構広い意味を持ちますけれども）ゲーデル数に関する議論に出て来るんであれば、自然数上の帰納的関数、というほどの意味であることが大抵だろうと思います。ま、「必ず有限回の演算で答が出る、自然数の組から自然数への関数」ぐらいに思っておけば良いかと。

> ある自然数がどの論理式の証明可能性をあらわしているか

　具体的な「ある自然数」が与えられれば、それを全く機械的にかつ一意的に文字列に変換できる。結果が論理式（の列）になっているかどうか（論理式の統語規則に従った文字列かどうか）も機械的に判別でき、そしてもしそれが論理式であれば、「どの論理式か」という問いへの答はその文字列です。さらに、論理式を自然言語の文に変換する（自然言語で読み下す）ことも機械的にできます。
　「人間が解釈を行う必要がある」とすれば、それは論理式を読み取って「あーそういうイミね」とナットクする、というところ。これは論理式を充足する何らかのモデルをイメージする、というほどのことであって、形式的証明とは無関係です。ってか、そういう曖昧な所を排除したのが形式主義ですもん。

　余談ながら、ゲーデルの議論の要諦は、具体的でない自然数、つまり「ある性質を満たすような自然数の全体」を考えるあたりから。ここでようやく、論理式を自然数に対応付けて論理式の操作を自然数上の関数で表現した（つまり、推論過程のモデルを自然数上で作った）、ということが意味を持って来る訳で、これで（個別の具体的な論理式ではなしに）具体的でない論理式の無限集合を扱えるようになった。これこそが「証明も反証も不可能な論理式は存在するか」という議論を可能にする仕掛けのミソです。

お礼

とても遅くなってしまいました、申し訳ありません。
回答ありがとうございます、今回もとても参考になりました。

>機械的にかつ一意的に文字列に変換できる
>具体的でない自然数、つまり「ある性質を満たすような自然数の全体」を考える

機械的に動かせる用にしておいてそこからあるまとまった範囲を考えるわけですね。そのようなことができるということ自体がある種、不思議に見えてしまって変なイメージを持ってしまっていたようです。
ただ、機械的に全て話が進むとわかっていても、やはり自然数を自然数として扱う立場と、自然数をなんらかの論理式の文字列として扱う立場では、どこかレベルが違う話なのではないかとこだわりを捨てられないでいる面もあります。つまり実際議論している対象は、動かしているのは自然数であって、それを論理式に見て取るのが人間ではないのかと・・・。
しかしおそらく、これは数学の疑問ではないのですね。

以下、少々関係のずれた疑問点になってしまって申し訳ないのですがもうひとつ伺いたいことがあります。

>必ず有限回の演算で答が出る、自然数の組から自然数への関数

いわゆる計算論において、関数は有限回の帰納的な操作によって記号を別の記号に書き換えること（「ｎ」に「‘」を書き足し「ｎ’」にするなどして）を記号間の関係として定義したモノだと思っていました。
そして、集合においても順序対として関数は導入されると思うのですが、
集合論の言葉では関数というのはある性質を持った、対応付けが存在するという風に書かれていると感じます。
この「存在する」という書き方の関数の定義で、上の定義と同様に有限回の操作で、ある対象に対応づけられた対象を特定できるのでしょうか、つまり実際に対応物をどうやって見つけてくるのかを教えてくれないのではないかといったことは問題として発生しないのでしょうか。
もちろん、論理的に問題なければ（人間の意味のレベルで）実際特定可能かどうかは本質的な問題ではないと思うのですが（非可述的定義も許されているわけですし）。
計算論ではそのような関数は出てこない、帰納的関数を主として扱うようなので、集合論における関数と何か相違点（そういった関数を扱わない理由）があるのだろうかと感じてしまいます。というか逆に集合論では計算論で扱えない関数も扱っているのだろうかと思うのです。

今回も回答本当にありがとうございました、しっかり考えて今後の糧として活かしたいと思います。
後半の方、かなり勘違い、無理解の類が混じっていると思い不安なのですが、もしお時間に余裕ありましたらよろしくお願いします。