$単語
メタ数学語の単語の中で良く使用されるものに $単語 があります。$単語は $ で始まります。$var, $Var はサンセリフ体の小文字, 大文字およびそれらに自然数が付いたものになります。例 \({\sf a}\), \({\sf A}\)
他に $.var, $..var もありサンセリフ体の小文字になります(tex表記は $var と同じ)。例 \({\sf a}\), \({\sf a}\)
メタ数学語は「単語列に関する何らかの規則」も記述しますが、$単語はそこでの変数になります。
規則を使用する際には、$varには１つのvar、$Varには単語列、$.var には word[arity : 1], $..var には word[arity : 2] が代入されます。その他の代入条件が課されることもあります。
【\(\neg\neg\neg Q\)】に【\(\neg\neg{\sf P}\)】を合わせる代入 \(({\sf P}\mapsto \neg Q)\) が計算され【\(\neg Q\)】という結果になります。
Form
一定の変形によってdecent(さらにはprefix)のFormになるものもFormと呼びます。
decentへの変形で変化するようなFormは超decentと呼ばれ、数学語の表現力を高めてくれます。
超decent Formのinputでは、塊を作るために { } が使われます。
超decent Formは ①decent Formの省略形 のことがあります。この場合、decentへの変形にはabbrというデータが使われます。
②特殊なtex表記法を持つ ことがあります。各単語のtex表記を並べるのではなく、一定の形の列に対してtex表記が与えられます。
abbr
「var以外の単語と$単語」の列を $列 と言います。abbrは次の形になります。
abbr0 ≈ abbr1 ただし、abbr0,abbr1は$列
これは「abbr0をabbr1に変形する」という規則だと捉えられます。
abbr …【\( \forall {\sf x} {\sf A} . {\sf P} \)】≈【\(\forall {\sf x} \, ( {\sf x} {\sf A} \Rightarrow ( {\sf P} ) )\)】
例えば次のPropは①のパターンです。
【\( \forall x \in R . \forall x \in S . x \in T \)】≈【\(\forall x \, ( x \in R \Rightarrow \forall x \, ( x \in S \Rightarrow x \in T ) )\)】
{ } による塊が崩れないよう、内側から計算する方が良いでしょう。
abbr1で \(({\sf P})\) の \((\;)\) は必要です。\({\sf P}\)に代入されるPropに \(\Rightarrow\) よりprecedの大きい単語が含まれている場合にも働くように。
abbr … 【\(\exists {\sf x}_{1} , \cdots , {\sf x}_n \, {\sf P}\)】≈【\(\exists {\sf x}_{1} \cdots \exists {\sf x}_n ( {\sf P} )\)】
特殊表記を持つForm
単独表記を持たないwordは、紹介時に$列のtex表記例が与えられます。例えば、クラスを生成する cls があります。word(vp,c)! …【\(\{ {\sf x} \mid {\sf P} \} \)】
【\(\{ x \mid x \in \{ y \mid x \in y \} \} \)】はClsで、②のパターンです。
decentに変形するときは、単独表記を持たないwordは表記法Fとみなして自然に行います。tex表記はできなくなります。
例 【\(\{ x \mid P \} \)】≈ cls(x , P)
特殊表記を持つFormのinputで引数を区切るには ; や | が使われます。
①②両方のパターンの例を挙げます。abbr0の表記で \({\sf X}\) が消える珍しい例です。abbr …【\(\{ {\sf T} \mid {\sf P} \}\)】≈【\(\{ {\sf x} \mid \exists {\sf X} \, ( ( {\sf P} ) , {\sf x} = {\sf T} ) \} \)】
例【\(\{ x \cup y \mid x \in X , y \in Y \}\)】≈【\(\{ z_{1} \mid \exists x , y \, ( x \in X , y \in Y ) , z_{1} = x \cup y \} \)】
abbrを使用するとき、abbr0に含まれずabbr1に含まれる$var(例えば上の \({\sf x}\))には適当なvarを代入します。私たちはFormの同値類を見ていることに注意しましょう。