book集

section この Book の読み方
txt この Book は、Mathelia で集合論の最初の部分（所属・包含・宇宙・空集合・べき集合・和と積・ZF の公理）を書いた例です。ヘッダは <code>import /common/word_basis</code>（集合論の基本の語を読み込む）です（thmel 行は書かないので default.thmel を読みます）。
txt 表示では ∈ と ∈_、= と =_、⊂ と ⊂_、X と X_ が同じ形になり、prf は表示されません。そこで各 Thm の直後に「ソース：」の行で thm と prf のソースを載せています（字下げした prf の続きの行は「　　」で示す）。
txt この Book の prf は、ほぼ次の型のどれかです。
txt <table border="1"><tr><th>prf の型（ソース）</th><th>何をしているか</th><th>主な例</th></tr><tr><td><code>goal -| O p;</code></td><td>-| の変換（<span style="color:brown">|cvt+</span>、5.book）が、クラスの語（𝕍・=_ など）の定義と内包を開いてから Prover9 へ</td><td>2.1・3.1・5.1</td></tr><tr><td><code>goal / W. -| O p; goal -| W. h;</code>（/ は1〜4本）</td><td>W.（集合の語の定義）で展開してから投げ、h; で「◀ W.」の形に戻す（4.book）。/ の本数は開く回数</td><td>2.2・3.1・3.3・4.1</td></tr><tr><td><code>goal -| ⋃. p; goal -| W. h;</code></td><td>必要な定義だけを sos に置いて投げ、h; で W. の形に</td><td>5.1</td></tr><tr><td><code>goal --| ax_s v;</code></td><td>クラス変数を含む公理を前提に、{s,c}ソートのまま Vampire へ（5.book）</td><td>6.1</td></tr><tr><td><code>goal --| ax_r[??p^:=&#96;…&#96;] v;</code> と <code>… ◀ ax_r h;</code></td><td>公理図式（schema）の実例を段の sos に直接書いて前提に使い、h; で「ax_r から導かれる」形に</td><td>6.3</td></tr><tr><td><code>ax_∅ -| ∅. p;</code></td><td>最後の段が thm と同じ goal・sos なので h; は無い（3.book）</td><td>5.2</td></tr><tr><td><code>/// W.'</code></td><td>〇.' があればそれで展開する slash（4.3）</td><td>4.3</td></tr></table>
txt <code>!prop/thm</code>・<code>!prop</code> の ! は「表示しない」印です（証明で使う補題など）。h; の段の関係の選び方は 3.book「h; の段の関係」。

section 基本関係
subsection 所属関係
txt 集合は現代の抽象数学の基礎概念と言えます。Matheliaは集合を容易に記述し、数学のスタートをスムーズにします。
txt 所属関係は2種類になります。「(クラスに)属する」以外に「(集合に)属する」が出てきます。
word ∈
br
txt Formel では「集合」と「クラス」を同一視して（いるように）扱えます（option ではなく組み込みの sc 変換）。
txt Form内でc-Formがあるべき所にあるs-Form ${\tt X}$ は $\{x \mid x \in {\tt X}\}$ に置き換えられます(sc変換)。
txt <div style="border-left:4px solid #0b64c8;background:#f3f7ff;padding:6px 10px"><b>sc 変換の例</b>（Y・X は s-Form。右は slash_cli の結果）<br><code>x ∈_ Y</code> → <code>x ∈ Y</code>（∈_ の右は c-Form の位置なので sc 変換で Y が内包に替わり、その内包が cvt で開かれる）<br><code>X ⊂_ Y</code> → <code>∀ w2 (w2 ∈ X ⇒ w2 ∈ Y)</code>（⊂_ は次の 2.2）<br>集合の語の引数（例 <code>X ⊂ Y</code> の X, Y）は c-Form の位置ではないので変わりません（<code>X ⊂ Y</code> → <code>X ⊂ Y</code>）。</div>
txt 次の自明に見える定理が生まれます。
thm `X ∈ Y ⟺ X ∈_ Y` ◀ O
prf goal -| O p;
txt 　ソース：<code>thm &#96;X ∈ Y ⟺ X ∈_ Y&#96; ◀ O</code>　<code>prf goal -| O p;</code>
txt 高度な表現を使うと `[∈] {**}⇔ [∈_]` 
thm `X =_ \{ cls x | x ∈ X \}` ◀ O
prf goal -| O p;
txt 　ソース：<code>thm &#96;X =_ \{ cls x | x ∈ X \}&#96; ◀ O</code>　<code>prf goal -| O p;</code>
br
txt （通常の数学の教科書とは逆に）`=` の定義は `=_` の定義から誘導するのが自然です（表示ではどちらも = です。ソースでは <code>=</code>＝集合の等号、<code>=_</code>＝クラスの等号）。定義 =. は `X = Y ⟺ X =_ Y`（word_basis で紹介済み）。

subsection 包含関係
txt ここでも「集合の包含関係」と「クラスの包含関係」の２つがあります。
word ⊂_
word ⊂
prop ⊂_.
br
txt `⊂`の定義 ⊂. も`⊂_`の定義から誘導されます（`X ⊂ Y ⟺ X ⊂_ Y`・word_basis で紹介済み）（ソースでは <code>⊂</code> と <code>⊂_</code>。表示ではどちらも ⊂ です）。
prop/thm =.. ◀ W.
prf =.. / W. -| O p; =.. -| W. h;
txt 　ソース：<code>prop/thm =.. ◀ W.</code>　<code>prf =.. / W. -| O p; =.. -| W. h;</code>
txt ${\tt P}$ / ${\tt Q}$ は「${\tt P}$<span style="color:brown">|cvt</span> を ${\tt Q}$<span style="color:brown">|cvt</span> で展開したもの」とされます。

section 集合・クラスの例①
subsection 宇宙、空集合
word 𝕍
prop 𝕍.
prop/thm ∈_𝕍 <- `x ∈_ 𝕍` ◀ O
prf ∈_𝕍 -| O p;
txt 　ソース：<code>prop/thm ∈_𝕍 &lt;- &#96;x ∈_ 𝕍&#96; ◀ O</code>　<code>prf ∈_𝕍 -| O p;</code>
prop/thm ⊂_𝕍 <- `X ⊂_ 𝕍` ◀ O
prf ⊂_𝕍 -| O p;
txt 　ソース：<code>prop/thm ⊂_𝕍 &lt;- &#96;X ⊂_ 𝕍&#96; ◀ O</code>　<code>prf ⊂_𝕍 -| O p;</code>
br
word ∅
prop ∅.
prop/thm ∉∅ <- `x {/}∈ ∅` ◀ W.
prf ∉∅ / W. -| O p; ∉∅ -| W. h;
txt 　ソース：<code>prop/thm ∉∅ &lt;- &#96;x {/}∈ ∅&#96; ◀ W.</code>　<code>prf ∉∅ / W. -| O p; ∉∅ -| W. h;</code>
prop/thm ∅⊂ <- `∅ ⊂ X` ◀ W.
prf ∅⊂ // W. -| O p; ∅⊂ -| W. h;
txt 　ソース：<code>prop/thm ∅⊂ &lt;- &#96;∅ ⊂ X&#96; ◀ W.</code>　<code>prf ∅⊂ // W. -| O p; ∅⊂ -| W. h;</code>
txt prfの <code>/</code> の本数は $\mathbb{W}.$ を適用する回数です。足りないと証明が見つからず FAIL になります。例えば `X ∩ Y ⊂ X` ◀ W. は <code>goal / W. -| O p;</code> では FAIL、<code>goal // W. -| O p;</code> では OK です（∩ は 4.2 で紹介します）。迷ったら slash_cli で開き残りの語が無いかを見てから本数を決めます（4.book）。

subsection 外延記法
txt <i>Formel</i> ではword familyも使用できます。指定した元だけを持つ集合を作ります。1以上の自然数 ${\tt n}$ に対して
word set\n
txt ただし s$^{\tt n}$ は s を${\tt n}$個並べたものです。
abbr set
txt Formelは `…` や `\n` はしかるべく処理します。例　`\{ set x ; \{ set x ; y \} \}` ≈ `set2 (x , set2 (x , y))`
br
txt 定義familyも使用できます。Bookで次のset${\tt n}$.が紹介されると $\mathbb{W}.$ は無限列になります。
prop set\n.

subsection べき集合
word ℘
prop ℘.
prop/thm wp0 ◀ W.
prf wp0 //// W. -| O p; wp0 -| W. h;
txt 　ソース：<code>prop/thm wp0 ◀ W.</code>　<code>prf wp0 //// W. -| O p; wp0 -| W. h;</code>

newpage
section 集合・クラスの例②

subsection 和・積
word ⋃_ ⋂_
word ⋃ ⋂
txt クラスの和・積は綺麗に定義でき、集合の和・積の定義はそこから誘導されます。
prop ⋃_.
prop ⋂_.
prop ⋃.
prop ⋂.
txt 例えば　⋃.<span style="color:brown">|cvt</span> … `∀ x (x ∈ ⋃ calX ⟺ [ ∃ X ∈_ calX . x ∈ X ])`
prop/thm ⋂_∅ <- `⋂_ ∅ =_ 𝕍` ◀ W.
prf ⋂_∅ / W. -| O p; ⋂_∅ -| W. h;
txt 　ソース：<code>prop/thm ⋂_∅ &lt;- &#96;⋂_ ∅ =_ 𝕍&#96; ◀ W.</code>　<code>prf ⋂_∅ / W. -| O p; ⋂_∅ -| W. h;</code>
txt W. に入るのは gram に c を含まない語の定義だけ（4.book）なので、⋂_. ・𝕍. ・=_. は W. に入りません。これらの定義は、-| の中の <span style="color:brown">|cvt+</span>（5.book）が開きます。W. から来るのは ∅. などです。
br
txt Bookでは<note>hidden prop<?>Bookを美しくするために表示したくはないけど、証明では何度も使われる補題</note>を使うこともできます。ソースでは次のように <code>!prop/thm</code> と書くと、表示されずに Thm として示され、後の prf で使えます。
!prop/thm ⋂.' ◀ W.
prf ⋂.' /// W. -| O p; ⋂.' -| W. h;
txt 　ソース：<code>!prop/thm ⋂.' ◀ W.</code>　<code>prf ⋂.' /// W. -| O p; ⋂.' -| W. h;</code>
txt ここでは中身を特別に表示しておきます。
prop ⋂.'

subsection 合併・共通部分
word ∪_ ∩_
prop ∪_.
prop ∩_.
word ∪ ∩
prop ∪.
prop ∩.

subsection 特殊なslash計算
prop/thm ∩=⋂ <- `X ∩ Y = ⋂ \{ set X ; Y \}` ◀ W.
prf ∩=⋂ /// W.' -| O p; ∩=⋂ -| W. h;
txt 　ソース：<code>prop/thm ∩=⋂ &lt;- &#96;X ∩ Y = ⋂ \{ set X ; Y \}&#96; ◀ W.</code>　<code>prf ∩=⋂ /// W.' -| O p; ∩=⋂ -| W. h;</code>

txt ${\tt P}$ / W. は「${\tt P}$ を 〇. で展開したもの」でした。 ${\tt P}$ / W.' は「${\tt P}$ を 〇.' があれば 〇.'、無ければ 〇. で展開したもの」です。ただし 〇.' の左辺が 〇. の左辺の形を含まないときは、〇. でも展開します（両方が別の場所に当たる）。〇.' の左辺が `=` の式（`X = ∅` など）のときは、W.' では `=` の定義 =. が先に当たるので、〇.' を使うには W.'!=. と書きます。 
txt 〇. が `$P ⟹ $Q ⇔ $R` のときは `$Q ⟺ \\{ And $P ⇒ $R \\ ¬ $P ⇒ $Q' \\}` に変換してから展開します。
txt ただし `$Q'` は `$Q` の 〇 を 〇_alias にしたものです。〇_alias は無駄な展開を防ぐためにあり / の処理終了時に 〇 に戻されます。
txt 上のprfでは
txt 　/ W.' … <code>[∀ w1 [⇔ [∈ w1 [∩ X Y]] [∈ w1 [⋂ [set2 X Y]]]]]</code>
txt 　// W.' … <code>[∀ w1 [⇔ [and [∈ w1 X] [∈ w1 Y]] [and [⇒ [∃ w2 [∈ w2 [set2 X Y]]] [∀ w3 [⇒ [∈ w3 [set2 X Y]] [∈ w1 w3]]]] [⇒ [¬ [∃ w2 [∈ w2 [set2 X Y]]]] [∈ w1 [⋂ [set2 X Y]]]]]]]</code>
txt 　/// W.' … <code>[∀ w1 [⇔ [and [∈ w1 X] [∈ w1 Y]] [and [⇒ [∃ w2 [or [= w2 X] [= w2 Y]]] [∀ w3 [⇒ [or [= w3 X] [= w3 Y]] [∈ w1 w3]]]] [⇒ [¬ [∃ w2 [or [= w2 X] [= w2 Y]]]] [∈ w1 [⋂ [set2 X Y]]]]]]]</code>
txt （slash_cli の出力そのまま＝前置記法。〇_alias は / の処理の終わりに 〇 へ戻るので、出力には出ません。）

newpage
section 集合の存在について①

subsection クラスが集合となるか
word Exi
prop Exi.
br
txt 集合でないクラスは固有クラスと呼ばれます。最初の例はRussellクラスです。
word 𝕍0
prop 𝕍0.
prop/thm ¬Exi𝕍0 <- `¬ Exi 𝕍0` ◀ O
prf ¬Exi𝕍0 -| O p;
txt 　ソース：<code>prop/thm ¬Exi𝕍0 &lt;- &#96;¬ Exi 𝕍0&#96; ◀ O</code>　<code>prf ¬Exi𝕍0 -| O p;</code>
br
txt もう一つ例を作ってみます。
word 𝕍1
prop 𝕍1.
prop/thm ¬Exi𝕍1 <- `¬ Exi 𝕍1` ◀ O
prf ¬Exi𝕍1 -| O p;
txt 　ソース：<code>prop/thm ¬Exi𝕍1 &lt;- &#96;¬ Exi 𝕍1&#96; ◀ O</code>　<code>prf ¬Exi𝕍1 -| O p;</code>
prop/thm 𝕍1⊂_𝕍0 <- `𝕍1 ⊂_ 𝕍0` ◀ O
prf 𝕍1⊂_𝕍0 -| O p;
txt 　ソース：<code>prop/thm 𝕍1⊂_𝕍0 &lt;- &#96;𝕍1 ⊂_ 𝕍0&#96; ◀ O</code>　<code>prf 𝕍1⊂_𝕍0 -| O p;</code>
prop/thm 𝕍1=_cls <- `𝕍1 =_ \{ cls x | x {/}∈ ⋃ x \}` ◀ W.
prf 𝕍1=_cls -| ⋃. p; 𝕍1=_cls -| W. h;
txt 　ソース：<code>prop/thm 𝕍1=_cls &lt;- &#96;𝕍1 =_ \{ cls x | x {/}∈ ⋃ x \}&#96; ◀ W.</code>　<code>prf 𝕍1=_cls -| ⋃. p; 𝕍1=_cls -| W. h;</code>

subsection ZF
txt 集合論の公理系についてはZF(Zermelo-Fraenkel)が有名です。
txt =.の$\Longleftarrow$ は外延性公理と呼ばれ、ZFの公理の１つです。ZFの公理は、これと正則性公理（5.4）以外は集合の存在を主張するものです。
br
txt 以下のZFの4公理は、Matheliaではwordの定義から導出される定理とすることが多いです。ただし公理が要らなくなるのではありません：∅・set2・℘・⋃ を返り値が s の語として定義 prop を置いた時点で、その集合が存在することを仮定しています。<b>存在の仮定を、公理から定義 prop へ移したと読みます。</b>
txt 空集合公理
prop/thm ax_∅ <- `Exi \{ cls x | ⊥ \}` ◀ ∅.
prf ax_∅ -| ∅. p;
txt 　ソース：<code>prop/thm ax_∅ &lt;- &#96;Exi \{ cls x | ⊥ \}&#96; ◀ ∅.</code>　<code>prf ax_∅ -| ∅. p;</code>
txt 対集合公理
prop/thm ax_set2 <- `Exi \{ cls a | a = x or a = y \}` ◀ set2.
prf ax_set2 -| set2. p;
txt 　ソース：<code>prop/thm ax_set2 &lt;- &#96;Exi \{ cls a | a = x or a = y \}&#96; ◀ set2.</code>　<code>prf ax_set2 -| set2. p;</code>
txt べき集合公理
prop/thm ax_℘ <- `Exi \{ cls A | A ⊂ X \}` ◀ ℘.
prf ax_℘ -| ℘. p;
txt 　ソース：<code>prop/thm ax_℘ &lt;- &#96;Exi \{ cls A | A ⊂ X \}&#96; ◀ ℘.</code>　<code>prf ax_℘ -| ℘. p;</code>
txt 和集合公理
prop/thm ax_⋃ <- `Exi \{ cls x | [ ∃ X ∈ calX . x ∈ X ] \}` ◀ ⋃.
prf ax_⋃ -| ⋃. p;
txt 　ソース：<code>prop/thm ax_⋃ &lt;- &#96;Exi \{ cls x | [ ∃ X ∈ calX . x ∈ X ] \}&#96; ◀ ⋃.</code>　<code>prf ax_⋃ -| ⋃. p;</code>

subsection 無限公理
txt 後続関数を準備しておきます。von Neumannは自然数を `0 = ∅`, `1 = ∅ suc`, … と作っていきました。
word suc
prop suc.
txt 先の4公理は初等的な集合を作り出しますが、無限集合は次の公理により初めて生まれます。
prop ax_∞ <- `∃ M (∅ ∈ M and [ ∀ x ∈ M . x suc ∈ M ])`
txt 空集合公理 は 無限公理 から導出されます。ただし下の prf は ∅. も前提に使っているので（ax_∞ の式自体が ∅ を含む）、「無限公理だけから空集合の存在が出る」ことを示す例にはなっていません。
thm ax_∅ ◀ W. , ax_∞
prf ax_∅ -| ax_∞ , ∅. p; ax_∅ -| W. , ax_∞ h;
txt 　ソース：<code>thm ax_∅ ◀ W. , ax_∞</code>　<code>prf ax_∅ -| ax_∞ , ∅. p; ax_∅ -| W. , ax_∞ h;</code>

subsection 正則性公理(基礎の公理)
txt 次の公理はvon Neumannによって導入されたものです。
prop ax0
!prop/thm ax0' ◀ W. , ax0
prf ax0' -| ax0 // W. p; ax0' -| W. , ax0 h;
txt 　ソース：<code>!prop/thm ax0' ◀ W. , ax0</code>　<code>prf ax0' -| ax0 // W. p; ax0' -| W. , ax0 h;</code>
prop/thm 𝕍1=_𝕍 <- `𝕍1 =_ 𝕍` ◀ W. , ax0
prf 𝕍1=_𝕍 / W. -| ax_set2 , ax0' p; 𝕍1=_𝕍 -| W. , ax0 h;
txt 　ソース：<code>prop/thm 𝕍1=_𝕍 &lt;- &#96;𝕍1 =_ 𝕍&#96; ◀ W. , ax0</code>　<code>prf 𝕍1=_𝕍 / W. -| ax_set2 , ax0' p; 𝕍1=_𝕍 -| W. , ax0 h;</code>

newpage
section 集合の存在について②

subsection 分出公理
txt 集合の部分クラスは集合である、ことが要請されます。
prop ax_s
txt 宇宙も固有クラスになります(ax0からも導出されます)。
prop/thm ¬Exi𝕍 <- `¬ Exi 𝕍` --| ax_s
prf ¬Exi𝕍 -| ax_s[C_:=`𝕍0`] p; ¬Exi𝕍 --| ax_s h;
txt 　ソース：<code>prop/thm ¬Exi𝕍 &lt;- &#96;¬ Exi 𝕍&#96; --| ax_s</code>　<code>prf ¬Exi𝕍 -| ax_s[C_:=&#96;𝕍0&#96;] p; ¬Exi𝕍 --| ax_s h;</code>
txt <code>ax_s[C_:=&#96;𝕍0&#96;]</code> は、ax_s の自由なクラス変数 C_ に 𝕍0 を代入した実例 <code>∃ X \, 𝕍0 ⊂_ X ⟹ Exi 𝕍0</code> です。prop のクラス変数への代入は、段の sos に直接書けます（名前を付けて <code>Le := ax_s[C_:=&#96;𝕍0&#96;] ;</code> としても同じ）。名前の無い式の項にも書けます：<code>&#96;x ∈_ A_&#96;[A_:=&#96;|B_&#96;]</code>（式は名前の無い prop として扱います。0_tutorial_jp/3.book）。実例は代入で作るので、証明器に示させる段は要りません。結論の段 <code>¬Exi𝕍 --| ax_s h;</code>（thm が --| なので最後の段も --|。-| の段をまたいでつなぐので確かめ直しが入る）では、主張の sos に ax_s があるので、Hyperion がそれを ax_s の実例と認めます（主張の sos に無い公理の実例は認めません）。本で定義した prop を主張の sos に置いた場合も同じです。例外は、証明済みのクラス変数の Thm（自由なクラス変数が1つで、それが自分の sos に現れないもの。articles2/word_set.book の帰納法 INDC など）で、主張の sos に無くても実例を使えます。
txt 証明済みのクラス変数の Thm を実例で使うときの注意が2つあります。<br>　・その Thm は <code>prop/thm</code>（表示しないなら <code>!prop/thm</code>）で立てます。<code>let/thm</code> の名前には代入できず、「let/thm の名前には代入できません」で落ちます。<br>　・自由なクラス変数の名前を、自分の sos にある prop のクラス変数と違うものにします。例えば sos に帰納法の公理 IND𝕄（C_ を含む）を置いた強い帰納法の Thm で自由な変数も C_ にすると、C_ が自分の sos に現れるので実例を使えません。D_ にします（INDC も D_）。
txt 代入の変数と同じ名前の prf ラベルは使えません。例えば prf で <code>C_ := &#96;\{ cls B | … \}&#96; ;</code> と置いてから <code>ax_s[C_:=&#96;C_&#96;]</code> と書くと、<code>:=</code> の左の C_（ax_s の変数）をラベルと取り違えるので、その Thm の査読エラーになります。ラベルを別の名前（<code>K_</code> など）にして <code>ax_s[C_:=&#96;K_&#96;]</code> と書きます。
txt 述語変数への代入（<code>ax_r[??p^:=…]</code>）も同じように段の sos に直接書けます（下の置換公理の節）。ただし主張（thm 行）の sos には書けません。
txt どこに何を書けるかをまとめると次のとおりです（表の右の列は、∀ を書いた述語変数の prop と schema の場合です）。
txt <table border="1"><tr><th>書く所</th><th>実例 <code>〇[V:=&#96;θ&#96;]</code>（クラス変数・述語変数への代入）</th><th>素の名前（∀ の述語変数を持つ prop・schema）</th></tr><tr><td>thm 行の sos</td><td>書けない</td><td>書く（実例の出所。無いと結論の段が通らない）</td></tr><tr><td>p; v; の段の sos</td><td>書ける（実例の式が証明器に渡る）</td><td>書くと査読エラー（証明器に渡らない）</td></tr><tr><td>s; の段の sos</td><td>書ける</td><td><code>satallax+ predicate:all</code> の本の <code>--| … s;</code> だけ、高階の公理として渡る（既定では査読エラー）</td></tr><tr><td>h の段の sos</td><td>—</td><td>書く（thm 行と同じ）</td></tr></table>
br
txt ax_sはZFの分出公理と同値です。ZFは一階論理なので、分出公理は ?R^ に入る式ごとに1つの公理（無限個の公理の集まり＝公理図式）です。Mathelia では「すべての ?R^ について」を式に書いて1つの prop にします（書き方は下の置換公理の節）。
prop ax_s' <- `∀ ?R^ ( ∀ X Exi \{ cls x ∈ X | ?R^ (x) \} )`
thm `∀ X Exi \{ cls x ∈ X | ?R^ (x) \}` ◀ ax_s
prf goal --| ax_s v;
txt 　ソース：<code>prop ax_s' &lt;- &#96;∀ ?R^ ( ∀ X Exi \{ cls x ∈ X | ?R^ (x) \} )&#96;</code>　<code>thm &#96;∀ X Exi \{ cls x ∈ X | ?R^ (x) \}&#96; ◀ ax_s</code>　<code>prf goal --| ax_s v;</code>
txt ∀ の述語変数を持つ prop の名前は goal に書けないので、∀ ?R^ の中の式をそのまま書きます。主張の中で自由な ?R^ は「どの述語 R についても」と読みます（Thm 全体で1回だけ量化・7.book）。証明は、ax_s のクラス変数 C_ に <code>\{ cls x ∈ X | ?R^ (x) \}</code> を入れるだけの一階の推論です。
thm ax_s ◀ ax_s'
prf ax_s --| ax_s'[?R^:=`x ∈_ C_`] v; ax_s ◀ ax_s' h;
txt 　ソース：<code>thm ax_s ◀ ax_s'</code>　<code>prf ax_s --| ax_s'[?R^:=&#96;x ∈_ C_&#96;] v; ax_s ◀ ax_s' h;</code>
txt 逆向きは、ax_s' の ?R^ に <code>x ∈_ C_</code> を代入した実例を使います（代入する式には、引数 x 以外の自由変数 C_ もそのまま書けます）。
txt <div style="border-left:4px solid #0b64c8;background:#f3f7ff;padding:6px 10px"><b>代入できるのは ∀ を書いた述語変数だけ</b><br>∀ を書かずに sos に置いた prop の <code>P^</code>・<code>?R^</code> は、その Thm の中で1つの決まった命題・述語を表すだけです。どの投げ先（p・v・s）でも同じで、例えば <code>⊥ ◀ P^</code> は成り立ちません（P が真なら反例）。「どの述語についても成り立つ」ことを前提として使いたいときは <code>prop 名 &lt;- &#96;∀ ?R^ ( … )&#96;</code> と書いて、代入 <code>名[?R^:=θ]</code> で実例を作ります。</div>
br
txt 空集合公理 はax_sからも導出されます。
thm ax_∅ ◀ ax_s
prf ax_∅ --| ax_s v;
txt 　ソース：<code>thm ax_∅ ◀ ax_s</code>　<code>prf ax_∅ --| ax_s v;</code>

subsection 集合に名前を付けて、最後に消す（h[fix] の ∃除去）
txt 長い証明では、内包で作った集合に定数の名前 <code>|Y</code> を付けて使い回すと、式が短くなり速くなります。名前は仮定ラベル <code>|Y =_ θ</code>（θ は c-Form）で置きます。最後の <code>h[fix];</code> で、θ が集合になる根拠があれば hyperion がこの仮定を消します（∃除去）。
thm `∃ y ∀ x \, ( x ∈ y ⟺ ( x ∈ a and x ∈ b ) )` ◀ W. , ax_s
prf |Y_ := `\{ cls x | x ∈ |a and x ∈ |b \}` ;
    hyY <- `|Y =_ |Y_` ;
    LYs <- `|Y_ ⊂_ |a` -| O p;
    `∃ y ∀ x \, ( x ∈ y ⟺ ( x ∈ |a and x ∈ |b ) )` -| hyY p;
    goal -| W. , ax_s h[fix];
txt 　ソース：
txt 　<code>prf |Y_ := &#96;\{ cls x | x ∈ |a and x ∈ |b \}&#96; ;</code> … c-Form に Form 名を付ける
txt 　<code>    hyY &lt;- &#96;|Y =_ |Y_&#96; ;</code> … 集合の定数 |Y がそのクラスと等しい、という仮定ラベル
txt 　<code>    LYs &lt;- &#96;|Y_ ⊂_ |a&#96; -| O p;</code> … 根拠：θ が集合 |a に含まれる
txt 　<code>    &#96;∃ y ∀ x \, ( x ∈ y ⟺ ( x ∈ |a and x ∈ |b ) )&#96; -| hyY p;</code> … |Y を使って示す
txt 　<code>    goal -| W. , ax_s h[fix];</code> … hyY を消し、|a・|b の bar を外す
txt hyY を前件へ戻すのではなく消せるのは、「θ と等しい集合がある」（<code>Exi θ</code>）からです。根拠は、前の段で示した <code>Exi θ</code> か、<code>θ ⊂_ σ</code>（このとき主張の sos に ax_s が要る＝分出公理で Exi θ）です。
txt <div style="border-left:4px solid #0b64c8;background:#f3f7ff;padding:6px 10px"><b>∃除去の約束</b>（h[fix]; の約束〈3.book〉に加えて）<br>・仮定ラベルは <code>|Y =_ θ</code> の形。|Y は集合の定数、θ に |Y も自由変数（束縛されていない bar の無い文字）も含めない<br>・根拠の段（<code>Exi θ</code> か <code>θ ⊂_ σ</code>）を、h[fix]; より前に示す。根拠の段に消す仮定 hyY を使わない<br>・|Y が thm の goal・sos（W. の中の定義を含む）・残る仮定・根拠の goal に現れない<br>・仮定が複数あれば1つずつ消す（順番は hyperion が探す）</div>
txt 根拠が無いと消せません。例えばラッセルのクラス <code>\{ cls x | x {/}∈ x \}</code> に |Y を等しいとおくと矛盾が出ますが、集合になる根拠が無いので h[fix]; は FAIL します。上の例でも LYs の段を抜くと「exists-elimination: no set justification for hyY」で FAIL します。

subsection 同じ段の3つの書き方
txt クラスを集合として使う段は、いくつかの書き方ができます。例：articles1/63.book の <code>&#96;X ≤# ℘ X&#96; ◀ W. , ax_s</code>。|g_ は単元集合への写像のクラスで、<code>|g_ ∈ |X →I ℘ |X</code> とは書けない（型が合わない）ので、それと等しい集合が要ります。
txt ① 仮定ラベル hyG で集合の定数 |g を置き、上の節と同じく h[fix]; の ∃除去で消す（0.15秒）。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">prf |g_ := &#96;\{ \&lt; pr x ; \{ set x \} \&gt; Cls x | x ∈ |X \}&#96; ;<br>&nbsp;&nbsp;&nbsp;&nbsp;hyG &lt;- &#96;|g =_ |g_&#96; ;<br>&nbsp;&nbsp;&nbsp;&nbsp;&#96;|g_ ⊂_ |X ^^pr ℘ |X&#96; // W.&#39;!=. -| set1. p;<br>&nbsp;&nbsp;&nbsp;&nbsp;LeI &lt;- &#96;|g ∈ |X →I ℘ |X&#96; /// W.&#39;!=. -| hyG , pr:0 , set1. p;<br>&nbsp;&nbsp;&nbsp;&nbsp;&#96;|X ≤# ℘ |X&#96; / ≤#.&#39; -| LeI p;<br>&nbsp;&nbsp;&nbsp;&nbsp;goal -| W. , ax_s h[fix];</div>
txt ② ラベルを置かず、LeI の sos に <code>&#96;|g =_ |g_&#96;</code> を直接書く。h[fix]; は sos の backtick の項も仮定として集めます（0.15秒）。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">prf |g_ := &#96;\{ \&lt; pr x ; \{ set x \} \&gt; Cls x | x ∈ |X \}&#96; ;<br>&nbsp;&nbsp;&nbsp;&nbsp;&#96;|g_ ⊂_ |X ^^pr ℘ |X&#96; // W.&#39;!=. -| set1. p;<br>&nbsp;&nbsp;&nbsp;&nbsp;LeI &lt;- &#96;|g ∈ |X →I ℘ |X&#96; /// W.&#39;!=. -| &#96;|g =_ |g_&#96; , pr:0 , set1. p;<br>&nbsp;&nbsp;&nbsp;&nbsp;&#96;|X ≤# ℘ |X&#96; / ≤#.&#39; -| LeI p;<br>&nbsp;&nbsp;&nbsp;&nbsp;goal -| W. , ax_s h[fix];</div>
txt ③ |g も LeI も置かず、「|g_ と等しい集合がある」を <code>ax_s[C_:=&#96;|g_&#96;]</code> で sos に入れて証明器に任せる（0.12秒・63.book の今の形）。この段は p; では Prover9 が時間切れになり、<code>/// W.</code> と v; で通ります。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">prf |g_ := &#96;\{ \&lt; pr x ; \{ set x \} \&gt; Cls x | x ∈ |X \}&#96; ;<br>&nbsp;&nbsp;&nbsp;&nbsp;Le &lt;- &#96;|g_ ⊂_ |X ^^pr ℘ |X&#96; // W.&#39;!=. -| set1. p;<br>&nbsp;&nbsp;&nbsp;&nbsp;&#96;|X ≤# ℘ |X&#96; / ≤#.&#39; /// W. -| ax_s[C_:=&#96;|g_&#96;] , Le , pr:0 , set1. v;<br>&nbsp;&nbsp;&nbsp;&nbsp;goal -| W. , ax_s h[fix];</div>
txt どれも正しい証明です。段の意味が読みやすいのは①、短いのは③です。書き換えたら、写した slash（例：ラベルに付いていた <code>/// W.&#39;!=.</code>）も外して試します。②では要りませんでした。

subsection 置換公理
txt 置換公理は、関数的な性質による集合の像は集合である、ことを要請します。順序対は使いません。
abbr ！
abbr ∃！
txt `[ ！ y P ]` は「Pを満たすyは高々1つ」です。`∀ x \, [ ！ y \, x ??p^ y ]` は「??p^ は各xに高々1つのyを対応させる」ことを表します。
prop ax_r <- `∀ ??p^ ( ∀ x \, [ ！ y \, x ??p^ y ] ⟹ ∀ X \, Exi \{ cls y | [ ∃ x ∈ X . x ??p^ y ] \} )`
txt `??p^` は2項の述語変数です。ZFの置換公理は ??p^ に入る式ごとに1つの公理（無限個の公理の集まり）で、ax_r は「すべての ??p^ について」とまとめて書いたものです。
txt <div style="border-left:4px solid #0b64c8;background:#f3f7ff;padding:6px 10px"><b>∀ の述語変数を持つ prop への代入</b><br>書き方：<code>prop 名 &lt;- &#96;∀ ??p^ ( ψ )&#96;</code><br>代入：<code>ax_r[??p^:=&#96;θ&#96;]</code> … ψ の ??p^ に θ を入れた実例（無限個の公理のうちの1つ）。段の sos に直接書くか、<code>!prop 名 &lt;- ax_r[??p^:=&#96;θ&#96;]</code> で名前を付けて使う<br>使い方：実例を前提に証明し、最後に <code>… ◀ ax_r h;</code> で「ax_r から導かれる」形にまとめる<br>素の名前 ax_r は主張の sos と結論の段 h に書く（書ける所は上の「分出公理」の節の表）。</div>
txt 代入する式の書き方：??p^ の1番目・2番目の引数は、ψ の中の <code>x ??p^ y</code> にならって x、y と書きます（ψ の中の ??p^ の出現は、どれも同じ引数の名前でなければなりません）。θ のそれ以外の自由変数（C_ など）はそのまま残せます。同じ意味を <code>schema ax_r(??p^;x,y;C_,s,t,u,v) := &#96;ψ&#96;</code>（引数の名前と残してよい変数を宣言する公理図式）でも書けます（7.book）。
br
txt 分出公理はax_rから導かれます。??p^ に「x∈_C_ and y=x」を代入したインスタンスを使います。
thm ax_s ◀ ax_r
prf ax_s --| ax_r[??p^:=`x ∈_ C_ and y = x`] v;
    ax_s ◀ ax_r h;
txt 　ソース：<code>thm ax_s ◀ ax_r</code>　<code>prf ax_s --| ax_r[??p^:=&#96;x ∈_ C_ and y = x&#96;] v;</code>　<code>　　ax_s ◀ ax_r h;</code>
txt 1段目は代入した実例を sos に直接書いて前提に使い、最後の <code>ax_s ◀ ax_r h;</code> で「ax_r から導かれる」という形のThmにまとめます。代入する式に x と y の両方が現れる必要はありません（例えば <code>!prop 名 &lt;- ax_r[??p^:=&#96;y = ∅&#96;]</code> で「X の各元を ∅ に送った像は集合」が示せます）。
br
txt 対集合公理もax_rから導かれます。まず、相異なる2元を持つ集合があることを、空集合とべき集合だけから示します（`℘ (℘ ∅)` は `∅` と `℘ ∅` を元に持ち、`∅ ∈ ℘ ∅` なので両者は異なります。等しいとすると `∅ ∈ ∅` となり ∅. に反するため）。
prop/thm le_set2 <- `∃ C \, [ ∃* s ; t ([ s ; t col ∈ C ]) ]` ◀ W.
prf le_set2 -| ℘. , ∅. , ⊂. p; le_set2 -| W. h;
txt 　ソース：<code>prop/thm le_set2 &lt;- &#96;∃ C \, [ ∃* s ; t ([ s ; t col ∈ C ]) ]&#96; ◀ W.</code>　<code>prf le_set2 -| ℘. , ∅. , ⊂. p; le_set2 -| W. h;</code>
txt 相異なる2元 s, t を持つ集合 C に対し、??p^ に「s を u へ、t を v へ送る」関係を代入すると、C の像は $\{u, v\}$ です。対集合の定義 set2. は使っていません。ここでは実例に <code>!prop</code> で名前を付けて使っています（直接書いても同じ）。
!prop ax_r_atST <- ax_r[??p^:=`(x = s and y = u) or (x = t and y = v)`]
thm ax_set2 ◀ ax_r , le_set2
prf ax_set2 --| ax_r_atST , le_set2 v;
    ax_set2 ◀ ax_r , le_set2 h;
txt 　ソース：<code>!prop ax_r_atST &lt;- ax_r[??p^:=&#96;(x = s and y = u) or (x = t and y = v)&#96;]</code>　<code>thm ax_set2 ◀ ax_r , le_set2</code>　<code>prf ax_set2 --| ax_r_atST , le_set2 v;</code>　<code>　　ax_set2 ◀ ax_r , le_set2 h;</code>

0_tutorial_AI/6.book

`0_tutorial_AI/6.book`