やる事
私たちは、数学を「単なる記号列を変形していくゲーム」とみなします。それを機械に行わせるべく、ルールを決めます。
数学の現場(大学の数学科)で行われていることを、なるべくそのまま行えるように意図します。
ルールは完全・厳密でなくても機械化をするのに十分であればOKと考えます。
まずは数学を記述するための数学語を作ります。一階言語を拡張し、数学の土台である集合とクラスを平易に扱えるようにします。通常の一階言語ではTermとPropを扱いますが、数学語では(TermをSetとし)さらにClsを扱います。
数学語に加え、その操作を記述するためのメタ数学語も作ります。特に、Propの一階言語への翻訳を定めます。翻訳により、一階論理を使ったり、一階言語のATPに乗せたりすることが可能となります。
なお、ここの地の文は、数学語やメタ数学語について説明するメタメタ語です。
単語
単に「単語」と言ったら「数学語の単語」のこととします。
ほとんどの単語は(単独で)tex表記を持ちます。通常は、私たちが目にするのはtex表記ですが、web上でそれをクリックすると単語本体が出てきます。例 \(=\)tex表記が同じでも異なる単語があります。tex表記が空の単語もあります。
単語はword、補助単語に分けられます。特別なwordにvarがあり、ローマ字およびそれらに自然数が付いたものになります。例 \(x_0\)
補助単語の例として \((\) \()\) とtex表記の無い { } があります。これらは塊を作るものです。
メタメタ語でも = や \(=\) を使います。記号はどうしても足らなくなります。変数としてタイプライター体\({\tt x}\)を使います。
wordのgram
wordはgramというデータを持ちます。gram は (gram0, gram1) という形になります。
・gram0 … s,c,p の列か vs か vp
・gram1 … s,c,p のどれか
また、arity : gram0の長さ、ただし gram0がvsかvp ⇒ arity : q とされます。
varは word(,s) です。var以外のword[arity : 0]はconstと呼ばれます。
例えば word(c,s) や word(p,s) は使用できません。基準はまだわかっていません…
word(ss,p) … \(\in\)
word(sc,p) … \(\in\)
wordの表記法
arityが0でないwordは表記法データも持ちます。それは次の3種類のどれかになります。
F ! 結合性(LかR)およびprecedの組
! は単独表記を持たないことを意味します。結合性は通常は L です。
word(vp,p)R … \(\forall\) \(\exists\) \(\exists!\)
precedは大小関係に意味があります。デフォルトでは次の値になります。
word[gram1 : sかc] … 300
word[gram0 : s,c以外を含まない、gram1 : p] … 700
word(vp,p) … 750
\(\neg\) … 730
\(\Rightarrow\) \(\Leftrightarrow\) … 770
\(,\) \(\mathbin{\rm o\!r}\) … 780
\(\Longrightarrow\) \(\Longleftrightarrow\) … 790