2 Mathelia論理
2.1 cvt+変換
|cvt+ という
Thmの変換を次のように作ります。
|cvt を施し、それでも残る(v_-Formでない)c-Formに対しgramが(s,p)の定数を一つ対応させます。例えば
\(\mathrm{X}\) に
\({\mathrm{X}}\) を。
そして
\(x \in \mathrm{X}\) を
\({\mathrm{X}} ( x )\) に置き換えます。（細かい規則はAI用tutorial）。
例えば
(
\(\mathrm{X} = \mathrm{X}\) ◀ O )
|cvt+ …
\(\forall x ( {\mathrm{X}} ( x ) \Leftrightarrow {\mathrm{X}} ( x ) )\) ◀ O
2.2 -|
Matheliaでは次のように規定しています。
\(\mathcal{T}\)
|cvt+|0 がエラーでなければ \(\mathcal{T}\) holds in \(\mathbb{L}_*\) \(\Longleftrightarrow\) \(\mathcal{T}\)
|cvt+|0 holds in \(\mathbb{L}_\mathrm{H}\)
次の略記法がよく使用されます。
\({\tt P}\) -| \(\Gamma\) … (\({\tt P}\) ◀ \(\Gamma\))
|cvt+|0クラスを利用した定理の例を挙げます。演算の中心について。「Book内定数」も利用してみます（ソース64行目の
let |C_ := `…`）
word(ss,s) …
\(+\) \(\mathrm{C}\) …
\(\{ x \mid \forall y \; x + y = y + x \}\) \(\forall u , v , w \; u + ( v + w ) = ( u + v ) + w \Longrightarrow \forall a , b \in \mathrm{C} . \, a + b \in \mathrm{C}\) \(\blacktriangleleft\) O2.3 elim変換
|cls-elim という
Thmの変換も作ります。
内包
\(\{ x \mid P \}\) の形のc-Formを、gramが(,c)の定数(例えば
\(\mathrm{X}\) )に置き替え、
\(x \in \mathrm{X} \Leftrightarrow P\) を sos に足します。
内包が自由な変数を含むときは、それを引数に取る記号に置き替えます（細かい規則はAI用tutorial）。
例えば
(
\(y \in \{ x \mid x = x \}\) ◀ O)
|cls-elim …
\(y \in \mathrm{X}\) ◀
\(x \in \mathrm{X} \Leftrightarrow x = x\) |fn-elim という
Thmの変換も作ります。
アロー関数を適用した
\(\lceil x \mapsto X \rfloor ( t )\) の形のFormを、gramが(s,s)の定数(例えば
\({\mathrm{F}}\) )を使った
\({\mathrm{F}} ( t )\) に置き替え、
\({\mathrm{F}} ( x ) = X\) を sos に足します。
アロー関数が自由な変数を含むときは、それも引数に取る記号に置き替えます（細かい規則はAI用tutorial）。
例えば
(
\(\lceil x \mapsto x + a \rfloor ( b ) = b + a\) ◀ O)
|fn-elim …
\(\mathbin{\mathrm{F}} ( a , b ) = b + a\) ◀
\(\mathbin{\mathrm{F}} ( a , x ) = x + a\) アロー関数を適用せずに受け取るword（例えば Rest）は、先にその定義で開いてから |fn-elim します（細かい規則はAI用tutorial）。
2.4 --|
Thmの簡単な演算に +sos があります。(\({\tt P}\) ◀ \(\Gamma\)) +sos \(\Delta\) は \({\tt P}\) ◀ \(\Gamma,\Delta\) です。
Matheliaには次の規定もあります。
\(\mathcal{T}\) holds in \(\mathbb{L}_*\) \(\Longleftrightarrow\) \(\mathcal{T}\)
|fn-elim|cls-elim +sos \(\mathbb{W}_\mathrm{c}.\) holds in \(\mathbb{L}_\mathrm{Hsc}\)
次の略記法がよく使用されます。
\({\tt P}\) --| \(\Gamma\) … (\({\tt P}\) ◀ \(\Gamma\))
|fn-elim|cls-elim +sos \(\mathbb{W}_\mathrm{c}.\)
上の定理のprf(ソース66行目)の -| は --| にしても通ります。
\(\forall u , v , w \; u + ( v + w ) = ( u + v ) + w \Longrightarrow \forall a , b \in \mathrm{C} . \, a + b \in \mathrm{C}\) \(\blacktriangleleft\) O\(\mathbb{L}_*\) の2つの定義が同値かは、一般には示されていません。Thm は書いた方の規定で査読します（同じ Thm が両方で通っても、同値の証明にはなりません）。
.thmel では、どの範囲のThmに対して同値であることを認めるかも記述されます（現在はまだ記述されていない）
2.5 -| がエラーになり、--| は ◀ と同じ定理の例
次のThmはソース97行目の --| を -| に替えると通りません。
|cvt+ で
\(x \in A\) が残るため。
\(x \in \mathrm{B}\) \(\blacktriangleleft\) \(x \in A\)このsosは「すべての x がすべてのクラス A_ に属する」という（強すぎる）主張です。
\(A\) に
\(\mathrm{B}\) を代入することを明示した証明（ソース101行目）も書けます。
\(x \in \mathrm{B}\) \(\blacktriangleleft\) \(x \in A\)s-Formを「もの(の種類)」、c-Formを「箱」と見なすと、∈_ は「入っている」を表すwordです。
1つの箱
\(X\) は、ものを「
\(X\)に入っている／いない」の2通りに分けます。1つの箱だけでは3点の区別はできません（鳩の巣原理）。
\(\neg \begin{cases} x_{1} \in X \not\Leftrightarrow x_{2} \in X \\ x_{2} \in X \not\Leftrightarrow x_{3} \in X \\ x_{3} \in X \not\Leftrightarrow x_{1} \in X \end{cases}\) \(\blacktriangleleft\) O実は
prover+ は相対化という操作をすることで \(\mathbb{L}_\mathrm{1sc}\) も判定できます。以上の2定理はprfの末尾の
v; を
p; にしても通ります。