book集

section 例で見るMathelia
txt Matheliaは堅牢な数学を作成するためのソフトです。数学はBookに書き、それを機械が検査（査読）します。
txt <div style="border-left:4px solid #0b64c8;background:#f3f7ff;padding:6px 10px">Matheliaは、AI が Book を書き、人間はできた Book を鑑賞するという使い方を想定しています。そのため書き方には曖昧さを残さず、書いたものは書いた通りに、すべて機械的に検査されます。この Book は、AI（と人間）が最初に読む説明です。</div>
txt Mathelia で何ができるか・何が弱いか・これから何が入るかの概観は 0.book にあります。
txt 3つの例で、①Thm と prf、②記号の紹介と前提、③定数と前提の足りないとき、を順に見ます。どの例もこのBookに実際に書かれていて、査読を通ります。
txt 以下では、ソースの行を説明のために <code>このような表示</code> で再掲します。.bookファイルにはその行をそのまま書きます。式はバッククォート &#96; &#96; で囲んで書きます。

subsection 例1　Thm と prf
thm `x = y ⟹ y = x` ◀ O
prf `x = y ⟹ y = x` ◀ O p;
txt ソース（.bookファイル）では次の2行です。
txt <code>thm &#96;x = y ⟹ y = x&#96; ◀ O</code>
txt 　thm はThm（主張）を書く命令です。A ◀ Γ は「◀ の右に並べた前提の列 Γ から、左の式 A が推論できる」と読みます。A を goal、Γ を sos（set of support＝前提の集まり）と言います。
txt 　O（大文字のオー）は空の列です。この例では ◀ の右に前提が何も無く、x = y は goal（x = y ⟹ y = x）の一部です。
txt 　x, y は変数で、「すべての x, y について」の意味になります。
txt 　= と ⟹ は、ヘッダの <code>import /common/word_logic</code> で読み込んだ Book が紹介済みの記号なので、そのまま使えます。その Book が紹介している主な記号は次のとおりです。
txt 　　⊤（真）　⊥（偽）　¬（否定）　and（かつ。表示は「,」）　or（または）　⇒ ⇔（ならば・同値）　⟹ ⟺（結合の弱い ならば・同値）　∀ ∃　=　{/}（否定。x {/}= y は x ≠ y）
txt 　結合は、+ などの演算が = より強く、= が and より強く、and が ⟹ より強くなります（x = y and y = z ⟹ x = z は (x = y and y = z) ⟹ x = z）。迷ったら括弧を付けます。
txt <code>prf &#96;x = y ⟹ y = x&#96; ◀ O p;</code>
txt 　prf は直前の Thm の確かめ方を書く所で、表示はされません。確かめ方はいくつかの段階に分けて書くこともできますが、この例は1回で済むので、Thm と同じ形をそのまま書き、末尾に投げ先を付けます。
txt 　p; は「prover+（内部で自動定理証明器 Prover9 を使う）に投げる」という意味です。自分で証明を1歩ずつ書く代わりに、証明器に「この前提からこの式が出るか」を探させます。投げ先はほかに v; s; h; があります（3.book）。
txt ここまでで最小のBookが書けます。次の7行が Mathelia の「Hello World」です。まずこれを動かしてください。Bookの一覧のページ（/book_collection/）で新しいBookを作り（ログインが必要）、7行を写して保存し、査読すると OK になります。
txt 　文字コードは UTF-8（BOM なし）です。⟹ ◀ などの記号は Unicode の文字そのもので書くので、この頁からコピーするのが確実です。ログインせずに作業するときは、同じ内容を .bookファイルとして置いて CLI で査読します（「CLIから査読する」の章）。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">title 最初のBook import /common/word_logic formel /common/default thmel /common/min --- thm &#96;x = y ⟹ y = x&#96; ◀ O prf &#96;x = y ⟹ y = x&#96; ◀ O p;</div>

subsection 例2　記号の紹介と前提
word +
prop +結合則 <- `x + (y + z) = (x + y) + z`
thm `x + (y + (z + w)) = ((x + y) + z) + w` ◀ +結合則
prf `x + (y + (z + w)) = ((x + y) + z) + w` ◀ +結合則 p;
txt 「結合則を満たす演算なら、4つの項でも括弧を付け替えられる」という定理です。ソースでは次の4行です。
txt <code>word +</code>
txt 　記号 + は import した Book が紹介していないので、使う前に紹介します。表示の (ss,s) は + のgramで、「s-Form を2つ受け取り s-Form を返す」＝2項演算であることを表します。gram は DB に登録されていて、紹介すると表示されます。
txt 　ここでは + の意味（数の足し算など）は何も決めていません。分かっているのは次の前提だけです。
txt <code>prop +結合則 &lt;- &#96;x + (y + z) = (x + y) + z&#96;</code>
txt 　prop は式に名前を付けます。名前を付けただけで、証明されたわけではありません。ここでは前提として ◀ の右に置きます。x, y, z は量化子（∀ ∃）で縛られていない変数なので、前提としても「すべての x, y, z について」の結合則になります。
txt <code>thm &#96;x + (y + (z + w)) = ((x + y) + z) + w&#96; ◀ +結合則</code>
txt <code>prf &#96;x + (y + (z + w)) = ((x + y) + z) + w&#96; ◀ +結合則 p;</code>
txt 　結合則を仮定しない演算では、この等式は一般には成り立ちません。実際、thm と prf の両方で ◀ の右の +結合則 を O に替えると、証明は見つからず、査読は FAIL になります。FAIL は「この前提からは確かめられなかった」ということで、主張が偽だという判定ではありません。

subsection 例3　定数と、前提の足りないとき
word ∈
prop 仮定1 <- `∀ x (x ∈ |A ⟹ x ∈ |B)`
prop 仮定2 <- `|a ∈ |A`
thm `|a ∈ |B` ◀ 仮定1 , 仮定2
prf `|a ∈ |B` ◀ 仮定1 , 仮定2 p;
txt 「A のどの元も B に属し、a が A に属するなら、a は B に属する」という定理です。ソースでは次の5行です。
txt <code>word ∈</code>
txt 　表示の (ss,p) は、∈ が「s-Form を2つ受け取り p-Form（命題）を返す」ことを表します。例2の + は s-Form を返し、∈ は p-Form を返します。
txt <code>prop 仮定1 &lt;- &#96;∀ x (x ∈ |A ⟹ x ∈ |B)&#96;</code>
txt <code>prop 仮定2 &lt;- &#96;|a ∈ |A&#96;</code>
txt 　|A, |B, |a のように | を付けたものは定数です。紹介せずに使えます。表示では | は消え、定数は立体（a）、変数は斜体（x）で示されます。
txt 　例2で見たとおり、量化子で縛られていない（集合・クラスの）変数は、前提の中でも「すべての値について」の意味になります。仮定1 の ∀ x は省いても同じ意味ですが、読みやすさのために書いています。
txt 　一方、仮定2 を |a ∈ |A でなく a ∈ A と書くと「すべての a, A について a ∈ A」という強すぎる前提になり、意図した定理ではなくなります。特定のものについて述べるときは定数を使います。
txt 　前提に書いたものの意味を表にまとめます（高階変数と schema は HOL.book・6.book で扱います）。
txt <table border="1"><tr><th>前提に書いたもの（ソース）</th><th>意味</th></tr><tr><td><code>x ∈ A</code>（量化子で縛られていない集合・クラスの変数）</td><td>すべての x, A について（全称で閉じる）</td></tr><tr><td><code>|a ∈ |A</code>（定数）</td><td>ある特定の a, A について</td></tr><tr><td><code>P^</code>・<code>?R^</code> を含む prop（高階変数）</td><td>Thm 全体の外側で1回だけ全称で閉じる＝goal と sos で同じ1つの命題・述語を指す（前提の中だけで閉じるのではない。式を代入して使うことはできない）</td></tr><tr><td>schema（<code>schema 名(…) :=</code>）</td><td>どの述語についても成り立つ前提。代入した実例 <code>名[?R^:=&#96;θ&#96;]</code> を段の sos に書いて使う</td></tr></table>
txt <code>thm &#96;|a ∈ |B&#96; ◀ 仮定1 , 仮定2</code>
txt 　前提が2つ以上あるときは ,（前後に半角スペース）で区切ります（表示では「，」になります）。旧い ,, は査読エラーです。
txt <code>prf &#96;|a ∈ |B&#96; ◀ 仮定1 , 仮定2 p;</code>
txt 　thm と prf の両方で ◀ の右を 仮定1 だけにする（仮定2 を外す）と、証明は見つからず、査読は FAIL になります。

section Bookの書き方
txt Bookは .bookファイル に記録され、表示ソフトで閲覧されます。
txt .bookファイルはヘッダと本文からなり、両者は --- という行で区切られます。各行は原則として<note>命令語で始まります<?>この行は txt という命令語で始まっています。命令語の一覧は後半の「辞書」の章にあります</note>（例外は、字下げして次の行に続けた prf の続きです）。上の例では thm・prf・word・prop が本文の命令語です。
txt ヘッダの行は次の意味です。
txt 　<code>title</code> … Bookの題。<code>author</code> … 書いた人。
txt 　<code>import /common/word_logic</code> … = ⟹ ∀ などの論理の記号を紹介済みの Book を読み込みます。書くときは .book を付けません（表示では付きます）。
txt 　<code>formel /common/default</code>、<code>thmel /common/min</code> … 式の言語と、Thm・証明の扱いを決める設定ファイルを指定します。
txt 保存すると、まずコンパイルで「書法にエラーが無く表示ができるか？」「他ファイルの読み込みはちゃんとできるか？」がチェックされ、表示されます。証明が正しいかは、次の査読で確かめます。

section Bookの査読
txt 査読はMatheliaの最も重要な機能で、「まだ紹介されてない記号が無いか？」「証明が正しいか」などを、文字通り「機械的に」チェックします。
txt それは、上から順に、そのBook（とimportされたBook）の「その位置までに紹介されたもの」に書かれていることだけで行われます。なおtxt行は人間のための説明であり査読では無視されます。
txt Bookを表示すると、各頁に「査読（この頁）」というボタンが出ます。押すと、紹介査読（語・prop などが使う前に紹介されているか）と Thm査読の結果が「紹介査読：…」「Thm査読：…」の2行で続けて出ます（下にまとめの1行はありません。まとめの総合判定は下の CLI が出します）。ヘッダに option review quick:true; と書いた本には「簡易Thm査読（この頁）」も出ます。結論のつなぎ（Hyperion）などを省いた速さ優先の Thm査読で、prf を試すときに使います（その OK は〇の根拠にはなりません）。Thm査読の表には Thm ごとに番号（#1.2-1 は 1.2 節の1番目の Thm。subsection の前にある Thm は #1-1 のように節番号だけ）と結果（通れば処理時間を添えた OK＝例 0.12秒 OK、落ちれば FAIL と理由）が並んで表示されます。
txt FAIL は査読に通らなかったことを示します。理由には、証明が見つからない場合（例2・例3の前提を外したとき）のほか、未紹介の記号を使った場合などがあります。例えば例2で word + の行を消すと、「本が紹介していない word を Form の中で使っています: +」という理由で FAIL になります。
txt 　CLI での査読結果は、例えば次のような行で返ります（Thm の番号・Thm または ファイル:行・結果）。
txt 　<code>#1.1-1　\(x = y \Longrightarrow y = x\) ◀ O　0.12秒 OK</code> 　<code>#1.2-1　1.book:35　FAIL: 本が紹介していない word を Form の中で使っています: +</code>
txt 　DB に無い記号を word で紹介しようとすると、査読より前のコンパイルの時点で「word は言語に無い綴りです: ♠」のようなエラーになり、表示もできません。
txt FAIL のときは理由を読み、記号を紹介する・前提を足す・証明を段に分ける（3.book）などをしてから、保存し直して再び査読します。
txt 査読されるのは保存済みの .book です。結果は頁ごとに保存され、前の頁やimportした本は、中身が変わっていなければ査読し直さず、保存された結果を使います。

section CLIから査読する
txt ブラウザの査読ボタンを押せない場合（AIエージェントが対話画面を持たずに作業しているときなど）は、Web画面の「査読」ボタンと全く同じ査読（紹介査読と Thm査読）をCLIから実行できます。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">cd /var/www/test2.atp-research.com && php wp-content/themes/lightning/mathelia/review_cli.php &lt;本の名前&gt; [頁番号] [--inputs]</div>
txt &lt;本の名前&gt;はフォルダ名/本の名前（拡張子なし。例 articles3/1）。頁番号は1から数え、省略すると本全体を査読します（「option review per-page:false;」を宣言した本では頁番号は効きません）。Webのエディタでも編集できるように、置いたファイルはグループを www-data、パーミッションを 664 にしておきます。
txt 実行すると、紹介査読の件数（落ちた行があれば行番号と理由）、各Thmの番号・結果（OK／FAIL、FAILなら理由）、全体の判定（例 総合判定: ALL OK（紹介査読 OK／Thm査読 OK））をプレーンテキストで返します。終了コードは0＝ALL OK、1＝紹介査読か Thm査読に FAIL あり、2＝引数や本の指定の誤り、3＝判定できない（コンパイルエラーなど。総合判定は「不明」）です。<code>--inputs</code> を付けると、FAIL した行の下に、落ちた段について prover+ などが受け取ったもの（翻訳した後の式）と、証明器へ投げた入力を、この順に出します（読み方は 3.book）。分割したときは入力が複数並び、1本ごとの結果（<code># 1/3 の結果：timeout</code> など）と、受理の条件（全部が proved なら認める）の集計も出ます。成功した段の入力は出しません。どの定義が開かずに残ったかなど、FAIL の原因を読むのに使います（6b.book）。式の読まれ方や slash の書き換えだけを確かめるときは、証明器に投げない次のコマンドを使います（2.book・4.book）。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">cd /var/www/test2.atp-research.com && php wp-content/themes/lightning/mathelia/slash_cli.php &lt;本の名前&gt; '&#96;式&#96; // W.'</div>
txt 式だけを書くと読まれ方（前置記法）が、<code>// W.</code> などを付けると書き換えた結果が返ります。自分で書いたThmが正しいかを確かめるのは、上の review_cli です。
txt DB の prop の本文は <code>'&#96;@名&#96;'</code> で見られます（例 <code>slash_cli.php articles3/0-pa '&#96;@+𝕄&#96;'</code>）。import する本にどんな定理があるかは、表示しない <code>!let/thm</code> などの補題も含めて、<code>grep -nE '^!?(thm|prop/thm|let/thm)' wp-content/themes/lightning/mathelia/articles3/0-pa.book</code> で一覧できます。表示しない補題も、import した本から使えます。
txt prf を探すときは、1つの Thm に prf の候補をいくつも当てて比べられます（本は書き換えません。外の AI も使ってかまいません）。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">cd /var/www/test2.atp-research.com && php wp-content/themes/lightning/.claude/prf_trial.php &lt;本の名前&gt; &lt;Thm の行番号&gt; '&lt;候補の prf&gt;' …</div>
txt 候補ごとに、通ったか・失敗した段・PHP と証明器の秒を JSON で返します。候補に <code>=</code> と書くと今の prf を測ります。<code>--quick</code> は結論のつなぎ（Hyperion）を省いた速い試しで、その ok は〇の根拠になりません。通った候補は本に書いて review_cli で確かめます。
txt 対象の Thm は、thm の行の行番号でも、その行の一部の文字列（一意に決まること）でも指せます。prf_trial は候補ごとに一時的な本を同じフォルダに作り、終わると消します。本の名前は拡張子なしで渡します（.book を付けても読めますが、表示が .book.book になります）。

section 次にすること
txt 〇例1の7行のBookに、例2・例3を書き足してみてください。
txt 〇ログインせずに作業するとき（AIエージェントなど）は、.bookファイルを /var/www/test2.atp-research.com/wp-content/themes/lightning/mathelia/フォルダ/名前.book に置き、上の「CLIから査読する」のコマンドで査読します。
txt 〇続きは 2.book（式の書き方 Formel）、3.book（Thmと証明 Thmel）、4.book（高度な表現）、5.book（ものとクラス）、6.book（集合とクラス）、6b.book（実践：投げ先・失敗・戦略）へ。高階変数と schema は HOL.book にあります。
br
txt ★Matheliaの仕様はまだ未確定のものも多いです。使用された方からの「こういう機能が欲しい」という建設的な意見をお待ちしております。

section Matheliaの部品
txt Matheliaは内部で独立性の高い部品を多く持っています。
txt 〇DB (データベース)は word・prop などのデータを保存します。
txt 〇数学の記述においては、Form（項や命題を表す記号の列）を扱う Formel、Thm を扱う Thmel が使用されます（詳しくは2.book, 3.book）。
txt 〇Thmを査読する backend(prover+, vampire+, satallax+, hyperion) はMatheliaの心臓部と言えます。prover+ は <a href="https://prover9.org/">Prover9</a> を、vampire+ は <a href="https://vprover.github.io/">Vampire</a> を、satallax+は <a href="https://www.ps.uni-saarland.de/~cebrown/satallax/">Satallax</a> を内部に持ちます。
txt 〇Mathelia本体はファイル操作・Book操作などを行う他、各部品間の橋渡しをします。
txt Bookの堅牢さを保証するためには、各部品を堅牢にし、部品間の情報のやり取りの流れを明瞭にすることが大事です。

section ファイルの基本
txt .bookファイルは文字コード UTF-8（BOM なし）で書きます。改行は LF でも CRLF でも構いません。
txt 　Shift_JIS などで保存すると「UTF-8 ではない文字があります」、BOM 付きの UTF-8 で保存すると「先頭に BOM があります」というコンパイルエラーになります。⟹ ◀ などの記号は Shift_JIS では表せません。
txt 記号は Unicode の文字そのもの（⟹ ∀ ∈ ◀ など）で書きます。これらの記号の以前の ASCII の綴り（==> all in など）は使えません。
txt 変数は英字1文字に数字や ' を付けたもの（x, A, x1, x'）とギリシャ文字（α, α1）などです。定数はその前に | を付けたもの（|a, |A1）です。
txt フォルダ名・Book名には半角の英数字と _ - を使います（例 0_tutorial_AI/1）。
txt 1行に1つの命令を書きます。長い prf だけは、次の行を字下げして続けられます。
txt 見た目が似ていても別の文字です。取り違えたときに出るエラーも挙げます。
txt 　⟹ と ⇒ … どちらも Formel の記号で、結合の強さが違います（2.book）。取り違えてもエラーにならないので注意します。
txt 　半角スペースと全角スペース … 命令語の後が全角だと「Unknown line kind」、式の中だと「この Formel の語でも変数・定数の綴りでもありません」。
txt 　&#96;（バッククォート）と &#8216; … thm で &#8216; を使うと「&#8216;式&#8216;（一階言語の式）は txt 行だけで使えます」。
txt 　∈ と ε … ε はギリシャ文字の変数になり、「Formとして消費されないwordがあります」。
txt 　◀ と ◁ … prf で ◁ を使うと「prf の段に書けない演算子です: ◁」。
txt 　-| の - と − （マイナス記号 U+2212）… thm で − を使うと「「−」（U+2212 マイナス記号）が使われています」。
txt 　, と ，・、 … 前提の区切りに ， や 、 を使うと「前提（sos）の区切りは半角の , です（前後に空白）」。旧い ,, や前後に空白の無い , も、その Thm の査読エラーになります。
txt 　O（大文字のオー）と 0（ゼロ）… ◀ 0 は「unintroduced sos name: 0」。
txt 　∅ と Ø … Ø は「この Formel の語でも変数・定数の綴りでもありません」。

newpage

section 辞書：命令語とオプションの一覧
txt <div style="border-left:4px solid #0b64c8;background:#f3f7ff;padding:6px 10px">ここから先は辞書です。初めて読むときは飛ばして 2.book へ進んで構いません。コンパイルエラーや査読エラーが出たとき、書き方を確かめたいときに引いてください。</div>
txt Bookのソース（.bookファイル）を書くための命令語・ヘッダ・オプションの一覧です。使い方の説明と例は 0_tutorial_AI の 2〜6・6b・HOL.book にあります。
txt Bookは mathelia/フォルダ/名前.book に置きます。本の名前は「フォルダ/名前」（拡張子なし。例 articles3/1）で指します。
txt 各行は「命令語 引数」の形です。命令語と引数の間は半角スペースです（全角スペースは区切りになりません）。空行は無視されます。
txt 命令語の頭に ! を付けたもの（!prop !thm など）は、表示しないが査読には使う版です。ただし <code>!txt</code> だけは表示も査読もされないメモです。
txt 知らない命令語や書き方の誤りは、コンパイル時に「ファイル:行番号 理由」の形のエラーになります。
txt 以下で <code>&#96;式&#96;</code> はバッククォートで囲んだ Formel の式、<code>名</code> は空白を含まない名前です。
txt 命令語は Bookエディタと同じ色で示します：ヘッダの欄、見出し、命令、txt・br、prf と ; と投げ先、!txt、&#96;Formel の式&#96;。

subsection ヘッダ
txt ヘッダは本文の前に書き、<code>---</code> だけの行で本文と区切ります。各欄は1回だけ書けます（option を除く）。
txt <code>title 題</code> … 必須。Bookの題です。
txt <code>author 名前</code> … 任意。
txt <code>import 本 本 …</code> … 他のBookが紹介した word・prop・abbr・lower と、証明済みの Thm（thm- 系を除く・6b.book「本を分ける」）を引き継ぎます。import した本の証明はやり直さず、保存された査読結果を使います。<code>/</code> で始めると mathelia/ からの位置（例 <code>/common/word_logic</code>）、始めなければ同じフォルダの本です。
txt <code>formel 名前</code> … 読み込む .formel（例 <code>/common/default</code>）。本文に Formel の式を書くなら必要です。
txt <code>thmel 名前</code> … 読み込む .thmel（例 <code>/common/min</code>、<code>/common/default</code>）。thm・prf を書くなら必要です。
txt formel・thmel は import した本から引き継がれません。本ごとに自分のヘッダに書きます。
txt <code>option 対象 名前:値;</code> … 表示・査読の設定です（下の「option」の節）。何行でも書けます。
txt <code>fragments 本 本 …</code> … 別ファイルの本文を順に取り込みます（現在の Book では使っていません）。

section 本文の命令語
subsection 地の文と見出し
txt <code>section 題</code>、<code>subsection 題</code> … 見出し。番号は自動で付きます（section は n、subsection は n.m）。Thm査読の番号は #n.m-k（subsection n.m の k 番目の Thm）で、subsection の前にある Thm は #n-k です。
txt <code>txt 文</code> … 地の文。HTML と MathJax（<code>\(…\)</code>）が使えます。査読されません。
txt 　txt の中でバッククォートで囲んだものは Formel の式として表示されます（書く本は formel の宣言が要ります）。<code>&#8216;式&#8216;</code> で囲んだものは一階言語の式として緑で表示されます（txt 行だけ）。
txt 　<code>&lt;note&gt;A&lt;?&gt;B&lt;/note&gt;</code> は A を表示し、クリックすると B を出します。
txt <code>!txt メモ</code> … 表示されないメモです（prf の中にも書けます）。
txt <code>br</code> … 空行を入れます。引数はありません。
txt <code>newpage</code> … 頁の区切りです。査読は頁ごとに行われます（option review per-page）。画面は続けて表示し、印刷ではここで改ページします。

subsection word・abbr・lower
txt <code>word 綴り 綴り …</code> … DB にある word を紹介します。1行に並べられるのは、紹介の見出し（分類と gram）が同じ語だけです。変数・定数・引数をとる記号（<code>?f</code> <code>|?p^</code> など）は紹介しません。
txt <code>word* 綴り …</code> … word と同じ紹介で、表示の仕方だけが違います（gram をそのまま出す）。
txt <code>!word 綴り …</code> … 表示しない紹介です。
txt <code>abbr 名前</code>、<code>!abbr 名前</code> … 省略表現の規則（abbr）を紹介します。
txt <code>lower 名前</code> … word+ を FCL へ下ろす規則（lower）を紹介します。word+ を式で使うには、その lower の紹介が要ります。
txt 紹介は使うより前に書きます。査読は、その位置までに紹介されたもの（import した本の分を含む）だけで行われます。

subsection prop と let
txt <code>prop 名</code> … DB にある prop を紹介して表示します。DB に無い名前でも、最初の数字の並びを <code>\n</code> に替えた名前の schema があれば、その実体として読みます（<code>prop ary1R</code> は <code>ary\nR</code> の n=1）。
txt <code>prop 名 &lt;- &#96;式&#96;</code> … 名前を付けた prop を自分で作ります。
txt <code>prop 名 &lt;- &#96;∀ ??p^ ( ψ )&#96;</code> … 「すべての述語 ??p^ について ψ」という prop です（式の外側に述語変数の ∀ を1つ書く）。<code>名[??p^:=&#96;θ&#96;]</code> で具体例を作れます（schema と同じ扱い・HOL.book・6.book の置換公理）。
txt <code>!prop 名</code> … 表示しない紹介です。
txt <code>prop 名 &lt;- schema名[P:=&#96;θ&#96;]</code> … schema（∀ を書いた prop も）の具体例に名前を付けます。
txt <code>let 名 &lt;- &#96;式&#96;</code> … Book の中だけの名前を式に付けます。表示されます（<code>!let</code> は表示しない）。置き直してよく、thm・prf で使ったときの中身が使われます。
txt <code>let |C_ := &#96;項&#96;</code> … Book 内の定数（| で始まる名前）。式の中に書くと項に展開され、証明器にも届きます。こちらだけは <code>:=</code> で書きます。
txt <code>form &#96;式&#96;</code> … 式を表示するだけです（査読の対象になりません）。
txt <code>schema 名(P;x,y) := &#96;ψ&#96;</code> … 命題変数・述語変数を含む schema の宣言です。∀ を書いた prop と同じ意味で、仮引数と共有変数を自分で宣言する書き方です（HOL.book を参照）。
txt <code>prop-family 頭 sos</code> … prop の族を紹介します（現在の Book では使っていません）。

subsection thm と prf
txt <code>thm goal 関係 sos</code> … Thm です。goal は prop の名前か <code>&#96;式&#96;</code>。関係は <code>◀</code> <code>-|</code> <code>--|</code> で、どれが使えるかは .thmel が決めます。sos は <code>,</code> で区切った prop の列、空の列は <code>O</code> です。goal が <code>&#96;式&#96;</code> のとき、prf の中では <code>goal</code> がその式を指します（prf の中で自分で <code>goal &lt;- …</code> と書くとその Thm の査読エラー）。
txt <code>prop/thm 名 関係 sos</code> … <code>prop 名</code> と thm を1行に。<code>prop/thm 名 &lt;- &#96;式&#96; 関係 sos</code> とも書けます。
txt <code>let/thm 名 &lt;- &#96;式&#96; 関係 sos</code> … let と thm を1行に。名前は後の Thm でも使えます（その Thm の prf の中だけで式を呼ぶなら <code>thm &#96;式&#96;</code> と <code>goal</code> で足ります）。
txt <code>!thm</code> <code>!prop/thm</code> <code>!let/thm</code> … 表示しない版です（査読はされます）。
txt <code>thm-</code> <code>prop/thm-</code> <code>let/thm-</code>（<code>!</code> 付きも）… private theorem です。その本の中（後の Thm・後の頁）では使えますが、import した本には運びません。<code>-</code> の無い Thm は、goal が <code>&#96;式&#96;</code> でも import した本で使えます（sos に <code>&#96;式&#96;</code> と引く）。
txt 使い分け：後の Thm・後の本から名前で引く定理は <code>prop/thm</code>（prop として紹介される）。式に名前を付けてその本の中で使うだけなら <code>let/thm</code>（Book 内のラベル）。名前が要らなければ <code>thm &#96;式&#96;</code>。細かい違いは 6.book・6b.book。
txt 行の末尾に <code>at \n=2..5</code> と書くと、n=2〜5 のそれぞれを査読します。確かめるのは書いた n だけです（すべての n についての証明ではありません）。
txt <code>prf 段 ; 段 ; …</code> … 直前の thm の証明です。thm の後、次の thm の前に1つだけ書きます（間に txt などがあってもよい）。長いときは、次の行を字下げして続けます。prf は表示されません。

subsection prf の段
txt 段は <code>;</code> で区切ります。証明器に投げる段は「goal 関係 sos 投げ先;」の形です（段の goal は <code>goal</code>・ラベル・<code>&#96;式&#96;</code>）。例 <code>&#96;x = y ⟹ y = x&#96; ◀ O p;</code>（第1頁の例1）
txt 投げ先の文字は .thmel の backend が決めます（p＝prover+、v＝vampire+、s＝satallax+、h＝hyperion）。投げ先は <code>;</code> の直前に空白なしで付けます。関係（◀ -| など）を含む段に投げ先が無いと査読エラーです（下のラベルだけの段は投げ先を持ちません）。
txt <code>p[whole];</code> … goal を断片に割らずに1つの問題として投げます。
txt 投げた段が OK になると、その段の Thm が既知の Thm として積まれます。
txt <code>名 &lt;- &#96;式&#96; ;</code> … prf の中だけのラベル（補題の式）。使うより前に書きます。式に名前を付けるのは <code>&lt;-</code> です。<code>名 &lt;- &#96;式&#96; 関係 sos p;</code> とすると、ラベルを付けてすぐ投げる1段になります。同じ prf で同じラベルを2回定義すると査読エラーです。
txt <code>名 := 〇[C_:=&#96;θ&#96;] ;</code> … prop の実例に名前を付けます（<code>:=</code>。<code>&lt;-</code> ではありません）。段の sos に <code>〇[C_:=…]</code> を直接書いても同じです（6.book「分出公理」）。
txt <code>|A_ := &#96;項&#96; ;</code>・<code>A_ := &#96;項&#96; ;</code> … Form（項）に名前を付けます。後の段の式の中で、その名前が項に置き換わります。bar 付き（<code>|A_</code>）は定数で示す段（固定化）の中で使う名前、bar 無し（<code>A_</code>）は変数の主張の中で使う名前です（3.book「固定化」・articles1/25.book）。
txt <code>goal 関係 sos h;</code> … hyperion に投げる結論の段。積まれた Thm から thm の主張を導けるかを確かめます。最後の h; の段が結論の段です。途中に置いた <code>名 &lt;- &#96;式&#96; 関係 sos h;</code> は、それまでの段をつないだ補題を積む段になります。
txt <code>goal 関係 sos h[fix];</code> … 定数（bar の付いた文字）で示した段をつなぎ、仮定ラベルを前件へ戻し、bar を外して変数の主張にする結論の段（3.book「固定化」）。集合に名前を付ける仮定 <code>|Y =_ θ</code> は、集合になる根拠があれば前件へ戻さずに消します（6.book「∃除去」）。
txt <code>goal -| sos h[lift];</code> … 多ソートで示した Thm（<code>◀</code>・<code>--|</code> の段）を、この <code>-|</code> の段でも使います（持ち上げ multisort→tfl。健全性は未証明で、その〇には印が付きます・3.book「h; の段の関係」）。書かない <code>h;</code> では使いません。<code>h[fix,lift];</code> のようにカンマで並べて書けます（空白は入れない）。
txt 投げた段がそのまま thm の主張を示しているとき（3.book の最初の例）は、結論の段は要りません。
txt 名前を付けない段（<code>&#96;式&#96; 関係 sos p;</code>）も書けます。後で引かない段には名前を付けません。
txt sos には prop の自由変数に式を代入した実例 <code>〇[C_:=&#96;θ&#96;]</code> を直接書けます（6.book「分出公理」）。
txt 段の goal には、次のものが使えます（/・//・W.・W.!〇. の説明は 4.book、@〇 は 3.book。以下の 〇 は prop の名前を入れる所です）。
txt 　<code>A / 〇.</code>（〇. で展開）　<code>//</code>（2回）　<code>/n 〇.</code>（n 番目だけ）　<code>W.</code>（定義の列）　<code>W.!〇.</code>（W. から 〇. を除く。空白を入れない）　<code>W.'</code>（証明済みの別定義を使う W.）
txt 　<code>@〇</code>（prop 〇 が指す式。Thm の中と、Book で作る prop の本文 <code>prop 名 &lt;- &#96;…&#96;</code> で使える。prop の本文では、その位置までに紹介した prop だけを引ける）
txt 　段の末尾（投げ先の前）の <code>{〇.'}</code>（別の定義でその段を翻訳）、<code>{〇.-}</code>（クラスへの所属を新しい述語に置き替える）
txt 　<code>goal [&amp;l -| A || &amp;r -| B] p;</code>（goal を連言の左右で分ける。<code>[⇒ … || &lt;= …]</code> は同値の向き）

section option と .thmel・.formel
subsection option
txt ヘッダに <code>option 対象 名前:値;</code> と書きます。宣言は <code>;</code> で区切り、1行に複数書けます。同じ宣言を2度書くとエラーです。
txt <code>option section format:第%n章　%t;</code> … section の見出しの形。<code>%n</code>（番号）と <code>%t</code>（題）をちょうど1つずつ含めます。既定は <code>%n %t</code>。
txt <code>option review per-page:false;</code> … 既定は true＝各頁に「この頁」の査読ボタンが出ます。false にすると最終頁に本全体の査読ボタンが出ます。
txt <code>option review quick:true;</code> … 既定は false。true にすると「査読」の隣に「簡易Thm査読」のボタンが出ます。結論のつなぎ（Hyperion）などを省いた速さ優先の Thm査読で、Book を書く・prf を試す段階に使います。結果は保存されず、その OK は〇の根拠になりません。
txt <code>option review original-relation:true;</code> … 本全体の査読ボタンの横に「原関係照合まで」のボタンを出します（現在の Book では使っていません）。

subsection .formel の行
txt Formel の言語を決めるファイルです。今あるのは common/default.formel です。
txt <code>name letter A-Z a-z</code> … 文字の集まりに名前を付けます。
txt <code>form s c p</code> … 使う Form の型。
txt <code>word tex_only \, \; \! !, { } _ ^</code> … 表示だけに使い、FCL 変換では無視する語。
txt <code>[lDP] [letter][0-9]*'*</code> … 正規表現に名前を付けます。
txt <code>word v-Form [lDP]</code> など … 変数・定数・引数をとる記号の綴りを正規表現で決めます。

subsection .thmel の行
txt thm・prf の関係と投げ先を決めるファイルです。今あるのは common/min.thmel（0_tutorial_AI の 1・3・4・HOL.book）、common/default.thmel（標準）、common/zf.thmel（default に satallax+（s;）を加え、Vampire の待ち時間を長くしたもの）です。
txt 新しい本では、import する本と同じ .thmel を使うのが無難です（articles の本の多くは zf.thmel）。
txt 3つの .thmel の違い（ファイルの記述そのまま・2026-10-07）：
txt <table border="1"><tr><th></th><th>min</th><th>default</th><th>zf</th></tr><tr><td>投げ先（target）</td><td>p v s h</td><td>p v h</td><td>p v s h</td></tr><tr><td>ソート（sort）</td><td>s c</td><td>s c f（\fn などを送れる）</td><td>s c f</td></tr><tr><td>-| の行</td><td><code>goal -| sos &lt;-&gt; (goal ◀ sos)|0</code>（|cvt+ を掛けない＝c-Form を含む段は FAIL）</td><td colspan="2"><code>goal -| sos &lt;-&gt; (goal ◀ sos)|cvt+|0</code></td></tr><tr><td>--| の行</td><td>無い（書くと査読エラー）</td><td colspan="2"><code>goal --| sos &lt;-&gt; goal|sc ◀ sos|sc</code></td></tr><tr><td>Prover9 の秒</td><td colspan="3">10</td></tr><tr><td>Vampire の秒</td><td>書いていない（査読の既定 20）</td><td>20</td><td>90</td></tr></table>
txt <code>backend p=prover+ v=vampire+ s=satallax+ h=hyperion</code> … 投げ先の文字と backend の対応。
txt <code>target p v s h</code> … この環境で使える投げ先。
txt <code>sort s c</code> … 多ソートの型として宣言するソート。
txt <code>translate 0 sc</code> … 使う翻訳。
txt <code>inference goal -| sos &lt;-&gt; (goal ◀ sos)|cvt+|0</code> … 関係の定義（この行が無い関係は使えません。min.thmel は |cvt+ を掛けない <code>(goal ◀ sos)|0</code>）。
txt <code>prover9 search:seconds 10</code>、<code>vampire search:seconds 20</code> … 1回の問題を待つ秒数。
txt <code>prover+ problem:split</code> / <code>problem:whole</code> … goal を割るかの既定（段ごとの <code>p[whole];</code> が優先）。
txt <code>satallax+ predicate:formula</code> / <code>predicate:all</code> … satallax+ の述語変数の ∀ と \cls の内包が何を走るか。書かなければ formula（Book の式で書ける述語だけ＝ZF の公理図式として読む）。all（λ項すべて＝高階論理として読む）と書いた本だけ、∀ を書いた prop を <code>--| … s;</code> の段の sos に素の名前で書けます（HOL.book）。今ある3つの .thmel はどれも書いていません（formula）。

0_tutorial_AI/zz1_pb.book

`0_tutorial_AI/zz1_pb.book`