Mathel

Matheliaで数学を記述する言語がMathelです。次の例を見て下さい。
　\(x \in X\)

青字のtex表記をクリックすると機械に入力するためのtxtと呼ばれるものが出てきます。
tex表記が同じでもtxtは異なることがありますので、こまめにクリックをして確認して下さい。

Mathelで使われる記号をwordと言い、「wordの列」のうち文法をみたすものをFormと言います。
Formにはs-Form, c-Form, p-Formがあります。\(\dagger\)
\(x\), \(\in\), \(X\) はwordで、上の例はp-Formです。

「文法をみたすもの」と言いましたが、正確な定義は長々となりそうですよね！？
私たちは機械でシステムを作っています。だから実用的には「会員ページでcheckをしてOKならForm」です。

諸注意

Formのtxtにおいて半角スペースがwordの区切りになります。
ただし \((\) \()\) の前後だけは、半角スペースを省略できます。

wordの結合力の差は自然に利用されます。例　 \(x = y \Rightarrow y = x\) ≈ \(( x = y ) \Rightarrow ( y = x )\)
結合力の等しいものは通常は左から読まれます。例　 \(P , Q , R\) ≈ \(( P , Q ) , R\)

\, \; \! { } _ ^ はtex cmdになるだけのwordです。
「\(X\)上の恒等写像」は \(\text{id} X\) ではなく \(\text{id} _ X\) とされることが多いです。これはs-Formです。

\(X\) が集合を動く変数である一方、\(X\) はクラスを動く変数となります。
「(クラスに)属する」を意味する \(\in\) を使った \(x \in X\) もp-Formです。

Prop、一階言語への翻訳

よく使用されるp-Formには名前が付けられ、Propと呼ばれます。
「等号の定義」は次になります。一般に 〇. は「〇の定義」という位置づけになります。
　=. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)
クラスの等号は \(=\) で、次が定義になります。
　=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)

Mathelは一階言語より大きいですが、一階言語への翻訳が定められています。
翻訳は =_. のような定義(から自動で作られる規則)によって主に行われます

Thm

p-Form(を一階言語へ翻訳したもの)たちの推論関係などの記述が重要です。
最も簡単な例は次でしょう。
　 \(\top\) ◀ O

このようなものをThm、◀ の左辺をgoal、右辺をsosと言います。Oは空の列です。
Thmにもtxtがあります。上のThmはtxtでは `⊤` ◀ O となります。

当システムでは一階論理は仮定されます。次のThmは引っ掛かりやすいかもしれません。
　\({\perp}\) ◀ \(x \neq y\)

最低限の説明は以上です。

Matheliaを使うと、数学の教科書を作る事、論文の査読を行う事、が誰にでもできます。
それはbookを作成して行います。bookにはword, Prop, Thm などのデータを並べます。
標準的な数種類のbookはデフォルトで準備されています。ぜひ最初のbookをご覧下さい。
ほとんどは読めば分かるはずです！？そして分からないところはAIエージェントに聞くのが基本です。
また、bookを自作するときはAIエージェントに手伝ってもらえます。