【自由研究】数学DB設計-000

PK_RNX_ずんだもん博士(数物系)

みなさんこんにちは、ずんだもん博士なのだ。今回から、長年チマチマ考えていた果て無き「僕の数学の基礎」を放流していきたいと思います。

基本的には「定理自動証明」という分野のことを自己流で考えていたのですが、最近はAIやらLeanなどの発達によって、ちょっとレッドオーシャンになりすぎているなと感じ始めています。アマチュアが手を出して何か残せる場所じゃないです。

それでも「数学の基礎を考えるのが楽しい、という思いを何か残せないかな？」と考えたとき、SEとしての経歴が活きて「数学データベース」という形でまとめるのが良かろうと思いました。数学の基礎を構成する最小単位をテーブルとして設計して、外部キー制約で証明の正しさを保証する、という構想が、おぼろげながら浮かんできました。

今回はPart-000ということで、僕が一体何をしたいのか？それに向けてどのようなことをしたいのか？そのようなプリフェイスを語っていくのだ！

ちなみに作り途中のやつGitHubで公開してます：


ユークリッド以来、数学を語るものは証明を語る

表題はブルバキ氏が大著「数学原論」の一言目です。だったと思います。たしか。

ユークリッド以前はとにかく計算して実用にできないと意味がありませんでした。たぶんね。それは例えばピラミッドを作るためだったり、方角を把握するために「星」という空の地図を把握するためだったりしました。あるいは宗教的な紋様を描くために、定規とコンパスで描ける図形を分類するためだったりしたようです。例外的に、とても平和だった(しらんけど)バビロニアでは二次方程式の解法が残されていたと言われます。

定規とコンパスで描ける図形を究めた結果、紀元前3世紀ごろ、ユークリッド(エウクレイデス)という古代エジプトの数学者は、3次元空間に描きうる正多面体を網羅すべく「原論」という書物を残しました。そこで展開された論理はまさに現代数学と何にも変わらないです。点から直線、平行であることなどに至る非常に精密な定義や公理から、正しい推論(証明)を行い、新たな定理を得る、そんな活動が描かれていました。世界史上最大のベストセラー本が聖書なら、二番目はユークリッド原論であろうとさえ言われて…聞いたことがあります。

結果を見れば、彼以降の数学・天文学は、彼に倣うことになったようです。例えばプトレマイオス著「アルマゲスト」も、現代風に言えば観測事実に対する天動説というひとつの「モデル」を定義し、そこから正しく推論(証明)して得られる結果を網羅したものでした。天動説の「モデル」は結果的に正しくなかったとしても、モデルを構築して正しい推論をして当時既存の観測結果を説明する、という活動は、数学的には何のミスもありません。だからこそ、実のところ「地動説」という新しいモデルも、数学的にそんなに間違っていないと思われたからこそ、実のところそんなに異端視されるということもなかったのです(例えばコペルニクスは、当時の教皇に自身の地動説を口頭で発表して、教皇は称賛したとすら言われますしらんけど)。

こうした哲学的・科学的・あるいは理学的な活動のすべては、ユークリッドが作り出した「定義(モデル)から始め、正しい推論(証明)をして、定理を導く」という活動です。ユークリッド以来、数学を語るものは証明を語るとは、そういう意味だと、僕はとらえています。

(防衛線の厚さ…)

「正しい推論(証明)」とは

モーダス・ポネンス

「人間は死ぬ。ソクラテスは人間である。ゆえにソクラテスは死ぬ」

こんな記事をここまで読んでる人の中で、この推論を知らない人・わからない人は、あの、すみません。この一行を100回読んでください。三段論法、ラテン語でモーダス・ポネンスといいます。まあでも、当然っぽい推論です。人間は死にますし、ソクラテスは人間でしたし、ソクラテスは死にましたし。でも、僕たちはなぜこれを正しいと思うのでしょうか？僕は実のところ、それには理由はないと思っています。あえて言えば、僕たちの知性、あるいは理性が物理法則に縛られているのであろうということ、そしてその物理法則が"それ"に則って運動している"のであろう"から、と考えています（思想の強さ）。

少なくとも数学基礎論では、一般的に三段論法が正しいということは「定義」します。どの目線でモノを言うとるんや！と思ったVシネマニア兄貴姉貴もいると思いますが、一般的には「僕たちの目線」だと思います。よくギャグ漫画で「いうてウチら架空のキャラクターやし…」みたいな「メタ発言」をする子がいますね。こういうメタ視点を認識する・させられると、えてして面白いと感じるものです。(僕はSCP-1374とか結構好きです)。それと同じで、こういう三段論法が正しいと定義する人は、三段論法を使いつつ「いうて三段論法は正しいとしてるから…」って言ってるようなものです。もしかしたら、僕たちを宇宙の外から見ている何者かは、僕たちがそう議論している様子をみてゲラゲラ笑っているかもしれませんし、僕たちは彼らの空想上の人物に過ぎないのかもしれません。貴様、見ているなッ！

ウィトゲンシュタインさんも「語り得ぬものには沈黙しなければならない」って言ってます。数学の基礎を求め続けても多分底がないです。多分数学の基礎が"正しいか間違ってるか"も語り得ぬものの一つです。デカルトも疑わしい余地がある命題をすべて取り去った結果、最後に残ったのが「われ思うゆえに我あり」だっていう話を聞いたことがあります僕哲学知らんけど。

まあ結局、僕の考える「正しい推論」というのはこうです。つまり、「いくつかの命題から新しい命題を導いてよいと、僕たちが理由なく定義する、いくつかの手続き」。数学基礎論ではこれを推論規則と呼んでいます。モーダスポネンスも推論規則の一つというわけです。そしたら、正しい推論、正しい証明というのは、正しいと定義した推論規則が正しく使われることの連続と定義すべきでしょう。

さて、推論規則の説明で未定義語「命題」が出てしまいました。これを紹介しましょう。

数学の基礎の構成単位ざっくり紹介

命題

命題とは「何かの主張」ではあります。ソクラテスの例でいえば、3つの命題がありました。

  • 人間は死ぬ

  • ソクラテスは人間である

  • ソクラテスは死ぬ

ただし、それぞれが正しいか間違っているかは、命題を定義するときの俎上には基本的に乗せられないです。例えば

$${1+1=2}$$

これも命題といえるものですが、これが正しいかどうかは「命題の定義」では議論しません。なんなら、$${\mathbb{Z}/2\mathbb{Z}}$$という環では$${1+1=0}$$なので、$${1+1=2}$$は正しくないとすらいえます。そういう意味で、「命題とは真偽が定まっている主張である」などとする命題の定義は誤りです。極論、例えば

ゴールドバッハ予想
6以上の偶数は二つの奇素数の和であらわせる

という未解決の命題があります。もし「真偽が定まっている主張」を命題とするならば、ゴールドバッハ予想は今のところ命題ではないことになってしまいます。例えばポアンカレ予想は2002～2003年にペレルマンによって肯定的に解かれましたが、それまでは命題ではなかったということになります。極端な話、連続体仮説「自然数濃度と実数体濃度の間の濃度は存在しない」というのは、ZFC公理系からは正しいとも誤っているとも証明できないことが証明されています。では連続体仮説は命題ではないの？てかそもそもZFC公理系をなす主張のおのおのは命題じゃないの？

結局のところ、命題とは何なのでしょうか？基礎論では命題を、「あるルールで定められた記号の羅列(論理式)のうち、ある分類に属するもの」と定義します。さて、また未定義の言葉が出てきました。「記号」とは何か？「あるルール」とは何か？それが命題であると分類する区分けは何か？

記号

基礎論で扱う最小単位こそおそらくこの「記号」です。例えば「1」は記号ですし、「2」も「+」も「=」も記号です。しかし、それぞれの記号が果たす役割というか、機能が全然違いますね。

例えば「1」や「2」はそれぞれ、具体的な実体を表すのに対して、「+」は二つの数学的実体を組み合わせて新しい数学的実体を出力する関数のような役割を果たします。「=」はまたそれらとは異なり、「1+1と2という二つの実体が同じものである」という主張、すなわち命題を作り出す記号です。

「1」や「2」は定数記号、あるいは引数の個数が0個の関数記号と定義されます。僕は基本的にはこれを後者、つまり、引数の個数が0個の関数記号と考えることにします。まあ実際、どっちでもいいでしょう。

「+」や「-」、加減乗除、微分・積分、その他を表す記号は関数記号と呼ばれます。僕は定数記号を引数の個数が0個の関数記号としたので、厳密には引数の個数が1以上の関数記号ということになります。

「=」や「～～～は集合である」とか「～～～は群である」「位相空間である」といったことを言い表す記号を述語記号といいます。僕は多くの述語記号を作るつもりでいます。例えば「IsSet」という述語記号を作って、「IsSet X」で「Xは集合である」という命題を作り出す機能を付与しようと思っています。他にも「IsGroup」「IsTopologicalSpace」などを構想しています。重要なのは、「記号だからと言って一文字しか許さないというルールはない」ということです。考えてみれば、三角関数「$${\sin,\cos,\tan}$$」なんかも1文字ではないですよね。

他にも「自由変数」「論理記号」「量化記号」などを用意するつもりです。変数は想像通りだと思います。論理記号も、例えば「and」を意味する$${\land}$$とか、「not」を意味する$${\neg}$$などを用意します。量化記号は二種類あって、「$${\forall, \exists}$$」もあれば、「$${\{\mid\}}$$」なども仲間入りします。$${\{\mid\}}$$は、命題$${P}$$とそれに含まれる自由変数$${x}$$を引数にして項$${\{x\mid P(x)\}}$$を作る記号です。つまり集合を作る量化記号です。日ごろ数学を嗜んでいる皆々様なら、なんとなく何を言っているか分かっていただけると思います。細かいことは次回以降語るとしましょう。

現在の僕の構想では、変数記号に「命題を代入するタイプの変数記号」、いわば命題型自由変数を用意するつもりでいます。多くの数学基礎論の教科書ではそのような記号は許可してないのですが、僕の目的はあくまで定理と証明のDB化。もしこれを許さないとどうなるかというと、例えば「二重否定則$${\neg\neg\varphi}$$から排中律$${\neg\varphi\lor\varphi}$$を導いてよい」というようなことを、個々の証明の中で、それを個々の命題$${\varphi}$$に対して適用するたびに、新しくその証明文を載せないといけなくなってしまうんですね。その対策としてまず考えうるのは、そういう主張を「推論規則として機能する定理」として分類するということですが、今度は定理の管理が面倒くさくなります。例えば「二重否定則から排中律が導ける」のように推論規則として機能する定理と、それ以外…例えば「ポアンカレ予想」みたいな定理の区分けが必要になってきます。そのために「定理を適用する」というごくありふれた証明の一文を書くのでさえ、プログラムとしてはその二つのどちらを使ったのかで煩雑な条件分岐が必要になってしまいました。実は僕は最初、命題型自由変数を認めず、推論規則型の定理を認める方針でコーディングまで進めていたのですが、そんなことがあって非常にしんどくなってしまいました。じゃあもう命題型自由変数を導入したすぎて、ウォーターフォールでいえば要件定義まで差し戻して考えているところです。。。

論理式の構成手続き

上記の「記号」には「種類」と「引数の個数」という属性を最低限持たせるつもりです。ざっくりとそれぞれ説明すると、

  • 種類：それが命題を作るか、あるいは項(数学的な物体)を作るか

  • 引数の個数：いくつの命題・項から、命題・項を作るかということ

例えば$${\land}$$は種類が「論理記号」、引数の個数が「2」です。例えば$${\times}$$は種類が「関数記号」、引数の個数が「2」です。否定記号$${\neg}$$は引数の個数が「1」の論理記号です。

ザックリ言って、「何か記号を使うとき、その引数の個数を合わせましょうや」っていうルールを「論理式の構成手続き」と呼びます。そして論理式の構成手続きというバリデーションを通過している記号列だけを「論理式」と呼ぶことにしています。

ところで、引数はなんでもいいっていうわけじゃないです。$${\varphi}$$を命題としたとき、$${\varphi+3}$$なんていう記号列が認められるわけじゃないです。なので、記号には「引数に取ってよい論理式の種類」という属性も付与します。

命題と項、そしてポーランド記法

例えば$${1+1}$$は項ですが、$${1+1=2}$$は命題です。つまり、「最後に使った記号が何か」に応じて、その論理式が命題であるか項であるかが決まります。例えば関数記号や項型自由変数、項型量化記号を最後に使った場合は項になるし、命題型自由変数・述語記号・論理記号・命題型量化記号を使った場合は命題になります。

ところが「最後に使った記号が何か」を判定するのは、このままでは難しそうです。そこでDB内部では、「ポーランド式」と呼ばれる文字列の並べ方を採用します。これは、演算子のような記号でさえ、引数の個数が2つの関数のように書くということで、例えば$${1+1=2}$$は

$$
\begin{align*}
=+112
\end{align*}
$$

となります。人間的にはとても見づらくなりますが、プログラムとしては非常に都合がいいです。例えば左端の文字を見れば、それが最後に使われた記号だとわかるからです。

また、論理式の構成手続きというバリデーションでも役に立ちます。記号に連なっている引数の個数が正しいかどうか、そしてその引数が命題・項かを機械的に判別できるからです。

定理と証明

定理は「仮定」と呼ばれるいくつかの命題と、「結論」と呼ばれる一つの命題からなるものと定義するのは、自然だと思います。

また、推論規則をどのように使ったかという手順の履歴の羅列を証明文ということにします。そうしたとき、定理の証明というのは、その定理のいくつかの仮定から始めて、結論に至る証明文ということになります。

公理

公理テーブルは作る予定ですが、僕のやりたいことについては普段あまり役に立たないテーブルだとは思っています。というのも、僕たちが定理を紡ぐにあたって、その定理の「仮定」がどの公理に属するものかはあまり気にしなくてもいいからです。

ただし、よく知られているように

ゲーデルの第1不完全性定理
(自然数論を含む)どのような無矛盾な公理系も、その公理系から独立した命題が存在する

ゲーデルの第2不完全性定理
(自然数論を含む)どのような公理系も、自身の無矛盾性を証明できない

というメタ定理が知られています。ゲーデルの不完全性定理が成り立つ大前提として、「有限ステップの証明文では」というものが入りますが、僕が作ろうとするDBは当然有限ステップの証明しか扱えないので、ゲーデルの不完全性定理に縛られるものです。

この観点から、ZFCやNBGなどの基本的な公理系は定義するけれども、それらは変更されうるという前提、あるいはそのこと自体を目的として作ります。公理テーブルに命題がぶら下がるっていうよりも、各命題に「どこそこの公理系に含まれている命題です」というタグをつけていくイメージです。

公理に変更または削除があった場合、DBというシステムとしては、その公理に依存している定理と証明にフラグを立てる処理を行おうと思います。そうすることで、人間の手で改めて考えるべきところが明らかになり、修正が容易になると思われます。

また、こう言っちゃうってことは、ゲーデルの不完全性定理とか、選択公理がZF独立とか、連続体仮設はZFC独立とか、そういう理論に対する理論、こういうのこそ数学基礎論の花形ではあるんですが、これまでデータ化を目指してないです。それは、誰かこのDBの上に作ってください。。。

公理図式

公理図式というのは、命題に「命題を入れる変数」が入ってしまっているせいで、それ単体が公理というよりは、「命題を入れて新しい命題を作ることを許可する」というルールになってしまっているものです。

余計難しく言ってしまった感じがします…僕たちの言葉でいうと、「命題型自由変数を含む命題」を公理として扱うときに、それを公理図式と呼びます。例えば分出公理が公理図式の典型例でしょう。これは任意の集合$${X}$$と、$${x}$$を引数にもつ命題型自由変数$${\psi(x)}$$に対して、$${\psi(x)}$$が真であるような新しい集合$${A=\{x\in X\mid\psi(x)\}}$$の存在を保証します：

$${{}^\forall X \;{}^\exists A \;{}^\forall x\;[x\in A\leftrightarrow[x\in X\land\psi(x)]]}$$

これには$${\psi(x)}$$という命題型自由変数が入っているので、公理図式です。ここで困難になるのは「命題型自由変数の中に項型自由変数を引数にとることがある」ということです。このことは、これを書いている今この瞬間に気づきました。これは結構やばい問題だと思います。「命題型自由変数への命題の代入」という操作が非常に難しくなりそうです。ここは後で詰めましょう。。。できれば、公理図式も命題として扱えるなら扱いたいなと思ってます。

公理図式は「命題を代入して命題を得る機能」って面では推論規則に近い気もするんですけどね。僕ももともとそういう方針でコーディングしてたんですが、どんどんどんどん難しくなっていって頭を抱えて、今最初から考え直そーって思ってます。

定義

みなさん「～～～をほにゃららら～と定義します」とか気軽に言いますが、これ何気なく一言で「定義」というと思いますが、実はいろんな種類の定義を一つの言葉に詰め込んでます。僕は具体的に、定義を4つのことに絞りました：

  • 述語記号の定義

    • 例：結合法則・単位元の存在・逆元の存在を満たすものを「群」と定義する

  • 関数記号の定義

    • 例：$${c:=299792458}$$

  • 論理記号の定義

    • 例：$${P\iff Q}$$を$${P\Rightarrow Q}$$かつ$${Q\Rightarrow P}$$で定義する

  • 量化記号の定義

    • 例：$${\exist!P(x)}$$を$${\exists x[P(x)\iff\forall y[P(y)\Rightarrow y=x]]}$$で定義する

言われてみると、それぞれやってることが全然違うことが分りますかね？結局、僕はそういうのはそれぞれで「定義集」みたいなのを作るしかないなと思いました。こいつらの共通点は「命題である」というぐらいのことしかないです。

関数記号だけは等号記号「$${=}$$」で定義が可能です。それ以外は、同値を意味する記号「$${\iff}$$」を定義したうえで定義可能でしょう。僕は「定義」を、そういった命題を公理に追加することと定義しようとしています。

結局やりたいこと

まずは以下の基礎論の構成要素をデータ化(テーブル化)します：

  • 記号

  • 論理式

  • 推論規則

  • 公理

  • 定義

  • 定理

  • 証明

これらは外部キーでガッチガチに固めて、証明の正しさを保証したいです。

またこれらの情報入力時に、「論理式の構成手続き」や「推論規則の適用」に対するバリデーション等を行うインターフェースを構築したいです。

もっと言うと、これをデータベース化することで、ブルートフォース的に命題を量産することも可能でしょう。あるいは近年発展著しいAIによる数学研究もしやすくなるんじゃないか？そんなことを思って、数学DBを構想するに至りました。

恐ろしいことは、もしこのシステムの中にわずかなバグでも存在してしまったら、最悪、すべてが台無しになることです。もし実際にこのシステムを構築するなら、そのようなリスクに対するヘッジも重要になってくると思います。

「病み数学者、基礎論に走りがち」はちょい感じてるんですが、まあ僕は還俗した身ですから…。それでは次回、「記号」周辺の設計についてお話しようと思います。それではまた！

いいなと思ったら応援しよう！