未ログイン ／
ログイン
← ファイル一覧
（保存にはログインが要ります）
0_tutorial/7.book
ヘッダ
行番号
title NBG author admin import /common/word_basis formel /common/default thmel /common/default
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;
表示（保存しません）
保存にはMatheliaへのログインが要ります。