ま ず、「超数学」ですが、「数学の証明をする」のではなくて、「数学で証明できることを、証明する」、とい う感じが「超(メタ)」なわけです。

つまり、「「この数学(整数)は全部の問題を証明できる」という問題を証明する」訳です。そこに、数学(整数)自体を使う、という のが不完全性定理のアイデアの一つで、そうしておいて、矛盾して解けない問題Gを作ることで、完全性(問題が全部解ける)と無矛盾性(矛盾しない)を証明する野望を打ち砕いたわけです。

不完全性定理によって、「カードゲームにされた数学(形式化された整数論)の無矛盾性と完全性を、”形式化された方法で”証明する」試みは失敗しましたが、数学が矛盾しているという訳でもないし、無矛盾性を証明することが絶対できない訳でもありません。また、カードゲーム(公理系)の中には、矛盾しておらず完全であることが証明可能なものもあります。

さて、ではこれが人工知能の実現に致命的な打撃を与えるかというと、必ずしもそう言うわけでもないようです。コンピュータが知りえないことを、不完全性定理によって人間が証明したわけではありません。

しかし、カードゲームのルールをどうやって選ぶのか、どのルールに意味を見出のかは、今のところコンピュータではできていません。ただし、それは不完全性定理によって証明されたことだけで解決できるものではなく、どうしたらできるのかは、引き続き考えなくてはなりません。

大回りをして見てきたとおり、論理学、幾何学、整数論、といった数学の様々な分野が、「形式化」によって記号の置き換えで表現できるようになってし まいました。論理も、幾何も、整数も、カードゲームのローカルルールの一種に過ぎないとも言えるわけですが、それらがどうして意味を持っているのか、とい う問題とも関係してくる事になります。

というわけで次回以降は、形式化の実際について見てゆきたいと思います。