book集

section NBG
txt 集合論の公理系についてはNBG(von Neumann-Bernays-Gödel)も有名です。
txt Bernaysは2ソート論理で、Gödelはクラスの導入で、形式化をしました。？
txt defalut.formelの言語はそのどちらにも自然な翻訳があります。？
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;

0_tutorial_AI/7.book

`0_tutorial_AI/7.book`