book集

txt もう一つの例として、同値関係の特徴づけを与えます。
word :R :T :X
lower :R
lower :T
lower :X
word ∈_
word \cls
abbr cls
prop =_.
thm `[|??p^] :R&:T&:X ⟺ [ ∀ a ; b \, ( a |??p^ b ⟺ \{ cls x | x |??p^ a \} =_ \{ cls x | x |??p^ b \} ) ]` -| O
prf goal -| O p;

section slashを使った証明
txt このbookでは $\cup$ の冪等性 を目標とします。
word ∪
prop =.
prop ∪. <- `X ∪ Y =_ \{ cls x | x ∈ X or x ∈ Y \}`
txt $\cup$ の冪等性
thm `X ∪ X = X` -| W.
prf goal // W. -| O p; goal -| W. h;

section 一意量化子
abbr ！
abbr ∃！
br
abbr ！+
abbr ∃！+

section word版・abbr版の比較で分かったこと
txt 綴りについて：abbr版（構文展開だけで完結する版）は、wordG1版と同じ綴り`！`・`∃！`を共有します。区別は使い方（構文上の位置）だけで付きます——wordG1版は`！ x (P)`のように直接適用し、abbr版は`[ ！ x P ]`のように大かっこで囲みます（`cls`・`fn`等、同じ綴りが複数の役割を兼ねる既存の作法と同じです）。制限付き版（`$_A`で範囲を絞る形）はabbr版のみ用意されており、綴りを`！+`・`∃！+`として区別します。
txt `！`（wordG1版）は、多ソート翻訳（`--|`・`--| … v;`）で`P^`が正しく展開されないバグを一度持っていました（2026-09-11に発見・修正済み）。修正前は、`P^`を含む定義を多ソート経路で使うと「`P^`はProver語への翻訳を持たない」という理由で拒否されていました。abbr版の`！`はMathel→TSL段階で展開が完結するため、そもそもこの種のバグが起きようがない設計です。
txt この経緯から「単ソート`-| … p;`にも同種の欠陥が残っているのでは」という仮説を立て、`！ x (x = 変数)`という形を実際に試しました。最初は「述語が変数を参照すると証明できない」ように見えましたが、調べ直すと比較の作り方自体に誤りがありました——`！ x (x = |c)`（通常の等号`=`）と`！ x (x =_ w)`（クラスの等号`=_`）という別の述語を比較していたのです。
txt `=_`は外延性を経由する定義（`X_ =_ Y_ ⟺ ∀x(x∈_X_⇔x∈_Y_)`）なので、`x =_ w`から`x=y`型の帰結を導くには外延性そのものを補助知識として使う必要があり、それを与えずに`not_proved`となるのは正しい挙動でした。等号を揃えて`！ x (x = w)`（通常の`=`）で試し直すと、単ソートでも正しく`proved`になり、abbr版の`！`と一致しました。
!txt 擬陽性（誤って`proved`になってしまう）方向も別途確認しました。sosと goal に同じ名前の自由変数（`y`,`w`）を分けて書くとProver9側の変数束縛の扱いにより見かけ上おかしな判定が出ることがありましたが、これも比較の作り方の問題で、`∀y∀w(...)`と明示的に束縛した自己完結の形に直せば、word版・abbr版とも正しく`not_proved`（偽の主張は証明されない）に揃いました。単ソートのword版・abbr版いずれにも、この調査で新たな擬陽性は見つかっていません。
txt 教訓：「動きが違う」と思ったら、まず比較している対象が本当に同じ主張かどうかを疑うこと。今回は`=`と`=_`という似て非なる記号を取り違えたことが原因でした。査読が機械的に厳密である一方、人間（やAIエージェント）が書くテスト自体にも同じ厳密さが要ります。
br
txt 結論として、word版`！`/`∃！`自体に単ソートでの新しい欠陥は見つかりませんでした。ただし、実際に見つかった多ソートのバグと、バックエンドごとに展開処理を複製せずに済むabbr版の設計上の単純さ（Mathel→TSL段の構文展開1回で完結する）を踏まえ、新しくBookを書くときはabbr版（`[ ！ x P ]`・`[ ∃！ x P ]`、制限付きなら`！+`・`∃！+`）を使うことを推奨します。wordG1版`！`/`∃！`は既存の利用箇所（`1_basis/4_ZF.book`・`book1/book1-1.book`）があるため削除はしていませんが、新規利用は避ける方向です。

1_basis/6.book

`1_basis/6.book`