cvt
cvtと呼ばれるタイプの変換規則があります。例えばcvt({/}.) \(A \stackrel{{\tt /}}{\mathop{{\sf p}}} B\) ≃ \(\neg ( A \mathop{{\sf p}} B )\)
例 \(x \notin x\) ≃ \(\neg ( x \in x )\)
次が重要です。
cvt(cls.) … \(T \in \{ x \mid P \}\) ≃ \(P\) の \(x\) に \(T\) を代入したもの
例 \(x \in \{ X \mid X \notin X \}\) ≃ \(x \notin x\)
\(x \in \{ y \mid z \in \{ x \mid x \in y \} \}\) は内側から計算する方が楽です。
外側からだと、\(\int f(x)dx=\int f(y) dy\) みたいな処理が必要ですね？
cls( ) の引数になるもの、例えば {/}. や cls. を def と言います。
defには . が付き、〇. は「〇の定義」のような意味合いを持ちます。
defの集合で . の前の重複がないものを defs と言います。
一個の . で終わるものは略して良く {} が最も基本的なdefsになります。
Propとその翻訳
Propと呼ばれるものを用意しp-Formをreferすることとします。\(\dagger\)testというPropを作ってみましょう。
test … \(x \in \{ X \mid X \notin X \}\)
直接作ることもできます。p-Form \({\tt P}\) をreferするPropを `\({\tt P}\)` とします。例 `x in X`
Propとdefsを並べたものを Prop+defs と言います。
\({\tt P\,d}\) は「\({\tt P}\)がreferするものに\({\tt d}\)が誘導する規則を適用したもの」をreferします。
test {{/}., cls.} … \(\neg ( x \in x )\)
test {}
と書けます。\(\dagger\)
クラスの等号 \(=\) はword(cc,p)で、次のPropが定義とみなされます。
=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)
ここで \(X\) はword(,c)です。=_. も自然にdefになります。
cvt(=_.) … \(X = Y\) ≃ \(\forall x \, ( x \in X \Leftrightarrow x \in Y )\)
集合とクラス
集合をクラスとみなす仕組みもあり、必要があればs-Form \({\tt X}\) は \(\{x \mid x \in {\tt X}\}\) に置き換えられます。\(\emptyset\) はword(,s)ですが、その定義は次です。
\0. … \(\emptyset = \{ x \mid {\perp} \}\)
これは \(\{ x \mid x \in \emptyset \} = \{ x \mid {\perp} \}\) と変換され
\0. {} … \(\forall x \, ( x \in \emptyset \Leftrightarrow {\perp} )\)
外延性公理は \(X = Y \Longrightarrow X = Y\) という、表記上は自明なp-Formとなります。
クラスが集合になるのか？という問いは自然に生まれます。\(\dot\exists\) というword(c,p)の定義は
Exi. … \(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)
Mathelでは「Russelのパラドクス」を次のように端的に記述できます。
\(\neg \dot\exists \{ x \mid x \notin x \}\)
{}翻訳では Exi., =_., cls., {/}. というdefが使用されて
\(\neg \exists X ( x \in X \Leftrightarrow x \notin x )\)
Thm
Prop+defs は一階言語をreferしなければなりません。一般にはそれは長いFormになります。
しかし、一階言語では一階論理が使えます。
この形のものをThm、\({\tt X}\)をgoal、\({\mathcal A}\)をsosと言います。
Thmの中では {} も略せます。`x = y` -| O のように。O は空の列です。
\0. のような定義Propを集めたものを W. とします。\({\tt X}\) -| W. は「\({\tt X}\)は定義から示せる」と読めます。
ライブラリでは \(x \notin \emptyset\) -| W. のように記述されてしまいます。 「Thmが正しいか」の判定が大事です。
当システムではその最終判断はProver9に委ねられます。\(\dagger\)
Prover9に送る前にはThmを変形することが必要で、それをprepと言います。\(\dagger\)
上のThmなら -| W. を -| \0. にprepして送ればよさそうですね？
どうやったら \0. は見つかるのでしょう？
prepには試行錯誤が必要で、その戦略を磨くことが課題です。
Thm自体の作成、さらには数学理論の作成まで、システムに行わせることが夢です。
終わりに
数学は記号列を変形していくゲームです。
これで最低限のルールが分かったと思いますので、ぜひライブラリをご覧下さい！
ライブラリでは記号や変換規則や定理などを蓄積しています。
なおライブラリでは、記述は淡々と行われ、記号の意味や読み方を与えたり親切に説明をすること等は基本的にありません。
私たちは会員を募集しています。
ルールの詳細などの私たちの発明の核心的な部分は非公開です。ぜひ会員になって共に議論しましょう！
代表：須田智彦[t@mshk1201.com]まで。
Formの定義を見たとき「文法をみたすってどういうこと？」と思いましたか？
本当は(会員ページで実行できる)form_checkをしてキチンと結果が返ってくるものがFormです。
また、oracleはthm_checkのページで受けることができます。