book集

section クラスの基本
txt クラスは素朴に「ものの集まり」と捉えるのが良いです。「属する」が基本になります。
word ∈_
txt `x ∈_ X_` はp-Formになります。「`x`というものがクラス`X_`に入っている」と読むと良いでしょう。
txt `=_` にも定義が与えられます（表示では = と同じ記号ですが、ソースでは <code>=_</code>＝クラスの等号です）。
prop =_.
br
txt 内包記法はクラスを生成する標準的な道具です。`\{ cls x | P^ \}` という自然な形で使用できるようにしておきます。
word \cls
abbr cls
txt 次の左辺では `$_X` が表記上無視されます。
abbr Cls
txt 次のものの左辺は特殊表記されています。$\sum_{i\in\{0,1\}}(i+1)=3$ という記述もできるようにします。
abbr -Cls

section -|

subsection cvt変換
txt 〇. は自然に cvt(〇.) という規則を生成します。例えば cvt(=_.) は
txt cvt …`$X =_ $Y` ≃ ‘∀ x \, (x ∈_ $X ⇔ x ∈_ $Y)‘
txt 次の cvt(cls.) という規則が重要です（cls.はありません）。
txt cvt …`$t ∈_ \{ cls ｘ | $P \}`≃ substitution(‘$P‘, ‘ｘ‘ ↦ ‘$t‘)
br
txt このBookではdefault.thmelが読み込まれています。Matheliaは現状ではこの.thmelを標準としてみなしています。
txt <code>|cvt</code> が「cvt規則を最大限繰り返し適用したもの」として<note>定義<?>「最大限繰り返す」は、適用できる規則が無くなるまでという意味です。確定した関数として扱うには、停止性と、適用順序によらないこと（または適用順序の指定）も必要です。</note>されています。
txt 次の翻訳は内側からやる方が楽です。 　`x ∈_ \{ cls y | z ∈_ \{ cls x | x = y \} \}`<code>|cvt</code> … ‘z = x‘
txt 外側からだと $\int f(x)dx = \int f(y)dy$ みたいな「束縛変数の名前替え」が必要になります。

subsection cvt+変換
txt <code>|cvt+</code> というThmの変換を作ります。「$\mathcal{T}$に対し次のものを作る」ことを最大限繰り返します。
txt 〇 $\mathcal{T}$<code>|cvt</code>
txt 〇 cvt(${\tt w}$.) がない gram(,c)でv_-Formでないword ${\tt w}$ があれば $\$x \in {\tt w}$ を `|?p^ ($x)` に替える(`|?p^` は$\mathcal{T}$に現れない)。
txt 〇 cvt(${\tt w}$.) がない gram(s,c)で?v_-Formでないword の ${\tt w}$ があれば $\$x \in {\tt w} (\$t)$ を `|??p^ ($t , $x)` に替える(`|??p^` は$\mathcal{T}$に現れない)。
txt 〇 $\mathbb{W}$(ss,c) などに対しても同様。
txt 新しい述語(`|?p^`など)の割当てはThm全体で保持します。既存のwordとは衝突させず、引数の順序とソートを保存します。
txt 例えば
txt 　(`|X_ =_ |X_` ◀ O )<code>|cvt+</code> … ‘∀ x (|?X^ (x) ⇔ |?X^ (x))‘ ◀ O

subsection 定義
txt default.thmelは次のように規定しています。
txt 　$\mathcal{T}$<code>|cvt+|0</code> がエラーでなければ　$\mathcal{T}$ holds in $\mathbb{L}_*$ $\Longleftrightarrow$ $\mathcal{T}$<code>|cvt+|0</code> holds in $\mathbb{L}_\mathrm{H}$
txt default.thmelには次の略記法も指定されています。
txt 　${\tt P}$ -| $\Gamma$ … (${\tt P}$ ◀ $\Gamma$)<code>|cvt+|0</code>
br
txt クラスを利用した定理の例を挙げます。演算の中心について。`+` が結合的なら、可換なものどうしの和もまた可換です。
word +
let |C_ := `\{ cls x | ∀ y \; x + y = y + x \}`
thm `[ ∀ u ; v ; w \; u + (v + w) = (u + v) + w ] ⟹ [ ∀ a ; b ∈_ |C_ . \, a + b ∈_ |C_ ]` ◀ O
prf goal -| O p;

newpage

section --|

subsection cls-elim変換
txt <code>|cls-elim</code> というThmの変換を作ります。「$\mathcal{T}$に対し次のものを作る」ことを最大限繰り返します。
txt 〇 `\{ cls x | $P \}` (この内包全体が自由なv-Form,v_-Formを含まない) があれば `|X_` に置き替え sos に `x ∈_ |X_ ⇔ $P` を追加する(`|X_`は$\mathcal{T}$に現れない)
txt 〇 `\{ cls x | $P \}` (この内包全体の自由なv-Form,v_-Formは v-Form `$z` だけ) があれば `|?X_ ($z)` に置き替え sos に `x ∈_ |?X_ ($z) ⇔ $P` を追加する(`|?X_`は$\mathcal{T}$に現れない)
txt 〇 `\{ cls x | $P \}` (この内包全体の自由なv-Form,v_-Formは v_-Form <code>$Y_</code> だけ) があれば <code>|?_X_ ($Y_)</code> に置き替え sos に <code>x ∈_ |?_X_ ($Y_) ⇔ $P</code> を追加する(<code>|?_X_</code>は$\mathcal{T}$に現れない)
txt 〇自由変数が2個以上でも同様
txt x は cls が束縛する変数です（∀ x と同じ規則）。$P の中の x は自由な出現に数えません。例えば `\{ cls x | x = x \}` は自由な変数を含みません。
txt 例えば
txt 　(`y ∈_ \{ cls x | x = x \}` ◀ O)<code>|cls-elim</code> … `y ∈_ |X_` ◀ `x ∈_ |X_ ⇔ x = x`

subsection 定義
txt Book内の自動変数 $\mathbb{W}_+.$ は「〇. (〇 はgramにcを含む) という形のpropすべての列」です。
txt Thmの簡単な演算に +sos があります。(${\tt P}$ ◀ $\Gamma$) +sos $\Delta$ は ${\tt P}$ ◀ $\Gamma,\Delta$ です。
txt default.thmelは次の記述もあります。
txt 　$\mathcal{T}$ holds in $\mathbb{L}_*$ $\Longleftrightarrow$ $\mathcal{T}$<code>|cls-elim</code> +sos $\mathbb{W}_+.$ holds in $\mathbb{L}_\mathrm{Hsc}$
txt 　${\tt P}$ --| $\Gamma$ … (${\tt P}$ ◀ $\Gamma$)<code>|cls-elim</code> +sos $\mathbb{W}_+.$
br
txt ここでも ${\tt P}$ -| $\Gamma$ と ${\tt P}$ --| $\Gamma$ が「意味を持つ限り」同値か、が重要な問題になります。
txt 次のThmは -| では意味を持たないです。<code>|cvt+</code> で `x ∈_ A_` が残るため。
thm `x ∈_ |B_` ◀ `x ∈_ A_`
prf `x ∈_ |B_` --| `x ∈_ A_` v;
txt このThmが通るのは、前提 `x ∈_ A_` が「すべての x がすべてのクラス A_ に属する」という強すぎる主張だからです（A_ に |B_ を入れれば goal そのもの）。意味のある定理ではなく、-| と --| の違いを見せるための例です。前提の点検の仕方は AI 用 tutorial の 0_tutorial_AI/6b.book にあります。

newpage
section アロー関数
word \fn
abbr fn
txt アロー関数は1項関数（gram の返り値が (s,s) の値）を作ります。項に適用するには、<code>?f (x)</code> と同じく直後に ( 引数 ) を書きます。ソース <code>｢ fn x ↦ x + a ｣ ( b )</code>、表示は `｢ fn x ↦ x + a ｣ ( b )` です。<code>｢</code> <code>｣</code> は半角のかぎ括弧（U+FF62・U+FF63）です。全角の「 」とは別の文字で、「 」と書くと拒否され、半角の ｢ ｣ を案内されます（旧綴り <code>\[</code> <code>\]</code> は2026-09-30 に廃止）。
txt word <code>ap</code>（<code>f ap (x)</code>）は、対の集合としての関数 f に代入する別の語です。gram は (ss,s) なので、アロー関数（(s,s) の値）に書くと型が合わず Form になりません（「「ap」の引数1には集合(s)が必要ですが…」というエラー）。
txt 次の cvt(fn.) という規則が重要です（fn.はありません）。
txt cvt …`｢ fn ｘ ↦ $X ｣ ( $t )`≃ substitution(‘$X‘, ‘ｘ‘ ↦ ‘$t‘)
br
txt $\mapsto$ の前のv-Formを `●` に替えられます。その際 `● ↦` は略されます。
txt 例　`｢ fn ● + a ｣` ≈ `｢ fn x ↦ x + a ｣`
txt `｢ fn ● ｣` は恒等写像です。
txt `●` は入れ子では使用すべきでありませんが、必ず内側から計算されます。
txt 例　`｢ fn ● + ｢ fn ● + a ｣ ( x ) ｣` ≈ `｢ fn ● + (x + a) ｣`

0_tutorial/5.book

`0_tutorial/5.book`