Thm
Mathelは一階言語に翻訳されると、長ーくなりがちです。
しかし一階言語では一階論理が使えます。
一階言語に翻訳された上で「\({\tt X}\)が\({\mathcal A}\)から推論される」ことを \({\tt X}\) ◀ \({\mathcal A}\) と表します。
この形のものをThm、\({\tt X}\)をgoal、\({\mathcal A}\)をsosと言います。
その最終段階はProver9に委ねられます。
Thmの各Formが、一階言語に翻訳され、さらにProver9の言語に翻訳され、Prover9に送られます。
Prover9からの返答はoracleと呼ばれ、会員は◀をクリックすると見れます。\(\dagger\) 一般にsosは列ですが、空の列はOとされます。
\({\tt X}\) ◀ O となる \({\tt X}\) は tautology と言われることがあります。最も短いものは次でしょう。
\(\top\) \(\blacktriangleleft\) O
\(\top\) はProver語の $T に変換されてProverに送られます。oracleの一行だけお見せしましょう。
% Length of proof is 2.
Russelのパラドクスもtautologyです！？
\(\neg \dot\exists \{ x \mid x \notin x \}\) \(\blacktriangleleft\) O
% Length of proof is 5.
prep
\0. のような定義Propを集めた列を W. とします。\({\tt X}\) ◀ W. は「\({\tt X}\)は定義から示される」と読めます。\(x \notin \emptyset\) \(\blacktriangleleft\) W.
はどうでしょう？そのままProverに送るのはやめた方がいいですよね？W. は大きすぎます。
一般にProver9に送る前にはThmを変形することが必要で、それをprepと言います。\(\dagger\)
\(x \notin \emptyset\) ◀ \0.
にすれば良さそうですね？人間は勘で \0. を見つけることができます…
「私たちにとって」は証明＝prepです。
良いprepを見つけProver9の探索空間を小さくすることを目標にします。
証明の能力を上げる＝prepの戦略を磨く、ことが重要課題です。
prepにもいろいろな手段を用意する必要がありますね？
W.から\0.を選び出すようなことだけでは全くたりません。
人間も「〇〇を一つとって固定する」や補題の利用など様々なことをします。
ruleとslash
よく使われるprep手段にslash計算があります。
これも機械にとっては容易に高速に実行できるものです。
rule(\0.) … \(x \in \emptyset\) → \({\perp}\)
rule(W.)も自然に作られ、次のように計算されます。
\(x \notin \emptyset\) / W. ＝ \(\neg {\perp}\)
先ほどのThmに対しては次のprepが良いということになります。
\(x \notin \emptyset\) / W. ◀ O
終わりに
数学は記号列を変形していくゲームです。
これで最低限のルールが分かったと思いますので、ぜひライブラリをご覧下さい！
ライブラリでは記号や変換規則や定理などを蓄積しています。
なおライブラリでは、記述は淡々と行われ、記号の意味や読み方を与えたり親切に説明をすること等は基本的にありません。
私たちは会員を募集しています。
ルールの詳細などの私たちの発明の核心的な部分は非公開です。ぜひ会員になって共に議論しましょう！
代表：須田智彦[t@mshk1201.com]まで。