1 クラスの量化

\(\mathbb{W}\)(v_p,p)R … \(\forall\)  \(\exists\)
例えば \(\forall X P\) はp-Formになります。
これは「単ソート翻訳」はできません。単ソート翻訳では、ものは1種類しかなく、クラスは cvt規則 で溶けてしまいます。

「多ソート翻訳」という翻訳があります。
「s,cをソートする翻訳」では、s(集合) と c(クラス) を別のソートとして持ちます。クラスは溶けずに「もの」のまま残るので、 \(\forall X P\) はその c を走る量化になります。

-| が単ソート翻訳、--| が多ソート翻訳での導出を表します。表示はどちらも ◀ です。
prfのチェックにおいて、多ソート翻訳のthmはVampireに投げられことが多く、v--| と記載されます。
その際の「仮定」には \(\mathbb{W}_+.\) が追加されます。
\(\mathbb{W}_+.\) は「〇. (〇はその行に出てくる\(\mathbb{W}_+\)) という形のpropすべての列」です。この本の\(\mathbb{W}_+\)は ∈_ =_ \cls の3つなので、実際に添えられるのは =_. だけです。
\(\mathbb{W}_+\) の語は、単ソート翻訳では cvt規則 が定義を使い切ってしまいますが、多ソート翻訳では記号として残ります。だから定義が要ります。
\(\mathbb{W}_+.\) は \(\mathbb{W}.\) と違って ◀ の右には書きません。書きませんが、仮定に入ります。
\(\in\) \(\mathsf{cls}\) \(\mathsf{fn}\) も \(\mathbb{W}_+\) ですが、定義propを持たない(意味を運ぶのは翻訳そのものです)ので \(\mathbb{W}_+.\) には関与しません。
なお、添えた定義の中に出てくる\(\mathbb{W}_+\)の語の定義は、添えられません。word family(\n を含むword)があると定義が無限個になるからです。その語は解釈されない記号のまま残ります。
単ソート翻訳で示したことを多ソート翻訳の行で使うときは、関係をまたぐので「持ち上げ」が要ります。持ち上げてよいかは機械が確かめます。

2 NBG のクラス存在公理

NBG では下の B1〜B5 は公理として置かれます。ここでは内包記法 \(\{ x \mid P \}\) の定義から定理として出ます。
各行の左辺に現れる内包項が、NBG が「存在する」と要請するクラスそのものです。
NBG-B2 … \(\exists X \forall x \, ( x \in X \Longleftrightarrow x \in A , x \in B )\) \(\blacktriangleleft\) O
B2（交わり）
\(\forall x \, ( x \in \{ y \mid y \in A , y \in B \} \Leftrightarrow ( x \in A , x \in B ) )\) \(\blacktriangleleft\) O
B3（補クラス）
\(\forall x \, ( x \in \{ y \mid y \notin A \} \Leftrightarrow x \notin A )\) \(\blacktriangleleft\) O
\(\mathbb{W}\)(ss,s)F … \(\mathsf{pr}\)
abbr … \(\langle X , Y \rangle\) ≈ \(\mathsf{pr} ( X , Y )\)
B4（定義域）
\(\forall x \, ( x \in \{ y \mid \exists z \, ( \langle y , z \rangle \in A ) \} \Leftrightarrow \exists z \, ( \langle x , z \rangle \in A ) )\) \(\blacktriangleleft\) O
B1（所属関係のクラス）
\(\forall x \, \forall y \, ( \langle x , y \rangle \in \{ w \mid \exists u \, \exists v \, ( w = \langle u , v \rangle , u \in v ) \} \Leftrightarrow \exists u \, \exists v \, ( \langle x , y \rangle = \langle u , v \rangle , u \in v ) )\) \(\blacktriangleleft\) O