book集

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

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の分出公理と同値です。ZFは一階論理なので、分出公理は ?R^ をパラメータとする公理図式（無限個の公理の集まり）で、schema で書きます。
schema ax_s'(?R^;x;C_) :=`∀ X Exi \{ cls x ∈ X | ?R^ (x) \}`
thm `∀ X Exi \{ cls x ∈ X | ?R^ (x) \}` ◀ ax_s
prf goal --| ax_s v;
thm ax_s ◀ ax_s'
prf ax_s --| ax_s'[?R^:=`x ∈_ C_`] v; ax_s ◀ ax_s' h;
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を対応させる」ことを表します。
txt ZFの置換公理は`??p^`をパラメータとする公理図式(無限個の公理の集まり)で、ax_rはその全体を表します。
txt schema の宣言は <code>schema 名(述語変数;その引数の変数;共有変数) :=&#96;ψ&#96;</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^:=&#96;x ∈_ C_ and y = x&#96;]</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^:=&#96;y = ∅&#96;]</code> で「X の各元を ∅ に送った像は集合」が示せます）。
br
txt 対集合公理もax_rから導かれます。まず、相異なる2元を持つ集合があることを、空集合とべき集合だけから示します（`℘ (℘ ∅)` は `∅` と `℘ ∅` を元に持ち、`∅ ∈ ℘ ∅` なので両者は異なります。等しいとすると `∅ ∈ ∅` となり ∅. に反するため）。
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)`] , le_set2 v;
    ax_set2 ◀ ax_r , le_set2 h;

!txt 【書きかけ・09-29 に表示から外した】subsection 関数の像：`Exi {^}$_f $A` というのが置換公理です(？)

newpage
section NBG
txt 集合論の公理系についてはNBG(von Neumann-Bernays-Gödel)も有名です。
txt Bernaysは2ソート論理で、Gödelはクラスの導入で、形式化をしました。default.formel の言語（s-Form と c-Form）は、そのどちらにも自然な翻訳があります。
br
txt NBGの公理は、補題として準備されます。まず2つ。
prop NBG-B2 <- `∃_ X_ ∀ x \, (x ∈_ X_ ⟺ x ∈_ A_ and x ∈_ B_)`
thm `∀ x \, (x ∈_ \{ cls y | y ∈_ A_ and y ∈_ B_ \} ⇔ (x ∈_ A_ and x ∈_ B_))` ◀ O
prf `∀ x \, (x ∈_ \{ cls y | y ∈_ A_ and y ∈_ B_ \} ⇔ (x ∈_ A_ and x ∈_ B_))` --| O v;

prop NBG-B3 <- `∃_ X_ ∀ x \, (x ∈_ X_ ⟺ x {/}∈_ A_)`
thm `∀ x \, (x ∈_ \{ cls y | y {/}∈_ A_ \} ⇔ x {/}∈_ A_)` ◀ O
prf `∀ x \, (x ∈_ \{ cls y | y {/}∈_ A_ \} ⇔ x {/}∈_ A_)` --| O v;

section 集合のwordを含んだ公理
word ∈
!txt 順序対（B1・B4・B5 で使う）
word \pr
abbr pr
prop NBG-B1 <- `∀ x \, ∀ y \, (\< pr x ; y \> ∈_ \{ cls w | ∃ u \, ∃ v \, (w = \< pr u ; v \> and u ∈ v) \} ⇔ ∃ u \, ∃ v \, (\< pr x ; y \> = \< pr u ; v \> and u ∈ v))`
thm NBG-B1 ◀ O
prf NBG-B1 -| O p;
br
prop NBG-B4 <- `∃_ X_ ∀ x \, (x ∈_ X_ ⟺ ∃ z \, (\< pr x ; z \> ∈_ A_))`
thm `∀ x \, (x ∈_ \{ cls y | ∃ z \, (\< pr y ; z \> ∈_ A_) \} ⇔ ∃ z \, (\< pr x ; z \> ∈_ A_))` ◀ O
prf `∀ x \, (x ∈_ \{ cls y | ∃ z \, (\< pr y ; z \> ∈_ A_) \} ⇔ ∃ z \, (\< pr x ; z \> ∈_ A_))` --| O v;

misc/7.book

`misc/7.book`