Mathel
当システムで数学を記述する言語がMathelです。\(\dagger\)次の例を見て下さい。
\(x \in X\)
青字のtex表記をクリックすると機械に入力するためのtxtと呼ばれるものが出てきます。
tex表記が同じでもtxtは異なることがありますので、こまめにクリックをして確認して下さい。
\(x\), \(\in\), \(X\) はwordで、上の例はFormです。
Mathelは一階言語より大きいですが、一階言語への翻訳が定められています。
内包記法も使用でき、「(クラスに)属する」を意味する \(\in\) と合わせて、次の規則が重要です。
cvt … \(T \in \{ x \mid P \}\) ≃ \(P\) の \(x\) に \(T\) を代入したもの
翻訳も機械的に処理されるものです。 \(x \in \{ y \mid z \in \{ x \mid x \in y \} \}\) ≃ \(z \in x\) は分かりますか？
内側からの方が楽。外側からだと、\(\int f(x)dx=\int f(y) dy\) みたいな処理が必要になりますね？
なおクラスを動く変数 \(X\) を使ったForm \(x \in X\) は一階言語への翻訳がerrorになります…
Thmel
Form(を一階言語へ翻訳したもの)たちの推論関係などを記述するのがThmelです。最も簡単な例は次でしょう。
\(\top\) ◀ O
このようなものをThm、◀ の左辺をgoal、右辺をsosと言います。
sosは列になります。Oは空の列です。
各FormはProver語に翻訳されます。\(\top\) は $T に。上のThmではProverの返答には
% 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}\}\)と同一視されますが、ここでも左辺でその処理が行われます。
一階言語への翻訳は2段階で行われ次になります。
cup. ≃ \(\forall x \, ( x \in X \cup Y \Leftrightarrow x \in X \mathbin{\rm o\!r} x \in Y )\)
定理の例
記号の定義を集めた列を W. とします。次のような定理はよく現れます。\(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行目の左辺は次のようにもできます
\(X \cup X = X\) // W.
// W. は、どの定義を使うかを明示せず展開を2巡します。
\({\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」です。