1 一階論理記号

このシステムでは(等号を持つ)一階論理は仮定され、次の記号が使用されます。
\(\mathbb{W}\)(,p) … \(\top\)  \({\perp}\)
\(\mathbb{W}\)(p,p) … \(\neg\)
\(\mathbb{W}\)(pp,p) … \(,\)  \(\mathbin{\rm o\!r}\)  \(\Rightarrow\)  \(\Leftrightarrow\)
\(\mathbb{W}\)(vp,p)R … \(\forall\)  \(\exists\)
\(\mathbb{W}\)(ss,p) … \(=\)
例えば \(\forall x P\) はp-Formです。

結合力が異なる次の記号もあります。
\(\mathbb{W}_{++}\)(pp,p) … \(\Longrightarrow\)  \(\Longleftrightarrow\)
lower … \(P \Longrightarrow Q\) ≃ \(P \Rightarrow Q\)
lower … \(P \Longleftrightarrow Q\) ≃ \(P \Leftrightarrow Q\)
form内の \(\mathbb{W}_{++}\) はlower規則によって、処理されます。なお \(P\) や \(Q\) はformの穴(formが代入されるもの)です。

二項述語の否定を作るword関数ともいうべきものがあります。
\(\mathbb{W}_{++}\)(\({\tt x}\)\({\tt y}\),p→\({\tt x}\)\({\tt y}\),p) … \({\tt /}\)
lower … \(A \stackrel{{\tt /}}{\mathbin{{\sf p}}} B\) ≃ \(\neg ( A \mathbin{{\sf p}} B )\)
引数のwordとの間にスペースは入れません。不等号は \(\neq\) で作れます。なお \(\mathbin{{\sf p}}\) は？

2 省略表現

通常の数学でよく使用される省略表現が用意されています。
省略表現は abbr規則 により処理されます。\(\cdots\) や \({\tt n}\) はしかるべく処理されます。
abbr … \(X_{1} , \cdots , X_{\tt n} \mathop{{\sf A}}\) ≈ \(X_{1} \mathop{{\sf A}} , \cdots , X_{\tt n} \mathop{{\sf A}}\)
例　 \(x , y \in A\) ≈ \(x \in A , y \in A\)

abbr … \(X_{1} \mathbin{{\sf p}} X_{2} \cdots \mathbin{{\sf p}} X_{\tt n}\) ≈ \(( X_{1} \mathbin{{\sf p}} X_{2} ) , \cdots , ( X_{\tt n\,{\text -}\,1} \mathbin{{\sf p}} X_{\tt n} )\)
次のような補題を用意しておくと便利なことがあります。
⇔\({\tt n}\) … \(( P_{1} \Leftrightarrow P_{2} \Leftrightarrow \cdots \Leftrightarrow P_{\tt n} ) \Longleftrightarrow ( P_{1} \Rightarrow P_{2} \Rightarrow \cdots \Rightarrow P_{\tt n} \Rightarrow P_{1} )\)
⇔3 \(\blacktriangleleft\) O

abbr … \(\forall x_{1} , \cdots , x_{\tt n} P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( P )\)
abbr … \(\exists x_{1} , \cdots , x_{\tt n} P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( P )\)
このような変換規則の表現内では \(x_{1}\) などはv-Formではなく v-Formの穴 です。