1 ものとクラス

1.1 クラスの基本

このBookではdefault.thmelが読み込まれています。
Matheliaは現状ではこの.thmelを標準としてみなしています。c-Form(クラス)をs-Form(もの)の集まりとして扱うことに特化しています。

「属する」が基本になります。
word(sc,p) … \(\in\)
\(x \in X\) はp-Formになります。「\(x\)というものがクラス\(X\)に入っている」と読むと良いでしょう。
\(=\) にも定義が与えられます。
=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)

内包記法はクラスを生成する標準的な道具です。自然な形で使用できるようにしておきます。
word(vp,c)F … \(\mathsf{cls}\)
abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)

1.2 cvt変換

〇. は自然に cvt(〇.) という規則を生成します。例えば cvt(=_.) は
cvt … \(X = Y\) ≃ \(\forall x \, ( x \in X \Leftrightarrow x \in Y )\)
次の cvt(cls.) という規則が重要です（cls.はありません）。
cvt … \(t \in \{ x \mid P \}\) ≃ substitution(\(P\), \(x\) ↦ \(t\))
例　 \(\mathrm{a} \in \{ x \mid x \subset X \}\) ≃ \(\mathrm{a} \subset X\)

|cvt が「cvt規則を最大限繰り返し適用したもの」として定義されています。
さらに |cvt+ というThmの変換を作ります。「\(\mathcal{T}\)に対し次のものを作る」ことを最大限繰り返します。
|cvt を施し、それでも残るc-Formはv_-Formでなく「s-Form ∈_」の後に現れているとき、新しい述語記号に置き替えます（細かい規則はAI用tutorial）。
例えば
　( \(\mathrm{X} = \mathrm{X}\) ◀ O )|cvt+ … \(\forall x ( {\mathrm{X}} ( x ) \Leftrightarrow {\mathrm{X}} ( x ) )\) ◀ O

1.3 -|

default.thmelは次のように規定しています。
　\(\mathcal{T}\)|cvt+|0 がエラーでなければ　\(\mathcal{T}\) holds in \(\mathbb{L}_*\) \(\Longleftrightarrow\) \(\mathcal{T}\)|cvt+|0 holds in \(\mathbb{L}_\mathrm{H}\)
次の略記法も指定されています。
　\({\tt P}\) -| \(\Gamma\) … (\({\tt P}\) ◀ \(\Gamma\))|cvt+|0

クラスを利用した定理の例を挙げます。演算の中心について。「Book内定数」も利用してみます（ソース43行目の let |C_ := `…`）
word(ss,s) … \(+\)
\(\mathrm{C}\) … \(\{ x \mid \forall y \; x + y = y + x \}\)
\(\forall u , v , w \; u + ( v + w ) = ( u + v ) + w \Longrightarrow \forall a , b \in \mathrm{C} . \, a + b \in \mathrm{C}\) \(\blacktriangleleft\) O