1
ほとんどのwordにはそのwordの定義とみなせるp-Formが付きます。
何度も使用されるp-Formに名前を与える枠組みから作ります。
Prop
p-Formを指し示すPropというものを導入し、Thmを作るための記号とされます。
Propを紹介するときは、それが指し示すp-Formを右側に書きます。
word(,s)に \(\emptyset\) があります。次の定義で \({\perp}\) は \(x \neq x\) とされることが多いです。
\({\emptyset.}\)【\(\emptyset = \{ x \mid {\perp} \}\)】
\(\downarrow\) は次のように計算されます。正確には、左辺はPropでなくp-Formにするべき？
\({\emptyset.}\) ≃【\(\forall x \, ( x \in \emptyset \Longleftrightarrow {\perp} )\)】
p-FormをPropとして扱いたいときには ` ` を使用します。tex表記はありません。p-Formのtxtと`の間にスペースは入れません。例 \(【\top】\)
Formの扱いについて諸注意をしておきます。特にvarの扱いについて。
Formへの代入
Form \({\tt F}\) のvar \({\tt x}\) にs-Form \({\tt T}\) を代入してできるFormを \({\tt F}^{{\tt x}\,\mapsto\,{\tt T}}\) とします。\({\tt F}[{\tt T}/{\tt x}]\) と書かれる事も多いようです。
例 \(【x=y】\!^{x\,\mapsto\,y}=【y=y】\)
例 \(【\exists y\;x \neq y】^{x\,\mapsto\, y} =【\exists z\;x \neq z】^{x\,\mapsto\, y} =【\exists z\;y \neq z】\)
defもやめる？slashの一種にすればいいじゃん？
Formのいろいろな変換を与えます。一番大事なのはp-Formの一階言語への「翻訳」です。その他、Formを扱う上で便利な仕組みを導入します。
なお 超decent→decent→prefix という操作には「変形」という言葉を当てます。
\(\downarrow\)
翻訳には 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 X} = {\sf Y}\)】≃【\(\forall {\sf x} \, ( {\sf x} \in {\sf X} \Leftrightarrow {\sf x} \in {\sf Y} )\)】
defを適用するときには、形をそろえる必要があります。def0をprefixにし、適用される方もprefixにするのが良いでしょう(例えばdecentでも\((\,)\)の付け方に自由度があったりで難しくなります)。
Form \({\tt F}\)に対しdefを使える所全てに使った結果を \(\downarrow{\tt F}\) とします。一度defを使った後、新たに使える場所が出てくればそこにも使います(継時使用)。\(\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を代入します。
sc
集合はクラスとみなされます。tex表記のないword scが用意されます。word(s,c)! …【\( {\sf X}\)】
def …【\( {\sf X}\)】≃【\(\{ {\sf x} \mid {\sf x} \in {\sf X} \}\)】
次のような計算が多用されます。 【\(x \in X\)】≃【\(x \in X\)】
Form内で、(gramから推測して)c-Formがあるべき所にあるとき、scは省略可能とされます。必要に応じて \({\tt X}\) を sc \({\tt X}\) に変換します(sc補完)。
例 【\(x \in X\)】→【\(x \in X\)】
なお、超decentのままでのsc補完はしません。{all x sub_ \({\tt C}\) . \({\tt P}\)} の x は {sc x} にしません。
word関数
補助単語の中には word→word の働きをするものがあります。そのような単語は # と一文字になります。txtではword関数とwordの間にスペースを入れません。
tex表記は特殊になるので紹介時に記されます。紹介時にはgramの変換データも記されます。s,c,pを動く変数として\({\tt x}\),\({\tt y}\),\({\tt z}\)等が使われます。表記法データは変化させないものとします。
def … 【\({\sf A}\!\not{\!{\sf p}}\,{\sf B}\)】≃【\(\neg ( {\sf A} \mathop{{\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}\) をそれぞれ一つの記号として扱われます。
alias
一階言語にまで翻訳されたp-Formは、一階言語を処理できるソフトに送られます。phpではform_proverという関数がprover用の文字列に変換します。
その際に同一視される記号があり ≅ で表されます。phpではaliasという関数で処理されます。
aliasは証明におけるヒントを与えるためだけにあり、もとのwordとtex表記,gramなどが同一です。
集合の等号として = ≅ = を用意し【\(X = \{ x , y \}\)】のように使用します。
一般にtxtで_aをつけたwordは元のwordのaliasになります。