book集

section 例から
txt この Book は Formel（式の書き方）の説明です。ヘッダの <code>formel /common/default</code> で default.formel を読み込んでいます。
txt まず、この頁で使う記号を紹介します（紹介のしかたは次の節）。
word ∈
word ∈_
word and or ⇒ ⇔
word ∀
txt 次の4つは、どれも正しい式です。表示では _ や | が見えなくなるので、ソースの綴りを並べます。「…」は読み方の目安です（式の意味は、後で定義や公理を置いて初めて決まります）。
txt 　① `x ∈ X` 　　ソース <code>x ∈ X</code> 　… 集合 x が集合 X に属する
txt 　② `x ∈_ X_` 　　ソース <code>x ∈_ X_</code> 　… 集合 x がクラス X_ に属する（∈ とは別の記号 ∈_）
txt 　③ `∀ x (x ∈ A ⇒ x ∈ B)` 　ソース <code>∀ x (x ∈ A ⇒ x ∈ B)</code> 　… A の元はすべて B の元
txt 　④ `P^ and Q^` 　　ソース <code>P^ and Q^</code> 　… 命題 P^ と命題 Q^ の両方
txt 次は式になりません。
txt 　⑤ ソース <code>x_ ∈_ X_</code> 　… ∈_ の左には集合（s-Form）しか置けないが、x_ はクラス（c-Form）
br
txt 用語：Formel で使われる記号をword、wordの列のうち文法をみたすものをFormと言います（①〜④はForm、⑤はFormでない）。
txt Formには3種類あります（default.formel の <code>form s c p</code>）。
txt 　s-Form … 集合を表す項（x、X、?f (x) など）
txt 　c-Form … クラスを表すもの（X_ など）
txt 　p-Form … 命題を表すもの（①〜④ など）
txt Formは高階{s,c}ソート言語の式です。s と c の2種類の項を持ち、P^ のように命題を動く変数もある、という意味です（ふつうは一階の部分だけを使います。証明器に渡すときの翻訳は 3.book）。
subsection 自分の Book では
txt ヘッダに <code>import /common/word_logic</code> と書くと、⊤ ⊥ ¬ and or ⇒ ⇔ ∀ ∃ = =_ and_ ⟹ ⟺ と、下の abbr（col・∀ など）が紹介済みになります。∈ と ∈_ は <code>word ∈</code>・<code>word ∈_</code> と自分で紹介します（\cls も同じ。.formel は word を紹介しません）。
subsection 読まれ方を CLI で確かめる
txt 式がどう読まれたかは、証明器に投げずに確かめられます。新しい書き方や、括弧を省いた式で迷ったときに使います。
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 0_tutorial_AI/2 '&#96;∀ x (x ∈ A ⇒ x ∈ B)&#96;'</div>
txt 結果は <code>[∀ x [⇒ [∈ x A] [∈ x B]]]</code> です。これは前置記法で、[ ] の先頭の word が外側、残りがその引数です（③ は「∀ x の中に ⇒ があり、⇒ の左右が ∈」と読まれた）。式はいくつでも並べて渡せます。本の名前（ここでは 0_tutorial_AI/2）は、その本が紹介した word を使って読むためのものです。
txt 以下の節でも、読み方の例にはこの結果を添えます。

section word
subsection 紹介とgram
txt ほとんどの word は DB に登録されていて、Book で紹介してから使います（例外は次の節の変数・定数など .formel に登録された word）。ソースで <code>word ∈</code> と書いた行が紹介です（上の節の4行）。表示ではその word の gram が付きます。
txt gram は「何を受け取って何を作るか」です。(〇,△) は「〇 を受け取って △ を作る」と読みます。
txt 　∈ … (ss,p)：s-Form 2つから p-Form を作る（① の x と X）
txt 　∈_ … (sc,p)：s-Form と c-Form から p-Form を作る（② の x と X_）
txt 　and or ⇒ ⇔ … (pp,p)：p-Form 2つから p-Form を作る
txt 　∀ … (vp,p)：変数と p-Form から p-Form を作る（③ の x と x ∈ A ⇒ x ∈ B）
txt gram の 〇 の文字数を arity と言います（∈ は 2）。gram が同じ word は1行でまとめて紹介できます。
txt word は tex（表示の形）も持ちます。∈ と ∈_ のように tex が同じ別の word があるので、表示の記号をクリックして確かめてください。自分で word を作るときは gram と tex を用意します。

section 変数と定数
txt 変数と定数は DB ではなく .formel に登録されている word です（紹介は要りません）。綴りで種類が決まります。
txt 　[lDP] … 英字1文字＋数字0個以上＋ ' 0個以上（<code>[A-Za-z][0-9]*'*</code>）。例 x、X1、A'
txt <table border="1"><tr><th>種類</th><th>gram</th><th>変数の綴り</th><th>定数の綴り</th><th>例（ソース）</th></tr><tr><td>集合</td><td>(,s)</td><td>[lDP]（v-Form）</td><td>|[lDP]</td><td><code>x</code> <code>|a</code></td></tr><tr><td>クラス</td><td>(,c)</td><td>[lDP]_（v_-Form）</td><td>|[lDP]_</td><td><code>X_</code> <code>|A_</code></td></tr><tr><td>命題</td><td>(,p)</td><td>[lDP]^（v^-Form）</td><td>|[lDP]^</td><td><code>P^</code> <code>|P^</code></td></tr></table>
txt 定数は変数の先頭に | を付けたものです。`|x ∈ X` も `x ∈_ |X_` もp-Formです。定数は量化できません：ソース <code>∀ |x P^</code> はFormでないです。
txt 引数をとる変数・定数（?f など）もあります。これは読み方の後の「高階の記号」の節で扱います。

section 読み方
subsection 区切りと括弧
txt word は半角スペースで区切ります。ただし ( ) の前後だけはスペースを省けます。例 <code>x ∈ (X)</code>
subsection 結合の強さ
txt 括弧が無いときは、word の結合の強さで読みます。強い順に
txt 　¬ ＞ ∀ ∃ ＞ ⇒ ⇔ ＞ and or ＞ ⟹ ⟺ ＞ and_
txt （and_ ⟹ ⟺ は結合の強さだけが違う and ⇒ ⇔ で、最後の節で紹介します）
txt （= や ∈、2項の述語変数を使った `x ??p^ y` はこれらより強く、互いに同じ強さ）。例：
txt 　`x = y ⇒ y = x` は `(x = y) ⇒ (y = x)`
txt <div style="border-left:4px solid #c00;background:#fff3f3;padding:6px 10px">注意：⇒ は and より強く結びつきます（ふつうの数学の書き方と逆）。 ソース <code>P^ and Q^ ⇒ R^</code> は <code>P^ and (Q^ ⇒ R^)</code> と読まれます（CLI の結果 <code>[and P^ [⇒ Q^ R^]]</code>）。 「P かつ Q ならば R」は、and より弱い ⟹ を使って <code>P^ and Q^ ⟹ R^</code>（CLI の結果 <code>[⇒ [and P^ Q^] R^]</code>）と書くか、括弧を付けて <code>(P^ and Q^) ⇒ R^</code> と書きます。 結合の強さは各 word の preced（最後の節）で決まっていて、「ならば・同値」には and より強い ⇒ ⇔ と、弱い ⟹ ⟺ の2組があります。取り違えてもエラーにならず、別の式として読まれるだけなので、迷ったら括弧を付けるか CLI で確かめます。</div>
txt 同じ強さの word が並ぶと左から読みます：`P^ and Q^ and R^` は `(P^ and Q^) and R^`（CLI の結果 <code>[and [and P^ Q^] R^]</code>）。and と or も同じ強さなので、ソース <code>P^ and Q^ or R^</code> は <code>(P^ and Q^) or R^</code>（<code>[or [and P^ Q^] R^]</code>）です。and を or より強くする慣習はありません。混ぜるときは括弧を付けます。
txt ただし表記法が R の word は右から読みます。∀ は R（紹介の行の gram の右に付いています）：`∀ x ∀ y P^` は `∀ x (∀ y P^)`（<code>[∀ x [∀ y P^]]</code>）
txt ∀ ∃ は ⇒ ⇔ and or より強く結びつきます。ソース <code>∀ x x ∈ A ⇒ x ∈ B</code> は <code>(∀ x x ∈ A) ⇒ x ∈ B</code>（<code>[⇒ [∀ x [∈ x A]] [∈ x B]]</code>）と読まれ、後ろの x は自由変数になります。エラーにはならないので、∀ ∃ の範囲は③のように必ず括弧で囲みます。

section 高階の記号
txt ここまでの一階の書き方に、変数の種類を1段増やします。
subsection 命題の変数
txt v^-Form（P^ など）は高階言語の記号です（一階論理の教科書ではメタ記号の扱い）。v^-Form や下の ?f を含む Thm も prf で p;（prover+）に投げられます。投げる前に定数へ置き換えて一階のThmにします（3.book「高階変数の定数化」）。
subsection 引数をとる変数・定数
txt 引数をとる変数もあります（高階言語の記号）。? は s-Form を、?_ は c-Form を引数にとることを表し、? の個数が引数の個数です。
txt 　?[lDP] … gram (s,s)。例 ソース <code>?f (x)</code> は s-Form（f(x)）。<code>?f (x) ∈ X</code> の CLI の結果は <code>[∈ [?f x] X]</code>
txt 　| を付ければ定数です。例 |??_[lDP]^ は gram (sc,p)：s-Form と c-Form を受け取る命題の定数。ソース <code>|??_p^ (x , X_)</code> は p-Form（<code>[|??_p^ x X_]</code>）
subsection F 表記
txt 表記法が F の word w は w(x1 , … , xn) の形で使います。例 ソース <code>?f (x)</code>・<code>|??_p^ (x , X_)</code>。表記法（R や F）は gram と同じく word のデータで、紹介の行で gram の右に表示されます（Book の中で変えることはできません）。

newpage

section 高レベルの表現
subsection 穴
txt 数学は記号列を変形していくゲームです。「記号列の変形の規則」もまた表現されます。
txt 規則を使うときに Form が代入される場所を「Formの穴」と言い、次の綴りを使います。
txt 　Formの穴 … <code>$[lDP]</code>。例：「or の前後をひっくり返す」規則は <code>$P or $Q</code> → <code>$Q or $P</code>
txt 　v-Formの穴 … 全角の <code>[ｌDP]</code>（[Ａ-Ｚａ-ｚ][0-9]*'*）
txt 　v_-Formの穴 … <code>[ｌDP]_</code>
txt 　wordの列の穴 … <code>$_[lDP]</code>

subsection tex計算とFCL変換
txt Formel は入力された Form を2通りに処理します。tex 表記の計算と、FCL（Formel Core Language）への変換です。FCL は略記などを処理し終えた形で、証明器に渡す式は FCL から翻訳して作られます。CLI の結果（前置記法）は FCL です。
txt default.formel では \, \; \! !, { } _ ^ が <code>word tex_only</code> に登録されています。空白で区切られた1つの word として書いたときだけ、表示のためだけに使われ、FCL 変換では無視されます。例 ソース <code>x { ∈ } X</code>（CLI の結果は <code>x ∈ X</code> と同じ <code>[∈ x X]</code>）。X_ や P^ の末尾の _ ^ は綴りの一部で、これとは別です。
br
txt word+ として紹介される word は高度な表現のためのもので、FCL 変換では lower という規則で処理されます。
txt 最も簡単な例が alias word（FCL 変換では同じ word になる別の word）です。次は結合の強さだけが違う論理記号です。
word and_ ⟹ ⟺
lower and_
lower ⟹
lower ⟺
txt word には precedence（preced）というデータもあり、上の「結合の強さ」はこれで決まります（preced が大きいほど弱い）。例：
txt 　`P^ ⇒ Q^ ⟺ ¬ P^ or Q^` は `(P^ ⇒ Q^) ⇔ (¬ P^ or Q^)`（CLI の結果 <code>[⇔ [⇒ P^ Q^] [or [¬ P^] Q^]]</code>。⟺ は FCL では ⇔ になる）
!txt 正確にはFCL変換の結果は、機械に扱いやすい prefix形・入れ子配列 です。
!txt 現状ではwordのprecedを操作する機能はありません…

subsection 省略表現
txt 省略表現も使えます。FCL 変換では abbr という規則で処理されます。abbr も word と同じように紹介してから使います。紹介すると、規則が表示されます（`\n` は自然数が代入されるもの。`\n-1` なども使えます）。
abbr col
txt col は「並べたものすべてについて同じことを言う」省略です。ソース <code>[ x ; y col ∈ A ]</code> は <code>x ∈ A and y ∈ A</code> になります（表示では and が「,」になるので、ソースで読んでください）。CLI の結果は <code>[and [∈ x A] [∈ y A]]</code> です。
txt 量化子の省略表現もあります。
abbr ∀
abbr ∀+
txt ソース <code>[ ∀ x ∈ A . x ∈ B ]</code> は <code>∀ x (x ∈ A ⇒ x ∈ B)</code>（③と同じ）になります。CLI の結果は <code>[∀ x [⇒ [∈ x A] [∈ x B]]]</code> で、③ の結果と一致します。
txt 省略表現を使った式は、このように CLI で展開後の形を確かめられます。
txt col と ∀ などの abbr は <code>import /common/word_logic</code> で紹介済みなので、その Book を import すれば書かずに使えます。

0_tutorial_AI/zz2_old.book

`0_tutorial_AI/zz2_old.book`