置換公理

${\displaystyle P}$ をクラス ${\displaystyle A}$ についての二項関係（述語）とおく。${\displaystyle A}$ の任意の元 ${\displaystyle x}$ について、${\displaystyle y}$ がただ一つ存在し、${\displaystyle P\left(x,\,y\right)}$ を満たす。

${\displaystyle \forall x\left[x\in A\Rightarrow \exists y\left[P\left(x,\,y\right)\right]\right]}$

${\displaystyle \forall x\left[x\in A\Rightarrow \forall y\ \forall z\left[\left[P\left(x,\,y\right)\land P\left(x,\,z\right)\right]\Rightarrow y=z\right]\right]}$

構成可能な関数 ${\displaystyle F_{P}}$ を下記のように定義する。

${\displaystyle F_{P}\left(x\right)=y\Leftrightarrow P\left(x,\,y\right)}$

${\displaystyle B}$ を下記のように定義する。

${\displaystyle y\in B\Leftrightarrow \exists x\left[x\in A\land F_{P}\left(x\right)=y\right]}$

また ${\displaystyle B=\left\{F_{P}\left(x\right)|\,x\in A\right\}}$ であり、${\displaystyle B}$ は ${\displaystyle A}$ 上の ${\displaystyle F_{P}}$ による値域と呼び、${\displaystyle F_{P}\left[A\right]}$ と書く。

置換公理の主張は、ここで ${\displaystyle F_{P}}$ が定義可能で ${\displaystyle A}$ が集合ならば、${\displaystyle B}$ もまた集合であることである。

より厳密には、すべての式を一階述語論理によって量化することはできないので、メタ変項（英語版）として式${\displaystyle \phi }$、及びその変数${\displaystyle w_{1},\dotsc ,w_{n},A,x,y}$を用いて、

${\displaystyle {\begin{aligned}\forall w_{1},\ldots ,w_{n}\,\forall A\,([\forall x\in A&\,\exists !y\,\phi (x,y,w_{1},\ldots ,w_{n},A)]\ \Longrightarrow \ \exists B\,\forall y\,[y\in B\Leftrightarrow \exists x\in A\,\phi (x,y,w_{1},\ldots ,w_{n},A)])\end{aligned}}}$

とする。${\displaystyle \exists$ !} はただ一つ存在することを表す。

Summarize Timeline Fact Check

置換公理は、通常の数学におけるほとんどの定理の証明に必ずしも必要とされない。実際、ツェルメロ集合論（Z）ではすでに二階算術（英語版）と多くの有限型の型理論を扱うことができ、数学の大部分を定式化するには十分である。置換公理は今日の集合論の標準的な公理であるものの、型理論のシステムやトポス理論における基礎的システムでは省略されることも多い。

多かれ少なかれこの公理は、ZFで証明可能な定理（たとえば集合の存在証明）や証明論的な無矛盾性の強さの点において、Zと比べて劇的にZFを強固にする。以下に重要な例を示す。

• フォン・ノイマンの現代的な定義を使うと、ω より大きい任意の極限順序数の存在証明に置換公理が必要である。順序数 ω·2 = ω + ω はそのような順序数の最初の例である。無限公理は無限集合 ω = {0, 1, 2, ...} の存在を主張する。ω·2 を数列 {ω, ω + 1, ω + 2,...} の合併として定義したいとする。しかし、そのような順序数のクラスは集合にはならない（例えば、すべての順序数のクラスは集合ではない）。置換公理を用いると、ω における有限の数 n それぞれを、対応する ω + n に置き換えることができ、そうすることでこのクラスを集合とみなすことができる。補足として、置換公理に頼らず ω·2 と同型な整列集合を簡単に構築できることに注意（単に二つの ω に対して、一方が他方より大きくなるように直和をとればよい）。しかし、内包によって完全に順序付けられていないため、これは順序数ではない。
• 大きな順序数ほど直接的には置換公理を使わなくなる。例えば、最小の非可算順序数 ω₁ は、以下のように構築できる。分出公理と冪集合公理より、可算整列集合は ${\displaystyle P({\mathbb {N} }\times {\mathbb {N} })}$ の部分集合として存在する（A 上の関係は ${\displaystyle A\times A}$ の部分集合であるため、冪集合 ${\displaystyle P(A\times A)}$の元となる。それゆえ、関係の集合は ${\displaystyle P(A\times A)}$の部分集合となる）。各整列集合をその順序数で置き換えると可算順序数の集合 ω₁ となり、これは非可算であることが示せる。この構築法では置換公理を2回使っている。まず各整列集合に順序数を割り当てるところで用い、そして整列集合をその順序数で置き換えるところで使っている。これはハルトークス数の結果の特別な場合であり、一般の場合も同様に証明できる。
• 上記のように、順序数をすべての整列集合へ割り当てるのにも置換公理が必要である。同様に、基数を各集合に割り当てるフォン・ノイマンの割り当てには置換公理と選択公理が必要である。
• ${\displaystyle A^{n}=A^{n-1}\times A}$ として再帰的に定義される組の集合を考える。大きな ${\displaystyle A}$ に対して、集合 ${\displaystyle \{A^{n}\mid n\in {\mathbb {N} }\}}$ は、冪集合公理と選択公理を含み置換公理を含まない集合論において、その存在を証明できないほど高い階数を持つ。
• 同様に、ハーベイ・フリードマン（英語版）はボレル集合の決定性（英語版）を示すのに置換公理が必要であることを示した。
• 集合 V_ω·2 を Z のモデルとすると、その存在を ZF で証明できるため、ZF＋置換公理で Z の無矛盾性を証明できる。基数 ${\displaystyle \aleph _{\omega }}$ はその存在を ZF で証明できるが Z で証明できない最小のものである。補足として、これらの理論それぞれが理論自身の無矛盾性を「表現する」文を含むが、理論が無矛盾である限り、理論の無矛盾性を理論自身の中では証明できないことがゲーデルの第二不完全性定理によって示されていることに注意。この結果はしばしば「どの理論も、理論が無矛盾である限り、自身の無矛盾性を証明できない」と大まかに表現される。

Summarize Timeline Top Qs Fact Check

集まりの公理図式（英: axiom schema of collection）は置換公理と密接に関連し、かつよく混同される。

ZF公理系では、置換公理図式を集まりの公理図式に書き換えても同値である。集まりの公理は冪集合公理やそのZFの構成可能な部分が不要である分、置換公理よりも強いが、排中律がないIZFの枠組みにおいては弱い。

置換公理は関数の像が集合であると読めるが、集まりの公理は関係の像に関するもので、単に関係の像の上位クラスに集合であるものがあることを主張するのみである。

言い換えれば、集合 ${\displaystyle B}$ は最小性を要せず、 ${\displaystyle \phi }$ における唯一性も必要ない。 つまり、 ${\displaystyle \phi }$ で定義される関係が関数である必要はない（${\displaystyle x\in A}$ の中には、 ${\displaystyle B}$ に属する複数の ${\displaystyle y}$ と対応するものがありうる）この場合、存在を主張する像集合 ${\displaystyle B}$ には、もとの集合の元 ${\displaystyle x}$ それぞれに対して少なくとも1つ（必ず1つとは限らない）対応する ${\displaystyle y}$ が含まれる。

${\displaystyle \phi }$ の自由変数が ${\displaystyle w_{1},\dotsc ,w_{n},x,y}$ 上にあるとする。ただし、 ${\displaystyle A}$ も ${\displaystyle B}$ も ${\displaystyle \phi }$ の自由変数ではない。すると集まりの公理は以下のようになる。

${\displaystyle \forall w_{1},\ldots ,w_{n}\,[(\forall x\,\exists \,y\phi (x,y,w_{1},\ldots ,w_{n}))\Rightarrow \forall A\,\exists B\,\forall x\in A\,\exists y\in B\,\phi (x,y,w_{1},\ldots ,w_{n})]}$

集まりの公理は上記の述語に関する制限なしで表現されることもあり（${\displaystyle B}$ 以外に ${\displaystyle \phi }$ に自由変数がない）、${\displaystyle \phi }$ は以下のようになる：

${\displaystyle \forall w_{1},\ldots ,w_{n}\,\forall A\,\exists B\,\forall x\in A\,[\exists y\phi (x,y,w_{1},\ldots ,w_{n})\Rightarrow \exists y\in B\,\phi (x,y,w_{1},\ldots ,w_{n})]}$

この場合、${\displaystyle \phi }$ で他の集合と対応付けられない ${\displaystyle A}$ の元 ${\displaystyle x}$ が存在しうる。しかし、集まりの公理は前述の通り 「${\displaystyle A}$ の元 ${\displaystyle x}$ が少なくとも1つの集合 ${\displaystyle y}$ と対応付けられれば、像集合 ${\displaystyle B}$ は少なくとも1つそのような ${\displaystyle y}$ を含む」ことを要請する。結果として、集まりの公理は境界性の公理図式（axiom schema of boundedness）とも呼ばれる。

ZFCのほかの公理図式である分出公理は置換公理と空集合の公理から導かれる。分出公理が集合論の言語における各論理式 ${\displaystyle \theta }$ に対して以下を含むことを思い出そう（${\displaystyle B}$ は自由変数でない）。

${\displaystyle \forall A\,\exists B\,\forall C\,(C\in B\Leftrightarrow [C\in A\land \theta (C)])}$

証明は以下のとおりである。まず ${\displaystyle B}$ に関して言及しない論理式 ${\displaystyle \theta (C)}$ と集合 ${\displaystyle A}$ から始める。もし ${\displaystyle \theta (E)}$ を満たす ${\displaystyle A}$ の元 ${\displaystyle E}$ がなければ、分出公理に必要な集合 ${\displaystyle B}$ は空集合である。そうでない場合、 ${\displaystyle \theta (E)}$ が成り立つ ${\displaystyle A}$ の元 ${\displaystyle E}$ を選ぶ。次にクラス関数 ${\displaystyle F}$ を以下のように定義する：任意の元 ${\displaystyle D}$ に対して ${\displaystyle \theta (D)}$ が成り立つ場合は ${\displaystyle F(D)=D}$ 、成り立たない場合は ${\displaystyle F(D)=E}$。すると ${\displaystyle F}$ による ${\displaystyle A}$ の像、すなわち集合 ${\displaystyle B=F''A:=\{F(x):x\in A\}=A\cap \{x:\theta (x)\}}$ が存在し（置換公理による）、まさしく分出公理に必要な集合 ${\displaystyle B}$ となる。

この結果から、ZFCが公理無限個の図式一つで公理化可能であることがわかる。そのような公理無限個の図式が少なくとも１つは必要であるので（ZFCは有限公理化可能でない）、必要であれば置換公理はZFCにおける公理無限個の図式で唯一のものにできることがわかる。分出公理は独立でないため、ZF公理系の現代的な定義からはよく省略される。

しかし、歴史的経緯によるZFCの一要素としての扱いや、他の集合論との比較において、 分出公理は重要である。置換公理を含まない集合論の定式化では、そのモデルに十分に多くの集合の集まりが含まれることを保証するため、よく分出公理が用いられる。集合論のモデルの研究において、フォン・ノイマン階層におけるモデル ${\displaystyle V_{\delta }}$ のように、置換公理を含まないZFCのモデルを考えると有用であることがある。

上記の証明では、${\displaystyle A}$ が空集合でないなら元を含むという仮定において、排中律を用いている（直観論理において、集合が元を含まなければその集合は「空集合」であり、「空集合でない」というのは、この形式的な否定である。これは「元を含まない」という命題よりも弱い）。 分出公理は直観集合論に含められる。