3 定義、定義による展開

3.1 定義を集めた列 \(\mathbb{W.}\)

集合論の最初に出てくる記号に次があります。
word(ss,p) … \(\in\)  \(\subset\)
\(\subset\) は次の定義を持ちます。一般に 〇. は 〇の定義 という位置づけになります。
⊂. … \(X \subset Y \Longleftrightarrow \forall x \in X . x \in Y\)
\(=\) にも定義があるという扱いが便利です。\(\Longleftarrow\) は外延性公理と呼ばれることが多いですが。
=. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)

Book内の自動変数が使用されます。
\(\mathbb{W}.\) は「〇. (〇 はgramにcを含まない) という形のpropすべての列」です。この段階では ⊂. =. です。
\({\tt P}\) ◀ \(\mathbb{W}.\) は「定義から\({\tt P}\)が示される」と読まれます。必要な定義を一々書くのはめんどくさいので、この形が好まれます。
=.. … \(X = Y \Longleftrightarrow X \subset Y \subset X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

一般には、Prover9に投げるときにはsosには必要なものだけを書く方がよいです。
ソース145行目で prf =.. -| W. p; の W. の代わりに ⊂. , =. を sos に置いても示せます（length:37）。ただし thm の主張は ◀ W. なので、最後に =.. -| W. h; でつなぎます。
\(\mathbb{W}.\) が無限列になったとき(例えば \({\tt n}\) を含むwordの定義が与えられたとき)は -| W. p; とはできません。

3.2 slash計算

/ は Thmel の2項演算で、\({\tt A}\) / \({\tt P}\) は「\({\tt A}\) を \({\tt P}\) で展開したもの」です。例えば
=.. / =. … \(\forall x \, ( x \in X \Leftrightarrow x \in Y ) \Longleftrightarrow X \subset Y \subset X\)

列 \(\mathcal{P}\) に対しても、自然に \({\tt A}\) / \(\mathcal{P}\) は定義されます。
上のThmのprfを新しいものにしてみます。
=.. \(\blacktriangleleft\) \(\mathbb{W}.\)
ソース159行目にあるprfの1段目 =.. / W. -| O p; に注目して下さい。Thmel で展開計算を済ませたことにより、Prover9へsos Oで渡せます。goalはかなり長い式になりますが、length:28に減ります。
2段目の =.. -| W. h; は hyperion の段で、1段目で示した事から、slash の除去（\({\tt A}\) / \(\mathcal{P}\) ◀ \(\Gamma\) から \({\tt A}\) ◀ \(\mathcal{P}, \Gamma\)）をします。

// W. は / W. / W. になります。
1回の / W. では、各部分式をその頭の語の定義で1段だけ開きます。開いてできた式は次の / で開きます。
W.!〇.（空白を入れずに書く）は W. から 〇. を除いた列です。
同じThmを -| W. p;（定義を sos に置く）でも / W. -| O p;（先に展開する）でも示せることが多いです。定義が増えて sos が大きくなると、先に展開する方が有利になります。