公理的集合論でも比較的後に追加された公理、それが正則性公理なのだ。基礎の公理とも言うのだ
正則性公理
空でない集合 $X$ に対して $\exist a\in X\st\forall x\in X, x\notin a$ なのだ
この形になじみがないけものも多いことと思うのだ。「$\in$ を(狭義半)順序としたときの極小元が存在する」という言い方もできて、順序を知ってればわかりやすいのだ
でも、多くのけものが知っているのは以下の主張のはずなのだ。よく使われると思うんだけど、これはどちらかというと系なのだ
系
$x_0\ni x_1\ni x_2\ni\cdots$ となるような集合列 $(x_n)_{n\in\N}$ は存在しないのだ
証明
$x_0\ni x_1\ni x_2\ni\cdots$ となるような集合列 $(x_n)_{n\in\N}$ が存在したとして、上の正則性公理から矛盾を導けばいいのだ
$X=\set{x_0,x_1,x_2,\ldots}$ とすれば、$\forall x_n\in X$ に対して $x_{n+1}\in x_n$ だから正則性公理に矛盾するのだ
さらにかみ砕いて「包含関係にループがあったら矛盾」と言うこともあるのだ。$x\in x$ とか、$n\in m\in n$ とかがそれで、見方を変えれば $n\ni m\ni n\ni m\ni n\ni\cdots$ などとなるからなのだ
従属選択公理による同値性
一応、従属選択公理を仮定すると系と正則性公理が同値になるのだ:
従属選択公理
空でない集合 $X$ と $R\subset X\times X$ に対して「$\forall x\in X,\exist y\in X\st\ang{x,y}\in R$」が成り立つとき、$\exist\par{x_n}_{n\in\N}\st\forall n\in\N, \ang{x_n,x_{n+1}}\in R$ なのだ
従属選択公理は選択公理より少し弱い公理なのだ。選択公理を大体仮定したと思えばいいのだ。証明は本当にそのままだから「そうだなー」って思ってくれればいいのだ
命題
従属選択公理 $\land$ 系 $\Rarr$ 正則性公理
証明
正則性公理を満たさない集合、すなわち $\forall x\in X, \exist y\in X\st x\ni y$ となるような $X$ があったとするのだ
このとき、$R\coloneqq\set{\ang{x,y}\in X\times X\mid x\ni y}$ に対して従属選択公理をつかえば $\exist(x_n)_{n\in\N}\st\forall n\in\N, x_n\ni x_{n+1}$ なのだ
この $(x_n)_{n\in\N}$ は系を満たさない列そのものなのだ
ほんの少しだけうれしい公理なのだ
他の公理が基本的である程度直感的、さらにないと困るのに対して、正則性公理はあんまり劇的な公理じゃないのだ
だから正則性公理を本質的に使った命題や定理というのがそんなに思いつかないのだ
その代わり、証明が楽になる例というのはたくさん存在するのだ
順序対 $\ang{a,b}$ の表現が $\set{\set{a},\set{a,b}}$ から $\set{a,\set{a,b}}$ のように簡単になるとか、順序数の定義が簡単になるとか、そういうものばっかりなどちらかというと技術的な公理なのだ
このように公理を定めても、証明できるものの幅が狭まったりしないこともわかっているのだ。正則性公理を認めなくても構成的集合、というアライㄜん達が普通に構成できる集合を扱う限り正則性公理を満たす集合しか扱わなくていいことがわかっているからなのだ
具体的には空集合、和集合の公理や置換公理などをつかって作り出した集合は正則性公理を満たすことがわかっているんだけど、置換公理の証明などが思いつかなくてちょっと長くなりそうなので今のところパスなのだ。そのうち追加するかもしれないのだ