正則性公理
正則性公理(せいそくせいこうり、テンプレート:Lang-en-short)は、別名「基礎の公理」(きそのこうり、テンプレート:Lang-en-short) とも呼ばれ、ZF公理系を構成する公理の一つで、1925年にジョン・フォン・ノイマンによって導入された。選択公理と同様、様々な同値な命題が存在する。
定義
以下の3つの主張はいずれもZF公理系の他の公理の元で同値であり、どれを正則性公理として採用しても差し支えない[1]。
- テンプレート:Math に対して、テンプレート:Math
- テンプレート:Mathについて、テンプレート:Math が テンプレート:Mvar 上整礎関係
- テンプレート:Math
ここで、テンプレート:Mvar は集合論の宇宙を指し、テンプレート:Mvar は整礎的集合全体のクラス(フォン・ノイマン宇宙)を指す。
ZF公理系内に限って話を進める。各順序数 テンプレート:Mvar に対して テンプレート:Math を次のように定義する( は冪集合)。
- テンプレート:Mvar が極限順序数のとき、
クラス テンプレート:Mvar はこれらを全て集めたものとして定義される。
ZF公理系の他の公理から得られる種々の集合演算(対集合、和集合、冪集合) の結果としての集合は常に テンプレート:Mvar 内に含まれる。すなわち テンプレート:Math の仮定は、全ての集合を テンプレート:Math に通常の集合演算を施すことによって得られるものだけに制限することを主張している。したがって、例えばテンプレート:Mathのような集合やテンプレート:Mathかつテンプレート:Mathなる集合は正則性の公理の下では集合にはなり得ない。
性質
テンプレート:Mvar の定義より、テンプレート:Math のとき、テンプレート:Math を満たす最小の順序数 テンプレート:Mvar は後続順序数になる。実際、テンプレート:Mvar を極限順序数として テンプレート:Math 及び テンプレート:Math が成り立っているとすると、
となって矛盾する。
そこで、集合 テンプレート:Mvar のランクを次のように定義する。
テンプレート:Math のとき、テンプレート:Math を満たす最小の テンプレート:Mvar を集合 テンプレート:Mvar のランクといい、テンプレート:Math で表す。
よって、テンプレート:Math ならば
が成り立ち、テンプレート:Math かつ テンプレート:Math となる。また、このランクの概念を用いて テンプレート:Math は次のように特徴付けられる。
及び、
ランクを計算するときに次の補題を使う。
のとき、
かつ
とすると
ならば だから