$Form
varを含まず$単語を含んだFormみたいな奴を $Form を言います。$列のうちarityが正しく処理されているものです。
$Formを作るときには $var, $Var は arity : 0 で $.var は arity : 1, $..Var は arity : 2 とされます。
$.var, $..varについては\({\sf p},{\sf q},{\sf r}\)で始まるものはpreced : 700, それ以外はpreced : 300とされます。
$Formも入れ子列とされます。超decentな$Formも使用されます。
$Formに対してもfvarは定義されます。
・\({\rm fvar}({\tt w})=\{\tt w\}\) if \({\tt w}\)が$var
\({\tt W}\)が$Varのときは、\({\rm fvar}({\tt W})\)はこれ以上計算されません。
def
一階言語への翻訳をするために def というデータが使用されます。最初の例はdef … 【\({\sf T} \in \{ {\sf x} \mid {\sf P} \} \)】≃\(【{\sf P}】\!^{{\sf x}\,\mapsto\,{\sf T}}\)
上の1個を除いて、defは次の形になります。
def0 ≃ def1 ただし、def0,def1は$Form、fvar(def0) = fvar(def1)
一階言語ではないwordについては、その定義と思えるdefが与えられます。例えば \(=\) の定義は
def …【\({\sf C} = {\sf D}\)】≃【\(\forall {\sf x} \, ( {\sf x} \in {\sf C} \Leftrightarrow {\sf x} \in {\sf D} )\)】
defの適用
defはFormの変換規則と捉えられます。
それを適用するときには、形をそろえる必要があります。def0をprefixにし、適用される方もprefixにするのが良いでしょう(例えばdecentでも\((\,)\)の付け方に自由度があったりで難しくなります)。
\(\downarrow\) による結果が等しくなることも ≃ で表します。
【\(x \in \{ y \mid z \in \{ x \mid x = y \} \} \)】のように入れ子になっているときは内側から計算しましょう。
≃【\(x\in\{y \mid z=y\}\)】≃【\(z=x\)】
ただし外側から計算しても同じ結果になります。
≃【\(x\in\{y \mid z \in \{u \mid u=y\}\}\)】≃【\(z\in\{u \mid u=x\}\)】≃【\(z=x\)】
defを使用する際、def1のみに現れる$var(例えば \(=\) の定義の\({\sf x}\))には適当なvarを代入します。
Propについては \(\downarrow\) の結果は一階言語になります。
word関数
補助単語の中には word→word の働きをするものがあります。
そのような単語は # と一文字になります。inputではword関数とwordの間にスペースを入れません。
tex表記は特殊になるので紹介時に記されます。
紹介時にはgramの変換データも記されます。s,c,pを動く変数として\({\tt x}\),\({\tt y}\),\({\tt z}\)等が使われます。
表記法データは変化させないものとします。
word関数 … \(/\)を重ね打ちする #/ : (\({\tt xy}\),p)→(\({\tt xy}\),p)
def …【\({\sf A} \cancel{{\sf p}} {\sf B}\)】≃【\(\neg ( {\sf A} {\sf p} {\sf B} )\)】
例 【\(x \notin X\)】≃【\(\neg ( x \in X )\)】 【\(P \not\Rightarrow Q\)】≃【\(\neg ( P \Rightarrow Q )\)】
同じword関数を重ねて使う事(例 #/#/$..p)はtex表記が困難になるのでやめましょう。
Form内では、word関数 \({\tt f}\) とword \({\tt w}\) に対し \({\tt fw}\) で一つのwordとして扱われます。
defを適用するときには \({\tt f}\) と \({\tt w}\) をそれぞれ一つの単語として扱われます。