2022年最終週の月曜日。朝の通勤客がそろそろ減るかなと思っていましたが普段通りです。昼休みの繁華街は冬休みなのか若い人が多くなりました。
約40年前に発刊された数学基礎論というか数学哲学の邦訳書、オンデマンド版が書店に普通に売られていてどうなっているのか。これ幸いと手に入れましたが。
何でも、数学に対する姿勢には、プラトン主義、形式主義、構成主義があるそうです。私の解釈ではプラトン主義は実数だとか三角形だとかが少なくとも形而上学的には存在するとする立場。形式主義は純粋に記号論理だけを追いかける立場。構成主義は公理から有限回の推論しか認めない立場、のようです。何だか異質なものを混ぜた感じがするので、単に歴史的な分類と思います。
時代的には最初の人工知能の流行期の直前で、LISP等による一部の追求はあった時代です。第五世代コンピュータ計画は少し後だったか。なので一階述語論理の構造に対する追求がいまいちの感じがします。
現在のコンピュータの能力はずっと進んでいますし、台数もすさまじい数です。人工知能の概念も進んでいると思います。それにもかかわらず、コンピュータが数学の証明を次々に進める、などと言った話は全く聞きません。どこかで秘密にしている、と言う意見に対しては、見栄を張る個人とか国家は多数ありますから否定して良いと思います。
つまり、数学の証明は一階述語論理に基づいてはいるものの、機械化は遅々として進んでいない、ということ。これは一階述語論理の構造を調べると自然に結論できると思うのですが、あまりそういった意見は見られないような気がします。この本も、その直前のところをぐるぐる回っているだけに見えました。最近は違うのかな?。
まあ、ここまで状況証拠が並んだら安心して良いでしょう。数学は普通に学問です。
