Mathel
当システムで数学を記述する言語がMathelです。\(\dagger\)次の例を見て下さい。
\(x \in X\)
青字のtex表記をクリックすると機械に入力するためのtxtと呼ばれるものが出てきます。
tex表記が同じでもtxtは異なることがありますので、こまめにクリックをして確認して下さい。
\(x\), \(\in\), \(X\) はwordで、上の例はFormです。
\(x\), \(X\) は特にv-Formとよばれ、集合を動く変数となります。\(\mathcal{X}\) や \(\alpha\) なども。
\(X\) はv_-Formでクラスを動く変数となります。「(クラスに)属する」を意味する \(\in\) を使った \(x \in X\) もFormです。
集合の量化だけでなくクラスの量化もできます。 \(\forall X P\) や \(\forall X P\) のように。
\(P\) はv^-Formで命題を動く変数です。
一階言語への翻訳
Mathelは一階言語より大きいですが、一階言語への翻訳が定められています。内包記法も使用でき、次の規則が重要です。
cvt … \(T \in \{ x \mid P \}\) ≃ \(P\) の \(x\) に \(T\) を代入したもの
ここで \(T\) や \(P\) はFormの穴(Formが代入されるもの)です。
そして変換規則の表現内では \(x\) はv-Formではなくv-Formの穴です。
次の翻訳は内側からやる方が楽です。
\(x \in \{ y \mid z \in \{ x \mid x \in y \} \}\) ≃ \(z \in x\)
外側からだと \(\int f(x)dx=\int f(y) dy\) みたいな束縛変数の名前替えが必要になります。
なお翻訳は一通りではありません。 \(x \in X\) や \(\forall X P\) などデフォルトの翻訳が無いものもあります…
Thmel
Form(を一階言語へ翻訳したもの)たちの推論関係などを記述するのがThmelです。最も簡単な例は次でしょう。
\(\top\) ◀ O
このようなものをThm、◀ の左辺をgoal、右辺をsosと言います。
sosは列になります。Oは空の列です。
各Formはそれぞれの言語に翻訳されます。\(\top\) はProver語では $T です。上のThmではProver9の返答に
% Length of proof is 2.
などと書かれています。check終了です\(\dagger\)
check内容は会員になると見ることができます。
当システムでは一階論理は仮定されます。次のThmは引っ掛かりやすいかもしれません。\({\perp}\) ◀ \(x \neq y\)
Prop
よく使用されるFormには名前が付けられ、Propと呼ばれます。「等号の定義」として次のPropが登録されています。一般に 〇. は「〇の定義」と読まれます。
=. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)
クラスの等号は \(=\) ですが、次のPropは一階言語への翻訳において使用されます。
=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)
「和集合の定義」 は次です。
cup. … \(X \cup Y = \{ x \mid x \in X \mathbin{\rm o\!r} x \in Y \}\)
集合\({\tt X}\)はクラス\(\{x \mid x\in{\tt X}\}\)と同一視されますが、ここでも左辺でその処理が行われます。
一階言語への翻訳は複数の段階を経て次になります。
cup. ≃ \(\forall x \, ( x \in X \cup Y \Leftrightarrow x \in X \mathbin{\rm o\!r} x \in Y )\)
Thmとそのcheckの例
記号の定義を集めた列を W. とします。次のようなThmはよく現れます。\(X \cup X = X\) ◀ W.
W. は無限列なのでこれをProver9に送ることは不可能です。どの定義を使っているか具体的に書いて
\(X \cup X = X\) ◀ =. , cup.
をProver9に送ると、次が返ってきます。
% Length of proof is 16.
/ 〇. は「〇の定義による展開」を行います。
\(X \cup X = X\) / =. = \(\forall x \, ( x \in X \cup X \Leftrightarrow x \in X )\)
\(X \cup X = X\) / =. / cup. = \(\forall x \, ( x \in X \mathbin{\rm o\!r} x \in X \Leftrightarrow x \in X )\)
2行目の左辺は次のようにもできます。// W. で、どの定義を使うかを明示せず展開を2巡します。
\(X \cup X = X\) // W.
\({\tt P}\) ◀ W. のcheckでは、\({\tt P}\) / W. ◀ O をProver9でcheckし、Hyperionというソフトで
\({\tt P}\) ◀ \({\tt P}\) / W. , W.
というメタ推論およびまとめをする、ということがあります。
\(X \cup X = X\) // W. ◀ O
の方がProver9にとっては簡単で、次が返ってきます。
% Length of proof is 6.
最低限の説明は以上です。
ぜひライブラリをご覧下さい。
ライブラリではword, Prop, Thmなどを蓄積しており、ほとんどは読めば分かるはずです！？
そして分からないところはAIエージェントに聞くのが基本です。
なおライブラリでは、記述は淡々と行われ、記号の意味や読み方を与えたり親切に説明をすること等は基本的にありません。
さらっと「文法をみたすものがForm」と言いましたが、その説明ってとても長くなりそうですよね？
私たちは機械でシステムを作っています。
だから本当は「会員ページで実行できるチェックをしてキチンと結果が返ってくるものがForm」です。