1 Formel の基本

1.1 ヘッダ指定、wordとForm

Formel の設定は .formelファイル に書かれています。
ヘッダで指定しなければ default.formel が読み込まれます。このBookもそうです。

Formel で使われる記号をwordと言い、「wordの列」のうち文法をみたすものをFormと言います。
Formには s-Form, c-Form, p-Form があります。
「s-Formは集合」という表現をしてしまいがちですが、注意が必要です。形式を見る時には前者、意味を見る時には後者を使います。「c-Formはクラス」も同じ。
Formは 高階{s,c}ソート言語 になります（一階部分しか使わないことが多いでしょうが）。

1.2 wordの基本

通常、wordは DB に登録されているものを呼び出し、Bookで「紹介」してから使用します。ソースには word で始まる行を書きます。
word(ss,p) … \(\in\)
(ss,p) はgramです。wordはtexというデータも持ち、\(\in\) のtexは \in です。gramやtexは DB に保存されています。
gram (〇,△) の〇の文字数を arity と言うことがあります。\(\in\) のarityは2です。
★現在は自分でwordを作ることはできませんが、自分でwordを作るときはgramとtexも用意する必要が出てくるでしょう。

texが同じでも異なるwordがありますので、こまめにクリックをして確認して下さい。次のwordも DB にあります。
word(sc,p) … \(\in\)
Bookを「読む」ときには一々集合とクラスを区別しなくて良いようにしています。

gramが同じwordはまとめて紹介できます。例えば次の2項命題結合子があります。
word(pp,p) … \(,\)  \(\mathbin{\rm o\!r}\)  \(\Rightarrow\)  \(\Leftrightarrow\)
wordは表記法（詳しくは下の「いろいろな記法」）というデータも持っており、紹介時にgramの右に付くことがあります。次の R など。
word(vp,p)R … \(\forall\)

1.3 変数・定数

変数は特別なwordであり.formelに登録されます。default.formelには次が登録されています。
v-Form (gramは(,s)) … [lDP]
v_-Form (gramは(,c)) … [lDP]_
[lDP] は「英字1文字の後に数字と ' が0個以上」（x, X1' など）を表します。
\(x \in X\) , \(x \in X\) はp-Formですが \(x \in X\) はFormでないです。なお、わざとこのような例を作っています。
.formelで指定すれば \(\alpha\) や \(\mathcal{X}\) などがv-Formとして使えるようになります。

次のv^-Formは高階言語の記号です（一階論理の通常の教科書ではメタ記号という扱い）。
v^-Form (gramは(,p)) … [lDP]^
\(\forall x P\) はp-Formです。

定数も登録されています。変数の先頭に | を付けるだけです。
word(,s) … |[lDP]
word(,c) … |[lDP]_
word(,p) … |[lDP]^
\(\mathrm{x} \in X\) , \(x \in \mathrm{X}\) もp-Formです。 \(\forall \mathrm{x} P\) はFormでないです。

1.4 いろいろな記法

Formのソースにおいては半角スペースがwordの区切りになります。
ただし \((\) \()\) の前後だけは、半角スペースを省略できます。例　 \(x \in ( X )\)

arity2のwordは中置されるのが基本です。
実はarityが1以上のwordにはprecedというデータも付きます（大小関係が意味を持ち、precedが大きいほど結合力が弱い)。
それは通常の数学で用いられる表現が使えるように意図されています。例　 \(x = y \Rightarrow y = x\) ≈ \(( x = y ) \Rightarrow ( y = x )\)
結合力の等しいものは通常は左から読まれます。例　 \(P , Q , R\) ≈ \(( P , Q ) , R\)
2項命題結合子の結合力については次のページに説明があります。
\(\forall\) は2項命題結合子より強く結びつきます。 \(\forall x x \in A \Rightarrow x \in B\) ≈ \(( \forall x x \in A ) \Rightarrow x \in B\) で \(\forall x ( x \in A \Rightarrow x \in B )\) と異なるので注意しましょう。

表記法がRのwordは右結合で、例えば \(\forall x \forall y P\) ≈ \(\forall x ( \forall y P )\)
表記法がFのword \({\tt w}\) は \({\tt w}\)(\({\tt x}_1\) , … , \({\tt x}_n\)) の形で使用されます。
仮に自分のBookで \(\in\) の表記法を F としたら、常に \(\in ( x , X )\) のように書くことになります。

★現在は word のprecedや表記法は DB にあるものから変更できません。

1.5 tex計算とFCL変換

Formel はFormの入力に対し2方向の処理をします。tex表記の計算 と FCL(Formel Core Language)への変換 です。
FCLは機械内部で扱いやすい形の言語で、入れ子配列になっています。 \(\forall x \forall y P\) のFCL変換は [\(\forall\), \(x\), [\(\forall\), \(y\), \(P\)]] です。
なお自然言語でもときどき問題になります。I think that that that that that boy wrote is wrong. は？
\({\tt F}\) と \({\tt G}\) のFCL変換が等しいことを \({\tt F}\) ≈ \({\tt G}\) と書いていたわけです。

default.formelには \, \; \! !, _ ^ が word tex_only に登録されています。
tex表示のためだけに使われ、FCL変換では無視されます。例　 \(x \; \in X\) ≈ \(x \in X\)
なおこれは空白で区切られた1つのwordとして書かれたときだけです。X_ の _ は綴りの一部で、これとは別です。
{ } は見えない括弧です。FCL変換では ( ) と同じです。例　 \(P , { Q \mathbin{\rm o\!r} R }\) ≈ \(P , ( Q \mathbin{\rm o\!r} R )\)