6 集合の存在について②

6.1 分出公理

集合の部分クラスは集合である、ことが要請されます。
ax_s … \(\exists X \, C \subset X \Longrightarrow \dot\exists C\)
宇宙も固有クラスになります(ax0からも導出されます)。
¬Exi𝕍 … \(\neg \dot\exists \mathbb{V}\) \(\blacktriangleleft\) ax_s
　ソース：prop/thm ¬Exi𝕍 <- `¬ Exi 𝕍` --| ax_s　prf ¬Exi𝕍 -| ax_s[C_:=`𝕍0`] p; ¬Exi𝕍 --| ax_s h;
ax_s[C_:=`𝕍0`] は、ax_s の自由なクラス変数 C_ に 𝕍0 を代入した実例 ∃ X \, 𝕍0 ⊂_ X ⟹ Exi 𝕍0 です。prop のクラス変数への代入は、段の sos に直接書けます（名前を付けて Le := ax_s[C_:=`𝕍0`] ; としても同じ）。名前の無い式の項にも書けます：`x ∈_ A_`[A_:=`|B_`]（式は名前の無い prop として扱います。0_tutorial_jp/3.book）。実例は代入で作るので、証明器に示させる段は要りません。結論の段 ¬Exi𝕍 --| ax_s h;（thm が --| なので最後の段も --|。-| の段をまたいでつなぐので確かめ直しが入る）では、主張の sos に ax_s があるので、Hyperion がそれを ax_s の実例と認めます（主張の sos に無い公理の実例は認めません）。本で定義した prop を主張の sos に置いた場合も同じです。例外は、証明済みのクラス変数の Thm（自由なクラス変数が1つで、それが自分の sos に現れないもの。articles2/word_set.book の帰納法 INDC など）で、主張の sos に無くても実例を使えます。
証明済みのクラス変数の Thm を実例で使うときの注意が2つあります。
　・その Thm は prop/thm（表示しないなら !prop/thm）で立てます。let/thm の名前には代入できず、「let/thm の名前には代入できません」で落ちます。
　・自由なクラス変数の名前を、自分の sos にある prop のクラス変数と違うものにします。例えば sos に帰納法の公理 IND𝕄（C_ を含む）を置いた強い帰納法の Thm で自由な変数も C_ にすると、C_ が自分の sos に現れるので実例を使えません。D_ にします（INDC も D_）。
代入の変数と同じ名前の prf ラベルは使えません。例えば prf で C_ := `\{ cls B | … \}` ; と置いてから ax_s[C_:=`C_`] と書くと、:= の左の C_（ax_s の変数）をラベルと取り違えるので、その Thm の査読エラーになります。ラベルを別の名前（K_ など）にして ax_s[C_:=`K_`] と書きます。
述語変数への代入（ax_r[??p^:=…]）も同じように段の sos に直接書けます（下の置換公理の節）。ただし主張（thm 行）の sos には書けません。
どこに何を書けるかをまとめると次のとおりです（表の右の列は、∀ を書いた述語変数の prop と schema の場合です）。

書く所	実例 〇[V:=`θ`]（クラス変数・述語変数への代入）	素の名前（∀ の述語変数を持つ prop・schema）
thm 行の sos	書けない	書く（実例の出所。無いと結論の段が通らない）
p; v; の段の sos	書ける（実例の式が証明器に渡る）	書くと査読エラー（証明器に渡らない）
s; の段の sos	書ける	satallax+ predicate:all の本の --| … s; だけ、高階の公理として渡る（既定では査読エラー）
h の段の sos	—	書く（thm 行と同じ）

ax_sはZFの分出公理と同値です。ZFは一階論理なので、分出公理は ?R^ に入る式ごとに1つの公理（無限個の公理の集まり＝公理図式）です。Mathelia では「すべての ?R^ について」を式に書いて1つの prop にします（書き方は下の置換公理の節）。
ax_s' … \(\forall {R} ( \forall X \dot\exists \{ x \in X \mid {R} ( x ) \} )\)
\(\forall X \dot\exists \{ x \in X \mid {R} ( x ) \}\) \(\blacktriangleleft\) ax_s
　ソース：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;
∀ の述語変数を持つ prop の名前は goal に書けないので、∀ ?R^ の中の式をそのまま書きます。主張の中で自由な ?R^ は「どの述語 R についても」と読みます（Thm 全体で1回だけ量化・7.book）。証明は、ax_s のクラス変数 C_ に \{ cls x ∈ X | ?R^ (x) \} を入れるだけの一階の推論です。
ax_s \(\blacktriangleleft\) ax_s'
　ソース：thm ax_s ◀ ax_s'　prf ax_s --| ax_s'[?R^:=`x ∈_ C_`] v; ax_s ◀ ax_s' h;
逆向きは、ax_s' の ?R^ に x ∈_ C_ を代入した実例を使います（代入する式には、引数 x 以外の自由変数 C_ もそのまま書けます）。


空集合公理 はax_sからも導出されます。
ax_∅ \(\blacktriangleleft\) ax_s
　ソース：thm ax_∅ ◀ ax_s　prf ax_∅ --| ax_s v;

6.2 集合に名前を付けて、最後に消す（h[fix] の ∃除去）

長い証明では、内包で作った集合に定数の名前 |Y を付けて使い回すと、式が短くなり速くなります。名前は仮定ラベル |Y =_ θ（θ は c-Form）で置きます。最後の h[fix]; で、θ が集合になる根拠があれば hyperion がこの仮定を消します（∃除去）。
\(\exists y \forall x \, ( x \in y \Longleftrightarrow ( x \in a , x \in b ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
　ソース：
　prf |Y_ := `\{ cls x | x ∈ |a and x ∈ |b \}` ; … c-Form に Form 名を付ける
　 hyY <- `|Y =_ |Y_` ; … 集合の定数 |Y がそのクラスと等しい、という仮定ラベル
　 LYs <- `|Y_ ⊂_ |a` -| O p; … 根拠：θ が集合 |a に含まれる
　 `∃ y ∀ x \, ( x ∈ y ⟺ ( x ∈ |a and x ∈ |b ) )` -| hyY p; … |Y を使って示す
　 goal -| W. , ax_s h[fix]; … hyY を消し、|a・|b の bar を外す
hyY を前件へ戻すのではなく消せるのは、「θ と等しい集合がある」（Exi θ）からです。根拠は、前の段で示した Exi θ か、θ ⊂_ σ（このとき主張の sos に ax_s が要る＝分出公理で Exi θ）です。

根拠が無いと消せません。例えばラッセルのクラス \{ cls x | x {/}∈ x \} に |Y を等しいとおくと矛盾が出ますが、集合になる根拠が無いので h[fix]; は FAIL します。上の例でも LYs の段を抜くと「exists-elimination: no set justification for hyY」で FAIL します。

6.3 置換公理

置換公理は、関数的な性質による集合の像は集合である、ことを要請します。順序対は使いません。
abbr … \(! x P\) ≈ \(\forall y , z \in \{ x \mid P \} . y = z\)
abbr … \(\exists! x P\) ≈ \(\exists x P , ! x P\)
\(! y P\) は「Pを満たすyは高々1つ」です。 \(\forall x \, ! y \, x \mathbin{p} y\) は「??p^ は各xに高々1つのyを対応させる」ことを表します。
ax_r … \(\forall \mathbin{p} ( \forall x \, ! y \, x \mathbin{p} y \Longrightarrow \forall X \, \dot\exists \{ y \mid \exists x \in X . x \mathbin{p} y \} )\)
\(\mathbin{p}\) は2項の述語変数です。ZFの置換公理は ??p^ に入る式ごとに1つの公理（無限個の公理の集まり）で、ax_r は「すべての ??p^ について」とまとめて書いたものです。

代入する式の書き方：??p^ の1番目・2番目の引数は、ψ の中の x ??p^ y にならって x、y と書きます（ψ の中の ??p^ の出現は、どれも同じ引数の名前でなければなりません）。θ のそれ以外の自由変数（C_ など）はそのまま残せます。同じ意味を schema ax_r(??p^;x,y;C_,s,t,u,v) := `ψ`（引数の名前と残してよい変数を宣言する公理図式）でも書けます（7.book）。

分出公理はax_rから導かれます。??p^ に「x∈_C_ and y=x」を代入したインスタンスを使います。
ax_s \(\blacktriangleleft\) ax_r
　ソース：thm ax_s ◀ ax_r　prf ax_s --| ax_r[??p^:=`x ∈_ C_ and y = x`] v;　　　ax_s ◀ ax_r h;
1段目は代入した実例を sos に直接書いて前提に使い、最後の ax_s ◀ ax_r h; で「ax_r から導かれる」という形のThmにまとめます。代入する式に x と y の両方が現れる必要はありません（例えば !prop 名 <- ax_r[??p^:=`y = ∅`] で「X の各元を ∅ に送った像は集合」が示せます）。

対集合公理もax_rから導かれます。まず、相異なる2元を持つ集合があることを、空集合とべき集合だけから示します（ \(\wp ( \wp \emptyset )\) は \(\emptyset\) と \(\wp \emptyset\) を元に持ち、 \(\emptyset \in \wp \emptyset\) なので両者は異なります。等しいとすると \(\emptyset \in \emptyset\) となり ∅. に反するため）。
le_set2 … \(\exists C \, \exists^* s , t ( s , t \in C )\) \(\blacktriangleleft\) \(\mathbb{W}.\)
　ソース：prop/thm le_set2 <- `∃ C \, [ ∃* s ; t ([ s ; t col ∈ C ]) ]` ◀ W.　prf le_set2 -| ℘. , ∅. , ⊂. p; le_set2 -| W. h;
相異なる2元 s, t を持つ集合 C に対し、??p^ に「s を u へ、t を v へ送る」関係を代入すると、C の像は \(\{u, v\}\) です。対集合の定義 set2. は使っていません。ここでは実例に !prop で名前を付けて使っています（直接書いても同じ）。
ax_set2 \(\blacktriangleleft\) ax_r ，le_set2
　ソース：!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;