未ログイン ／
ログイン
← ファイル一覧
（保存にはログインが要ります）
0_tutorial/6.book
ヘッダ
行番号
title 集合とクラス author admin import /common/word_basis formel /common/default thmel /common/zf
section 基本関係 subsection 所属関係 txt 集合は現代の抽象数学の基礎概念と言えます。Matheliaは集合を容易に記述し、数学のスタートをスムーズにします。 txt 所属関係は2種類になります。「(クラスに)属する」以外に「(集合に)属する」が出てきます。 word ∈ br txt default.formelでは<b>sc_sup</b>というoptionを有効にしています。それは「集合」と「クラス」を同一視して（いるように）扱えるようにします。 txt Form内でc-Formがあるべき所にあるs-Form \({\tt X}\) は \(\{x \mid x \in {\tt X}\}\) に置き換えられます(sc変換)。 txt 次の自明に見える定理が生まれます。 thm `X ∈ Y ⟺ X ∈_ Y` ◀ O prf goal -| O p; txt 高度な表現を使うと `[∈] {**}⇔ [∈_]` thm `X =_ \{ cls x | x ∈ X \}` ◀ O prf goal -| O p; br txt （通常の数学の教科書とは逆に）`=` の定義は `=_` の定義から誘導するのが自然です（表示ではどちらも = です。ソースでは <code>=</code>＝集合の等号、<code>=_</code>＝クラスの等号）。 prop =. subsection 包含関係 txt ここでも「集合の包含関係」と「クラスの包含関係」の２つがあります。 word ⊂_ word ⊂ prop ⊂_. br txt `⊂`の定義も`⊂_`の定義から誘導されます（ソースでは <code>⊂</code> と <code>⊂_</code>。表示ではどちらも ⊂ です）。 prop ⊂. prop/thm =.. ◀ W. prf =.. / W. -| O p; =.. -| W. h; txt default.thmelでは \({\tt P}\) / \({\tt Q}\) は「\({\tt P}\)<code>|cvt</code> を \({\tt Q}\)<code>|cvt</code> で展開したもの」とされます。 section 集合・クラスの例① subsection 宇宙、空集合 word 𝕍 prop 𝕍. thm `x ∈_ 𝕍` ◀ O prf goal -| O p; thm `X ⊂_ 𝕍` ◀ O prf goal -| O p; br word ∅ prop ∅. thm `x {/}∈ ∅` ◀ W. prf goal / W. -| O p; goal -| W. h; thm `∅ ⊂ X` ◀ W. prf goal // W. -| O p; goal -| W. h; 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 です。迷ったら本数を増やして試します。 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; newpage section 集合・クラスの例② subsection 和・積 word ⋃_ ⋂_ word ⋃ ⋂ txt クラスの和・積は綺麗に定義でき、集合の和・積の定義はそこから誘導されます。 prop ⋃_. prop ⋂_. prop ⋃. prop ⋂. txt 例えば ⋃.<code>|cvt</code> … `∀ x (x ∈ ⋃ calX ⟺ [ ∃ X ∈_ calX . x ∈ X ])` thm `⋂_ ∅ =_ 𝕍` ◀ W. prf goal / W. -| O p; goal -| W. h; txt W. に入るのは gram に c を含まない語の定義だけ（4.book）なので、⋂_. ・𝕍. ・=_. は W. に入りません。これらの定義は、-| の中の <code>|cvt+</code>（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 ここでは中身を特別に表示しておきます。 prop ⋂.' subsection 合併・共通部分 word ∪_ ∩_ prop ∪_. prop ∩_. word ∪ ∩ prop ∪. prop ∩. subsection 特殊なslash計算 thm `X ∩ Y = ⋂ \{ set X ; Y \}` ◀ W. prf goal /// W.' -| O p; goal -| W. h; 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.' … `∀ x (x ∈ X ∩ Y ⟺ x ∈ ⋂ \{ set X ; Y \})` txt // W.' … `∀ x (x ∈ X , x ∈ Y ⟺ \\{ And ∃ a ∈ \{ set X ; Y \} ⇒ [ ∀ a ∈ \{ set X ; Y \} . x ∈ a ] \\ ¬ ∃ a ∈ \{ set X ; Y \} ⇒ x ∈ ⋂_alias \{ set X ; Y \} \\})` txt /// W.' … `∀ x (x ∈ X , x ∈ Y ⟺ \\{ And ∃ a (a = X or a = Y) ⇒ ∀ a ((a = X or a = Y) ⇒ x ∈ a) \\ ¬ ∃ a (a = X or a = Y) ⇒ x ∈ ⋂ \{ set X ; Y \} \\})` newpage section 集合の存在について① subsection クラスが集合となるか word Exi prop Exi. br txt 集合でないクラスは固有クラスと呼ばれます。最初の例はRussellクラスです。 word 𝕍0 prop 𝕍0. thm `¬ Exi 𝕍0` ◀ O prf goal -| O p; br txt もう一つ例を作ってみます。 word 𝕍1 prop 𝕍1. thm `¬ Exi 𝕍1` ◀ O prf goal -| O p; thm `𝕍1 ⊂_ 𝕍0` ◀ O prf goal -| O p; thm `𝕍1 =_ \{ cls x | x {/}∈ ⋃ x \}` ◀ W. prf goal -| ⋃. p; goal -| W. h; subsection ZF txt 集合論の公理系についてはZF(Zermelo-Fraenkel)が有名です。 txt =.の\(\Longleftarrow\) は外延性公理と呼ばれ、ZFの公理の１つです。ZFの公理は、これと正則性公理以外は集合の存在を主張するものです。 br txt 以下のZFの4公理は、Matheliaではwordの定義から導出される定理とすることが多いです。 txt 空集合公理 prop/thm ax_∅ <- `Exi \{ cls x | ⊥ \}` ◀ ∅. prf ax_∅ -| ∅. p; txt 対集合公理 prop/thm ax_set2 <- `Exi \{ cls a | a = x or a = y \}` ◀ set2. prf ax_set2 -| set2. p; txt べき集合公理 prop/thm ax_℘ <- `Exi \{ cls A | A ⊂ X \}` ◀ ℘. prf ax_℘ -| ℘. p; txt 和集合公理 prop/thm ax_⋃ <- `Exi \{ cls x | [ ∃ X ∈ calX . x ∈ X ] \}` ◀ ⋃. prf ax_⋃ -| ⋃. p; 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; subsection 正則性公理(基礎の公理) txt 次の公理はvon Neumannによって導入されたものです。 prop ax0 !prop/thm ax0' ◀ W. ,, ax0 prf ax0' -| ax0 // W. p; ax0' -| W. ,, ax0 h; thm `𝕍1 =_ 𝕍` ◀ W. ,, ax0 prf goal / W. -| ax_set2 ,, ax0' p; goal -| W. ,, ax0 h; newpage section 集合の存在について② subsection 分出公理 txt 集合の部分クラスは集合である、ことが要請されます。 prop ax_s txt 宇宙も固有クラスになります(ax0からも導出されます)。 thm `¬ Exi 𝕍` --| ax_s prf goal -| ax_s[C_:=`𝕍0`] p; goal --| ax_s h; br txt ax_sはZFの分出公理と同値です。 prop ax_s' <- `∀ X Exi \{ cls x ∈ X | ?R^ (x) \}` thm ax_s' ◀ ax_s prf ax_s' --| ax_s v; !txt 上の方向（ax_s'をax_sから導く方向）は、ax_sの（全称的な）クラス変数C_へ具体的な項`\{ cls x ∈ X | ?R^ (x) \}`を代入するだけの通常の一階の代入で証明できます（`?R^`という述語変数自体への代入は不要です）。 thm ax_s ◀ ax_s' prf Le <- `Exi \{ cls x ∈ X | x ∈_ C_ \}` --| ax_s' s; ax_s --| Le v; ax_s ◀ ax_s' h; !txt 【2026-09-20 現状】この形（schema不使用・Leをprf内ローカル代入）で、3本のThm（`¬Exi 𝕍`・`ax_s' ◀ ax_s`・`ax_s ◀ ax_s'`）とも実機で通ります。`Le --| ax_s' s;`は、`\cls`本体の自由なクラス変数`C_`を「共有する1つのSkolem関数＋THFのλ」で扱う（`ax_s0/class_comprehension.php`・2026-09-17）ため、2026-09-16の「fail-closedガードで拒否される」という記述は解消しました。 txt ZFは一階論理であり、正確には分出公理は`?R^`をパラメータとする公理図式(無限個の公理の集まり)です。 br txt 空集合公理 はax_sからも導出されます。 thm ax_∅ ◀ ax_s prf ax_∅ --| ax_s v; subsection 置換公理 txt 置換公理は、関数的な性質による集合の像は集合である、ことを要請します。順序対は使いません。 abbr ！ abbr ∃！ txt `[ ！ y P ]` は「Pを満たすyは高々1つ」です。`∀ x \, [ ！ y \, x ??p^ y ]` は「??p^ は各xに高々1つのyを対応させる」ことを表します。 schema ax_r(??p^;x,y;C_,s,t,u,v) :=`∀ x \, [ ！ y \, x ??p^ y ] ⟹ ∀ X \, Exi \{ cls y | [ ∃ x ∈ X . x ??p^ y ] \}` txt ZFの置換公理は`??p^`をパラメータとする公理図式(無限個の公理の集まり)で、ax_rはその全体を表します。 txt schema の宣言は <code>schema 名(述語変数;その引数の変数;共有変数) :=`ψ`</code> の形です。ax_r では、??p^ が2項の述語変数、<code>x,y</code> はその1番目・2番目の引数の名前（代入する式の中で x が1番目、y が2番目を表します）、<code>C_,s,t,u,v</code> は代入する式の中に自由なまま残してよい変数（共有変数）です。共有変数に無い自由変数を代入する式に書くと、「代入式の自由な個体変数はラムダ引数か共有変数に含めてください」と拒否されます。 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 1段目の sos の <code>ax_r[??p^:=`x ∈_ C_ and y = x`]</code> は、ax_r の ??p^ に「x∈_C_ and y=x」を代入した実例です。代入した実例はこのように段の sos に直接書けます。最後の <code>ax_s ◀ ax_r h;</code> で「ax_r から導かれる」という形のThmにまとめます。代入する式に x と y の両方が現れる必要はありません（例えば <code>ax_r[??p^:=`y = ∅`]</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 相異なる2元 s, t を持つ集合 C に対し、??p^ に「s を u へ、t を v へ送る」関係を代入すると、C の像は \(\{u, v\}\) です。対集合の定義 set2. は使っていません。 thm ax_set2 ◀ ax_r ,, le_set2 prf ax_set2 --| ax_r[??p^:=`(x = s and y = u) or (x = t and y = v)`] ,, ax_r ,, le_set2 v; ax_set2 ◀ ax_r ,, le_set2 h; !txt 【書きかけ・09-29 に表示から外した】subsection 関数の像：`Exi {^}$_f $A` というのが置換公理です(？)
表示（保存しません）
保存にはMatheliaへのログインが要ります。