第8章　辞書：命令語とオプションの一覧

Bookのソース（.bookファイル）を書くための命令語・ヘッダ・オプションの一覧です。使い方の説明と例は 0_tutorial_AI の 2〜7.book・practice.book にあります。
Bookは mathelia/フォルダ/名前.book に置きます。本の名前は「フォルダ/名前」（拡張子なし。例 articles3/1）で指します。
各行は「命令語 引数」の形です。命令語と引数の間は半角スペースです（全角スペースは区切りになりません）。空行は無視されます。
命令語の頭に ! を付けたもの（!prop !thm など）は、表示しないが査読には使う版です。ただし !txt だけは表示も査読もされないメモです。
知らない命令語や書き方の誤りは、コンパイル時に「ファイル:行番号 理由」の形のエラーになります。
以下で `式` はバッククォートで囲んだ Formel の式、名 は空白を含まない名前です。
命令語は Bookエディタと同じ色で示します：ヘッダの欄、見出し、命令、txt・br、prf と ; と投げ先、!txt、`Formel の式`。

8.1 ヘッダ

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

第9章　本文の命令語

9.1 地の文と見出し

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

9.2 word・abbr・lower

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

9.3 prop と let

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

9.4 thm と prf

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

9.5 prf の段

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

第10章　option と .thmel・.formel

10.1 option

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

10.2 .formel の行

Formel の言語を決めるファイルです。今あるのは common/default.formel です（ヘッダに formel 行が無い本はこれを読みます）。
name letter A-Z a-z … 文字の集まりに名前を付けます。
word tex_only \, \; \! !, { } _ ^ … 表示だけに使い、FCL 変換では無視する語。
[lDP] [letter][0-9]*'* … 正規表現に名前を付けます。
word v-Form [lDP] など … 変数・定数・引数をとる記号の綴りを正規表現で決めます。

10.3 .thmel の行

thm・prf の関係と投げ先を決めるファイルです（ヘッダに thmel 行が無い本は default.thmel を読みます）。今あるのは common/default.thmel（標準）、common/zf.thmel（default と探索秒数だけが違うもの：Prover9 10秒・Vampire 90秒）です。
ふつうは thmel 行を書かず default.thmel を使います（articles・standard_math の本もそうです）。zf.thmel は Vampire に20秒より長くかかる段があるときに使います。
2つの .thmel の違い（ファイルの記述そのまま・2026-10-11）：

	default	zf
投げ先（backend）	p v h s
Prover9 の秒	20	10
Vampire の秒	20	90

backend p=prover+ v=vampire+ s=satallax+ h=hyperion … 投げ先の文字と backend の対応。
関係 -|・--| の意味は Thmel が決めていて、.thmel には書きません（goal -| sos ＝ (goal ◀ sos)|cvt+|0、goal --| sos ＝ (goal ◀ sos)|fn-elim|cls-elim +sos Wc.）。
prover9 search:seconds 20、vampire search:seconds 20 … 1回の問題を待つ秒数（default）。
prover+ problem:split / problem:whole … goal を割るかの既定（段ごとの p[whole]; が優先）。
satallax+ predicate:formula / predicate:all … satallax+ の述語変数の ∀ と \cls の内包が何を走るか。書かなければ formula（Book の式で書ける述語だけ＝ZF の公理図式として読む）。all（λ項すべて＝高階論理として読む）と書いた本だけ、∀ を書いた prop を --| … s; の段の sos に素の名前で書けます（7.book）。今ある2つの .thmel はどれも書いていません（formula）。