4 2ソートのThm

s-Form（集合）を「もの」、c-Form（クラス）を「箱」と見なし、「入っている」を表す word ∈_ を使います。表示では ∈_ は ∈ と、X_ は X と同じ形になるので、ソースで区別します。最初の例はクラス変数 X_ を含むので、表のとおり ◀ … v; で投げます（次の Hall の例もクラス定数 |A_ を含むので ◀ … v; です。min.thmel の -| は |cvt+ を掛けないので、クラスの語を含む段は -| … p; では通りません）。
word(sc,p) … \(\in\)
1つの箱 \(X\) は、ものを「\(X\) に入っている／いない」の2通りに分けます。入っているかどうか（真か偽か）だけでは、3つのもの x1, x2, x3 を互いに区別できません（2通りに3つを入れる鳩の巣原理）。
ソースの読み方：\\{ And A \\ B \\ C \\} は A and B and C を縦に並べて書く形、{/}⇔ は ⇔ の否定（「真偽が違う」）。
\(\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

次は Hall の定理（各箱から異なるものを選べる条件）の小さな具体例です。3つの箱に何が入っているかを具体的に与え（prop Hall）、そこから「各箱から異なるものを1つずつ選べる」ことを示します。|p などは定数です（変数だと「すべての」の意味になる）。
ソースの読み方：[ |p ; |q col ∈_ |A_ ] は |p ∈_ |A_ and |q ∈_ |A_（col は 2.book）、[ ∃ x ∈_ |A_ . P ] は ∃ x (x ∈_ |A_ and P)、{/}= は ≠。
Hall … \(\begin{cases} \mathrm{p} , \mathrm{q} \in \mathrm{A} \\ \mathrm{q} , \mathrm{r} \in \mathrm{B} \\ \mathrm{r} , \mathrm{p} \in \mathrm{C} \end{cases}\)
neq … \(\mathrm{p} \neq \mathrm{q} , \mathrm{q} \neq \mathrm{r} , \mathrm{r} \neq \mathrm{p}\)
\(\exists x \in \mathrm{A} . \exists y \in \mathrm{B} . \exists z \in \mathrm{C} . ( x \neq y , y \neq z , z \neq x )\) \(\blacktriangleleft\) Hall ，neq
Vampire は一瞬で割り当て（\(\mathrm{A}\)→\(\mathrm{p}\), \(\mathrm{B}\)→\(\mathrm{q}\), \(\mathrm{C}\)→\(\mathrm{r}\) など）を見つけます。

5 仕組み

5.1 prop と Thm

Thmel の定数として Formel の p-Form を登録したものをpropと言います。prop は DB に登録されたものを使うほか、prop名 <- `…` で作れます。
prop \({\tt P}\) と prop の列 \(\Gamma\) に対し \({\tt P}\) ◀ \(\Gamma\) の形のものをThmと言います。Thm の eval は各 prop を Formel に投げ FCL に変換したものです。
prop \({\tt P}\) が指す p-Form を式の中で使うときは @\({\tt P}\) と書きます。使えるのはThmの中と、Book で作る prop の本文です。ふつうは prop を sos に名前で置けば足ります。

5.2 Thmの変換 |0

backend ごとに扱える論理が違うので、Thm をその backend が扱える言語の Thm に変換してから投げます。変換を |f と書き、\(\mathcal{T}\)|f の eval は \(\mathcal{T}\) を eval してから |f を計算したものです。
Form は高階{s,c}ソート言語です。それとは別に「高階言語」（ソートの無い言語）があるとみなし、変換 |0 を作ります。
　\(\mathcal{T}\) が部分Formとして c-Form を含まなければ \(\mathcal{T}\)|0 = (\(\mathcal{T}\) を高階言語に自然に翻訳したもの)、含めば \(\mathcal{T}\)|0 はエラー
高階言語の Thm は ◀ ではなく ◁ で書きます（説明でしか使わない記号）。違う言語であることを示すため、式を緑にします。例　(\(\top\) ◀ O)|0 \(=\) \(\top\) ◁ O
min.thmel は goal -| sos を (goal ◀ sos)|0 と規定しています（cvt を掛けない）。c-Form を含む Thm は |0 がエラーなので、そういう段は査読の失敗になります。default.thmel は |0 の前に |cvt+（5.book）を掛けます。

5.3 論理と定理

Thm は形式的なものです。Thm に意味を与えるものを論理と言います。Thm \(\mathcal{T}\) を論理 \(\mathbb{L}\) で扱え、◀ を「推論できる」と読めるとき、\(\mathcal{T}\) holds in \(\mathbb{L}\) と書きます。
Mathelia では 高階{s,c}ソート論理 \(\mathbb{L}_{\rm Hsc}\) と 高階論理 \(\mathbb{L}_{\rm H}\) は既知とし、通常はその部分論理 一階{s,c}ソート論理 \(\mathbb{L}_{\rm 1sc}\) と 一階論理 \(\mathbb{L}_1\) を使います。\(\mathbb{L}_1\) の公理には等号公理と領域の非空性 \(\exists x \, ( x = x )\) が含まれます。
backend が「\(\mathbb{L}\) を判定する」とは「Thm \(\mathcal{T}\) を受け取ったとき、\(\mathcal{T}\) holds in \(\mathbb{L}\) を確かめると 〇 を返す」ことです。
Thmel は論理 \(\mathbb{L}_*\) を規定し、\(\mathcal{T}\) holds in \(\mathbb{L}_*\) の形のものを「定理」と呼びます。min.thmel の規定：
　\(\mathcal{T}\) holds in \(\mathbb{L}_*\) \(\Longleftrightarrow\) \(\mathcal{T}\) holds in \(\mathbb{L}_\mathrm{Hsc}\)
　\(\mathcal{T}\)|0 がエラーでなければ　\(\mathcal{T}\) holds in \(\mathbb{L}_*\) \(\Longleftrightarrow\) \(\mathcal{T}\)|0 holds in \(\mathbb{L}_\mathrm{H}\)
Thm の後の prf は \(\mathcal{T}\) holds in \(\mathbb{L}_*\) の証明とみなせるもので、Thm 査読で査読器に見てもらいます。