wordとForm
ほとんどのwordはライブラリで「紹介」されます。例えばword(ss,p) … \(\in\)
この (ss,p) はgramと呼ばれます。gramに現れる型には v,s,c,p があります。\(\dagger\)
Formにはs-Form, c-Form, p-Formがあり、特別なs-Formにv-Formがあります。
\(x\) , \(X\) はv-Formで、 \(x \in X\) はp-Formです。
wordの結合力の差は自然に利用されます。例 \(x = y \Rightarrow y = x\) ≈ \(( x = y ) \Rightarrow ( y = x )\)
結合力の等しいものは通常は左から読まれます。例 \(\mathrm{P} , \mathrm{Q} , \mathrm{R}\) ≈ \(( \mathrm{P} , \mathrm{Q} ) , \mathrm{R}\)
wordは紹介時に表記法 R か F が付くことがあります。例えば
word(vp,p)R … \(\forall\) \(\exists\)
このRは右から読むことを表し \(\forall x \forall y \mathrm{P}\) ≈ \(\forall x ( \forall y \mathrm{P} )\)
表記法がFのword \({\tt w}\) は \({\tt w}\)(\({\tt x}_1\), …, \({\tt x_n}\)) の形で使用されます。
特殊なword
Russelクラス \(\{ x \mid x \notin x \}\) がc-Formになることも見ていきましょう。{ } で挟まれたwordは「wordからwordを作る関数」のように働きます。
word(\({\tt x}\)\({\tt y}\),p→\({\tt x}\)\({\tt y}\),p) … \({\tt /}\)
これで \(\notin\) はword(ss,p)になります。
次のwordは(単独では)tex表記を持ちません。
word(vp,c) … cls
なお {/} や {cls で { の後に半角スペースを入れてはいけません。
メタ自然数も利用されます。1以上の自然数 \({\tt n}\) に対して
word(s\(^{\tt n}\),s) … set\({\tt n}\)
ただし s\(^{\tt n}\) は s を\({\tt n}\)個並べたものです。
Formのtxtでは\({\tt n}\)は略せます。s-Form \(\{ x , \{ y \} \}\) ではset2とset1が使用されています。
\, \; \! { } _ ^ はtex cmdになるだけのwordです。
\(\text{id}\) というword(s,s)があります。「\(X\)上の恒等写像」は \(\text{id} X\) ではなく \(\text{id} _ X\) とされることが多いです。
\(x_{1} x_{2} \cdots x_{99}\) なんてのも使用されます。
abbr
省略記法の処理するための abbr という規則があります。例えばabbr … \(\{ x \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mid x \mathop{{\sf A}} , ( P ) \}\)
例 \(\{ x \in X \mid x \neq 0 \}\) ≈ \(\{ x \mid x \in X , x \neq 0 \}\)
なお \(( P )\) の \(( )\) は塊を維持するために必要です。
次のものは正確には無限後のabbrを生成します。2以上の自然数 \({\tt n}\) に対し
abbr … \( X_{1} , \cdots , X_{\tt n} \mathop{{\sf A}}\) ≈ \(X_{1} \mathop{{\sf A}} , \cdots , X_{\tt n} \mathop{{\sf A}}\)
{ } は通常はFormとしての塊を作りますが、稀にその塊を崩すこともあります。
abbrを使用するときは ( ) を補いますが、補わないものは abbr* とされます。
pileというwordはtex表記が無く、次のabbr*はtex表記からは何が何だか。
abbr* … \( X\) ≈ \(X , X\)
例 \(x \in X \in \mathcal{X}\) ≈ \(x \in X , X \in \mathcal{X}\)
cvt
Mathelの一階言語への翻訳ではcvtと呼ばれるタイプの変換規則が使われます。例えばcvt … \(A \stackrel{{\tt /}}{\mathop{{\sf p}}} B\) ≃ \(\neg ( A \mathop{{\sf p}} B )\)
例 \(x \notin x\) ≃ \(\neg ( x \in x )\)
次が重要です。
cvt … \(T \in \{ x \mid P \}\) ≃ \(P\) の \(x\) に \(T\) を代入したもの
例 \(x \in \{ X \mid X \notin X \}\) ≃ \(x \notin x\)
以上の２つを合わせると
\(x \in \{ X \mid X \notin X \}\) ≃ \(\neg ( x \in x )\)
\(x \in \{ y \mid z \in \{ x \mid x \in y \} \}\) は内側から計算する方が楽です。
外側からだと、\(\int f(x)dx=\int f(y) dy\) みたいな処理が必要になりますね？
翻訳が必要なword \({\tt w}\) に対し \({\tt w}\). というPropは自然にcvtを作ります。例えば =_. は次を作ります。
cvt … \(X = Y\) ≃ \(\forall x \, ( x \in X \Leftrightarrow x \in Y )\)
defaltの翻訳では \({\tt w}\). が使用されます。
\({\tt w}\). の代わりに別定義 \({\tt w}\).. を使って翻訳する、というときには {\({\tt w}\)..} をPropの後につけます。
Russelのパラドクス
クラスが集合になるのか？という問いは自然に生まれます。\(\dot\exists\) というword(c,p)の定義はExi. … \(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)
\({\tt X}\) ◀ O となる \({\tt X}\) は tautology と言われることがありますが、Russelのパラドクスもです！？
\(\neg \dot\exists \{ x \mid x \notin x \}\) \(\blacktriangleleft\) O
翻訳には4段階必要です。そのような計算も機械の得意分野です。
≃ \(\neg \exists X ( \forall x ( x \in X \Leftrightarrow x \notin x ) )\)
私たちは会員を募集しています。
会員は◀をクリックするProver9からのoracleを見れます。
ルールの詳細などの私たちの発明の核心的な部分は非公開です。ぜひ会員になって共に議論しましょう！
代表：須田智彦[t@mshk1201.com]まで。