列

ものを並べたものを列と言います。
\({\tt x}\) を \({\tt n}\) 個並べた列を \({\tt x}^{\tt n}\) とします。
列 \({\tt F}\) に対して\({\tt F}\)の\(n+1\)番要素を \({\tt F}[n]\) とします。
\({\tt F}\)の長さが\(n+1\)のとき \({\tt F}={\tt F}[0]\,{\tt F}[1]\,\cdots\,{\tt F}[n]\) となります。

一般に言語は「単語の列のうち文法を満たすもの」で構成されます。
自然言語に於いては意味が考慮され「文」は入れ子の列になります。
例　I think that [that that that [that boy wrote] is wrong].
入れ子でない列→入れ子列 を parse、入れ子列→入れ子でない列 を flatten と言います。

列は誤解を生みうるものです。10 は「数字の十」とも「1,0の列」とも取れます。単語はsymbolの列です。

単語列の取り扱い

数学はFormを使うゲームです。それは「単語列のうちarityが正しく処理されているもの」です。
単語列は【】内にtex表記され、クリックするとinputと呼ばれるものが出てきます。
inputは単語毎にスペースを入れたものです。例　【\(x x\)】
ただし ( ) { } の前後ではスペースを略せます。例　【\(( x )\)】
tex表記でスペースを調整するためだけの単語に \, \; \! があります。例　【\(x \; x\)】

Formは(そうすることが必要な時には)入れ子列とみなされます。
Formはいくつかの形をとります。他の形に変えること「変形」と言います。他のFormへ「変換」することも後で出てきます。

prefix Form

Formの機械用の形は、wordの列で帰納的に作成されます。
・\({\tt w}\)がword[arity : \(n\)],  \({\tt F}_1,\cdots,{\tt F}_n\)がForm ⇒  \({\tt wF}_1\cdots{\tt F}_n\)がForm
・\({\tt w}\)がword[arity : q], \({\tt x}\)がvar, \({\tt F}\)がForm ⇒ \({\tt wxF}\)がForm

word[arity : 0] はそれだけでFormになります。例　【\(x\)】
入れ子列としては、例えば　【\(\neg \neg \top\)】\([1][0]\) = \(\neg\)

Formの中でもgramが正しく処理されているものには Set, Cls, Prop があります。それらの細かい規則として、例えば
・\({\tt w}\)がword(s,p)，\({\tt S}\)がSet ⇒  \({\tt wS}\)がProp
【\(\neg P\)】はPropにはなっていません…【\(P\)】はSetなので。
また正確には
・\({\tt w}\)がword[arity : q], \({\tt x}\)がvar, \({\tt F}\)がProp ⇒ \({\tt wxF}\)がForm

decent Form

wordと \((\) \(,\) \()\)の列で、読みやすい形を作ります。
word[arity : 2] はinfixにされます。例　【\(P , Q\)】
表記法がFのword [arity : \(n\)] \({\tt w}\) は【\({\tt w}({\tt x}_1,\cdots,{\tt x}_n)\)】の形で使用されます。
後置もできます？

prefixへの変形によって等しくなることを ≈ で表します。
infixでは\((\;)\)が必要になりますが、precedの差を利用して略せることがあります。
例　【\(x = y \Rightarrow y = x\)】≈【\(( x = y ) \Rightarrow ( y = x )\)】
例　【\(P \Rightarrow Q \Longleftrightarrow \neg P \mathbin{\rm o\!r} Q\)】≈【\(( P \Rightarrow Q ) \Longleftrightarrow ( ( \neg P ) \mathbin{\rm o\!r} Q )\)】

L結合性でprecedが等しいものは左から読まれます。例　【\(P , Q , R\)】≈【\(( P , Q ) , R\)】
\(\forall\) はR結合性で　【\(\forall x \forall y P\)】≈【\(\forall x ( \forall y P )\)】
なお、decentでは区別されますが、prefixでは次の同一視をして良いです。
　\(\Rightarrow\) ≈ \(\Longrightarrow\)
　\(\Leftrightarrow\) ≈ \(\Longleftrightarrow\)