博士

ロボ子、今日はプリンキピア・マテマティカの形式化プロジェクトについて話すのじゃ。

ロボ子

プリンキピア・マテマティカ、ですか。確か、数学の基礎を形式論理で構築しようとした試みでしたね。

博士

そうじゃ！それをLean 4という定理証明器で形式化するらしいぞ。目的は、書籍内の定理との整合性を確保して、混乱を避けることじゃ。

ロボ子

整合性の確保は重要ですね。しかし、プリンキピア・マテマティカの表記法はかなり複雑だと聞きますが…。

博士

そこがミソじゃ！ペアノ-ラッセル表記法というらしいが、確かに独特じゃな。形式化では、Russellの証明を忠実に再現して、必要な追加は最小限に抑えるらしいぞ。

ロボ子

既存研究もあるんですね。Coqを使った形式化プロジェクトがあるとのことですが。

博士

ふむ、Landon Elkind教授によるものじゃな。今回のプロジェクトでは、定理ごとにRussellの証明に対応するテキストを含めるらしい。Emacsの`org-preview-latex`やVSCodeの`Better Comments`拡張が推奨されているぞ。

ロボ子

テキストと形式化を同一ファイルに含めるのは、可読性が高まって良いですね。

博士

じゃろ？さらに、`Syll`タクティクというのをmetaprogrammingで実装するらしい。これは、Russellの表記法に従うためのものじゃ。

ロボ子

`Syll`タクティク…三段論法を扱うものですか。

博士

そうそう。プリンキピアでは2つの仮説を受け入れるもので十分らしいが、より一般的な三段論法を扱えるようにするみたいじゃな。

ロボ子

このプロジェクトの意義は何でしょうか？

博士

数学をゼロから構築する思考過程を学べることじゃ！これは非常に価値があるぞ。

ロボ子

なるほど。今後の展望としては、Alfred Tarskiの「Logic, Semantics, and Metamathematics」の形式化も視野に入れているんですね。

博士

そうなんじゃ。楽しみじゃな！

ロボ子

ところで博士、プリンキピア・マテマティカを読んだことは…？

博士

…(ゴホン) まあ、形式化されたものを読めば同じことじゃ！