book集

section 集合
txt 集合は現代の抽象数学の基礎概念と言えます。

txt 特にsc_supというoptionが有効です。
txt それは「集合」と「クラス」を同一視して（いるように）扱えるようにします。

txt 所属関係は2種類あります。「(集合に)属する」と「(クラスに)属する」です。
word ∈

br
txt 集合は自然にクラスと見なされます。Form内でc-Formがあるべき所にあるs-Form \({\tt X}\) は \(\{x \mid x \in {\tt X}\}\) に置き換えられます(sc変換)。
txt 次の自明な定理が生まれます。
!let goal := `X =_ \{ cls x | x ∈ X \}`
thm goal -| O
prf goal p-| O;
!let goal := `X ∈ Y ⟺ X ∈_ Y`
thm goal -| O
prf goal p-| O;

br
txt （通常の数学の教科書とは逆に）`=` の定義を `=_` の定義から誘導するのが自然です。
prop =. := `X = Y ⟺ X =_ Y`
txt この\(\Longleftarrow\)は外延性公理と呼ばれ、ZFの公理の１つです。

br
txt クラスが集合となるか、が議論されます。
word Exi
prop Exi.

section 集合・クラスの最初の例
txt 宇宙を作ります。
word \V
prop \V.
!let goal := `x ∈_ \V`
thm goal -| O
prf goal p-| O;

br
txt 空集合を作ります。
word ∅
prop ∅.
!let goal := `x {/}∈ ∅`
thm goal -| W.
prf goal / W. p-| O; goal h-| W. ;
txt \(\mathbb{W}.\) はbook内変数で「〇. (〇は\(\mathbb{W}\)) という形のpropすべての列」です。この段階では =. ∅. です。
txt \({\tt P}\) ◀ \(\mathbb{W}.\) は「定義から\({\tt P}\)が示される」と読まれます。
txt ZFの公理の1つに空集合公理があります。私たちのシステムでは ∅. から導出するのが標準です。
!let goal := `Exi \{ cls x | ⊥ \}`
thm goal -| ∅.
prf goal p-| ∅.;

br
txt 集合でないクラスは固有クラスと呼ばれます。最初の例はRusselクラスです。
word \V0
prop \V0.
!let goal := `¬ Exi \V0`
thm goal -| O
prf goal p-| O;

section 包含関係
txt ここでも「集合の包含関係」と「クラスの包含関係」の２つがあります。
word ⊂_
word ⊂
prop ⊂_.
prop ⊂. := `X ⊂ Y ⟺ X ⊂_ Y`
txt `⊂`の定義は`⊂_`の定義から誘導されます。
prop/thm =.. -| W.
prf =.. / W. p-| O; =.. h-| W.;

br
txt 集合の部分クラスは集合である、ことが要請されます。
prop ax_s0
br
txt 宇宙も固有クラスになります。
!let goal := `¬ Exi \V`
thm goal --| ax_s0
!txt hint : goal -| `∃ X \, \V0 ⊂_ X ⟹ Exi \V0`
prf goal v--| ax_s0;

section ZF
txt 集合論の公理系についてはZF(Zermelo-Fraenkel)が有名です。ZFの中の一つに外延性公理があります。
txt 私たちのシステムではZFの公理そのものを採用せず、wordの定義を作ってZF公理を定理とすることが多いです。

1_basis/5_set.book

`1_basis/5_set.book`