1 例から

この Book は Formel（式の書き方）の説明です。ヘッダに formel 行が無いので default.formel を読み込んでいます。
まず、この頁で使う記号を紹介します（紹介のしかたは次の節）。
word(ss,p) … \(\in\)
word(sc,p) … \(\in\)
word(pp,p) … \(,\)  \(\mathbin{\rm o\!r}\)  \(\Rightarrow\)  \(\Leftrightarrow\)
word(vp,p)R … \(\forall\)
次の4つは、どれも正しい式です。表示では _ や | が見えなくなるので、ソースの綴りを並べます。「…」は読み方の目安です（式の意味は、後で定義や公理を置いて初めて決まります）。
　① \(x \in X\) 　　ソース x ∈ X 　… 集合 x が集合 X に属する
　② \(x \in X\) 　　ソース x ∈_ X_ 　… 集合 x がクラス X_ に属する（∈ とは別の記号 ∈_）
　③ \(\forall x ( x \in A \Rightarrow x \in B )\) 　ソース ∀ x (x ∈ A ⇒ x ∈ B) 　… A の元はすべて B の元
　④ \(P , Q\) 　　ソース P^ and Q^ 　… 命題 P^ と命題 Q^ の両方
次は式になりません。
　⑤ ソース x_ ∈_ X_ 　… ∈_ の左には s-Form しか置けないが、x_ は c-Form

用語：Formel で使われる記号をword、wordの列のうち文法をみたすものをFormと言います（①〜④はForm、⑤はFormでない）。
Formには3種類あります。
　s-Form … 集合を表す項（x、X、?f (x) など）
　c-Form … クラスを表すもの（X_ など）
　p-Form … 命題を表すもの（①〜④ など）
「s-Form は集合」と言ってしまいがちですが、形式（書けるか・gram・翻訳できるか）を見るときは s-Form・c-Form・p-Form、意味（何を表すか・真偽）を見るときは集合（もの）・クラス・命題と言い分けます。gram に c を含まない word を集合の語、含む word をクラスの語と言います（∈ も集合の語）。定数の綴りの先頭の | を bar と言います。主張は Thm 全体、goal はその ◀ の左（1.book）です。
Formは高階{s,c}ソート言語の式です。s と c の2種類の項を持ち、P^ のように命題を動く変数もある、という意味です（ふつうは一階の部分だけを使います。証明器に渡すときの翻訳は 3.book）。

1.1 自分の Book では

ヘッダに import /common/word_logic と書くと、⊤ ⊥ ¬ and or ⇒ ⇔ ∀ ∃ ∀_ ∃_ = =_ and_ ⟹ ⟺ {/} と、下の abbr（col・∀ など）が紹介済みになります。∈ と ∈_ は word ∈・word ∈_ と自分で紹介します（\cls も同じ。.formel は word を紹介しません）。集合とクラスの基本の語（∈_ ∈ \cls cls ！ \fn など・=. ⊂. ⊂_. =_. などの定義）までまとめて紹介するなら import /common/word_basis（6.book）。

1.2 読まれ方を CLI で確かめる

式がどう読まれたかは、証明器に投げずに確かめられます。新しい書き方や、括弧を省いた式で迷ったときに使います。

結果は [∀ x [⇒ [∈ x A] [∈ x B]]] です。これは前置記法で、[ ] の先頭の word が外側、残りがその引数です（③ は「∀ x の中に ⇒ があり、⇒ の左右が ∈」と読まれた）。式はいくつでも並べて渡せます。本の名前（ここでは 0_tutorial_AI/2）は、その本が紹介した word を使って読むためのものです。
以下の節でも、読み方の例にはこの結果を添えます。

2 word

2.1 紹介とgram

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

3 変数と定数

変数と定数は DB ではなく .formel に登録されている word です（紹介は要りません）。綴りで種類が決まります。
　[lDP] … 英字1文字＋数字0個以上＋ ' 0個以上（[A-Za-z][0-9]*'*）。例 x、X1、A'

種類	gram	変数の綴り	定数の綴り	例（ソース）
s-Form	(,s)	[lDP]（v-Form）	|[lDP]	x |a
c-Form	(,c)	[lDP]_（v_-Form）	|[lDP]_	X_ |A_
p-Form	(,p)	[lDP]^（v^-Form）	|[lDP]^	P^ |P^

定数は変数の先頭に | を付けたものです。 \(\mathrm{x} \in X\) も \(x \in \mathrm{X}\) もp-Formです。定数は量化できません：ソース ∀ |x P^ はFormでないです。
引数をとる変数・定数（?f など）もあります。これは読み方の後の「高階の記号」の節で扱います。

4 読み方

4.1 区切りと括弧

word は半角スペースで区切ります。ただし ( ) の前後だけはスペースを省けます。例 x ∈ (X)

4.2 結合の強さ

括弧が無いときは、word の結合の強さで読みます。強い順に
　¬ ＞ ∀ ∃ ＞ ⇒ ⇔ ＞ and or ＞ ⟹ ⟺ ＞ and_
（and_ ⟹ ⟺ は結合の強さだけが違う and ⇒ ⇔ で、最後の節で紹介します）
（= や ∈、2項の述語変数を使った \(x \mathbin{p} y\) はこれらより強く、互いに同じ強さ）。例：
　 \(x = y \Rightarrow y = x\) は \(( x = y ) \Rightarrow ( y = x )\)

同じ強さの word が並ぶと左から読みます： \(P , Q , R\) は \(( P , Q ) , R\) （CLI の結果 [and [and P^ Q^] R^]）。and と or も同じ強さなので、ソース P^ and Q^ or R^ は (P^ and Q^) or R^（[or [and P^ Q^] R^]）です。and を or より強くする慣習はありません。混ぜるときは括弧を付けます。
ただし表記法が R の word は右から読みます。∀ は R（紹介の行の gram の右に付いています）： \(\forall x \forall y P\) は \(\forall x ( \forall y P )\) （[∀ x [∀ y P^]]）
∀ ∃ は ⇒ ⇔ and or より強く結びつきます。ソース ∀ x x ∈ A ⇒ x ∈ B は (∀ x x ∈ A) ⇒ x ∈ B（[⇒ [∀ x [∈ x A]] [∈ x B]]）と読まれ、後ろの x は自由変数になります。エラーにはならないので、∀ ∃ の範囲は③のように必ず括弧で囲みます。

5 高階の記号

ここまでの一階の書き方に、変数の種類を1段増やします。

5.1 命題の変数

v^-Form（P^ など）は高階言語の記号です（一階論理の教科書ではメタ記号の扱い）。v^-Form や下の ?f を含む Thm も prf で p;（prover+）に投げられます。投げる前に定数へ置き換えて一階のThmにします（3.book「高階変数の定数化」）。

5.2 引数をとる変数・定数

引数をとる変数もあります（高階言語の記号）。? は s-Form を、?_ は c-Form を引数にとることを表し、? の個数が引数の個数です。
　?[lDP] … gram (s,s)。例 ソース ?f (x) は s-Form（f(x)）。?f (x) ∈ X の CLI の結果は [∈ [?f x] X]
　作る Form は末尾の印で決まります：印なしは s-Form、_ は c-Form、^ は p-Form。例 ?_F_ (X_)（gram (c,c)）は c-Form、?_p^ (X_)（gram (c,p)）は p-Form。c-Form を受け取って s-Form を作る ?_f の綴りはありません。引数が s と c の両方なら ? を先に並べます（??_p^ (x , X_)）。
　| を付ければ定数です。例 |??_[lDP]^ は gram (sc,p)：s-Form と c-Form を受け取り p-Form を作る定数。ソース |??_p^ (x , X_) は p-Form（[|??_p^ x X_]）

5.3 F 表記

表記法が F の word w は w(x1 , … , xn) の形で使います。例 ソース ?f (x)・|??_p^ (x , X_)。表記法（R や F）は gram と同じく word のデータで、紹介の行で gram の右に表示されます（Book の中で変えることはできません）。