はじめに

定理証明支援系の基礎を考えるにあたっての自分は重要論文だと思う

Per Martin-Löf(2006). 100 years of Zermelo's axiom of choice: what was the problem with it?

の野良訳です。あんまりよくわかってないので間違いあると思います。論文をGeminiに突っ込んで訳させて数式等を直しただけです。間違いあったら適宜直します。
数式が変換されてないところがありますが、後々直そうと思います（直し方がわからない）。

ツェルメロの選択公理の100年：何が問題だったのか？（100 years of Zermelo's axiom of choice: what was the problem with it?）

ペール・マルティン＝レーフ（Per Martin-Löf）

カントールは、1879年から1884年の5年間に「Mathematische Annalen」誌に発表された一連の6つの論文の中で集合論を構想した。1883年に出版されたこれらの論文の5番目において¹、彼は思考の法則（Denkgesetz）として、すべての集合は整列可能である、より正確には、いかなる明確に定義された集合も整列集合の形式に持ち込むことが常に可能であると述べた。さて、それを思考の法則と呼ぶことは、暗黙のうちにそれが自明であることを主張するものであったが、1890年代に彼は整列原理の証明を試みて失敗しているため²、どこかの時点でその主張を放棄したに違いない。

これに最初に成功したのはツェルメロであった³が、証明の前提条件として、彼は新しい原理を導入しなければならなかった。それは、1908年の彼の2つの論文において、それぞれ選択の原理（Prinzip der Auswahl）および選択公理（Axiom der Auswahl）と呼ばれるようになった⁴⁵。この主題に関する彼の最初の論文は1904年に出版され、わずか3ページから構成されており、ヒルベルトがツェルメロから受け取った手紙から抜粋したものである。その手紙は1904年9月24日付であり、抜粋の冒頭には、その証明が前週のエハルト・シュミットとの議論から生まれたことが記されている。これは、選択公理の登場と整列定理の証明を1904年9月と確実に断定できることを意味している。

ツェルメロの論文は簡潔であったが、数学的公理の妥当性、あるいは受容性に関して、おそらくこれまでに数学者の間で行われた中で最も活発な議論を引き起こした。1~2年のうちに、この議論への書面による寄稿が、ドイツではフェリックス・ベルンシュタイン、シェーンフリース、ハメル、ヘッセンベルク、ハウスドルフ、フランスではベール、ボレル、アダマール、ルベーグ、リシャール、ポアンカレ、イギリスではホブソン、ハーディ、ジュールダン、ラッセル、ハンガリーではユリウス・ケーニヒ、イタリアではペアノ、オランダではブラウワーによって出版された⁶。ツェルメロは、1908年の2番目の論文において、批判的であったこれらの寄稿の大部分に応答した。この2番目の論文には、整列定理の新しい証明も含まれているが、それは最初の証明よりも直感的でなく、明快さに欠けることは認めざるを得ない。また、選択公理の新しい定式化も含まれており、この定式化は以下の考察において決定的な役割を果たすことになる。

当初の強い反対にもかかわらず、ツェルメロの選択公理は、集合論だけでなく、例えば位相幾何学、代数学、関数解析など、数学のいくつかの分野の発展の初期段階で必要とされたため、次第に受け入れられるようになった。1930年代の終わりまでには、それは確固たる地位を築き、ツォルンの補題⁷という形で標準的な数学のカリキュラムの一部となった。

他方で、直観主義者たちは最初から選択公理を拒絶した。ベール、ボレル、ルベーグはみな、1905年に「集合論に関する5通の手紙（Cinq lettres sur la théorie des ensembles）」⁸という題名で出版された書簡集への寄稿の中で、それを批判していた。1907年のブラウワーの学位論文には、整列原理に関する節があり、そこではそれが冷淡なやり方で（「もちろん、これには全く動機がない」）扱われ、ボレルに従って⁹、選択公理からのツェルメロの証明¹⁰を軽視している。ブラウワーやハイティングの著作には、選択公理に関するこれ以上の議論は見当たらないようである。おそらく、それは彼らによって非構成的原理の代表例と見なされていたのであろう。

したがって、1967年という遅い時期にビショップが次のように述べたことは驚きであった。

構成的数学において選択関数は存在する。なぜなら、存在というまさにその意味によって選択が含意されているからである¹¹。

もっとも、彼自身が後の章で導入した用語法によれば、「選択関数」ではなく「選択操作」と言うべきであった。彼が念頭に置いていたのは、明らかに
$$(\forall i : I)(\exists x : S)A(i,x) \rightarrow (\exists f : I \rightarrow S)(\forall i : I)A(i,f(i))$$
そして、さらに一般的には、
$$(\forall i : I)(\exists x : S_i)A(i,x) \rightarrow (\exists f : \Pi_{i:I} S_i)(\forall i : I) A(i,f(i))$$
の真理性が、論理定数のブラウワー・ハイティング・コルモゴロフ解釈を思い出すと、ほぼ即座に自明になるということであった。これは、1930年代初頭にはすでに観察されていた可能性があったことを意味する。そして、構成的型理論において形式的な証明に変えられたのはこの直観的正当化（intuitive justification）であり、その証明は、解釈の中だけでなくシステム自体の中に証明オブジェクトを出現させた結果として定式化が可能になった、$\exists$-除去の強い規則を効果的に使用している。

1975年、ビショップによる構成的選択公理の擁護のすぐ後に、ディアコネスクは、トポス理論において排中律が選択公理から導かれることを証明した¹²。さて、トポス理論は、非可述的ではあるものの直観主義的な理論であるため、排中律の構成的な受け入れがたさから、これは表面的にはビショップの観察と相容れないものである。したがって、ブラウワー・ハイティング・コルモゴロフ解釈によって妥当とされる構成的選択公理が、一方でツェルメロの選択公理と、他方でトポス理論的選択公理とどのように関連しているかを調査する必要がある。

この目的のために、構成的型理論を分析の道具として用いて、ツェルメロの選択公理を単純に証明しようとしてみよう。この試みはもちろん失敗するはずであるが、その過程において、少なくともそれの何が本当に異論の余地があるのかを発見できるかもしれない。

では、ツェルメロの選択公理とは何であったか？ 1904年の最初の論文において、彼はそれに以下の定式化を与えた。

各部分集合 $M'$ に対して、それ自体に含まれ、$M'$ の『特権的な』要素と呼ばれる任意の一つの要素 $m_1'$ が割り当てられていると考える¹³。

ここで $M'$ は、与えられた集合 $M$ の、少なくとも一つの要素を含む任意の部分集合である。この定式化において驚くべきことは、構成的な観点から見て異論を唱えるべき点が何もないことである。

実際、特権的な要素 $m_1'$ は、部分集合 $M'$ が $M$ の少なくとも一つの要素を含むという存在命題 $(\exists x : M)M'(x)$ の証明の左射影（left projection）として取ることができる。これは、整列定理の証明において、その非構成的な要素が正確には何であるかを判断するために、証明の中身に入り込まなければならないことを意味する。

そうする代わりに、私は、ツェルメロが1908年の整列定理に関する2番目の論文で好んだ選択公理の定式化に目を向けることにする。

公理：それぞれが少なくとも一つの要素を含む、互いに素な部分 $A,B,C,\dots$ に分解される集合 $S$ は、考慮される各部分 $A,B,C,\dots$ と正確に一つの要素を共有する少なくとも一つの部分集合 $S_1$ を持つ¹⁴。

このように定式化されると、ツェルメロの選択公理は、ホワイトヘッドとラッセルが基数理論の発展に不可欠であることを見出した乗法公理と一致することが判明する¹⁵¹⁶。この選択公理の定式化の型理論的表現は、カントール的集合論の意味における基本的な集合が、型理論における外延的な集合（すなわち、同値関係を備えた集合）に対応し、外延的集合の部分集合が、当該の同値関係に関して外延的な命題関数として解釈されることを思い出せば、直接的である。

したがって、ツェルメロの1908年の選択公理の定式化のデータは、集合 $S$（これは同値関係 $=_{S}$

を備えている）と、$S$ 上の命題関数の族 $(A_i)_{i:I}$ であり、以下の特性を満たすものである。

(1) $x =_{S} y \rightarrow (A_i(x) \leftrightarrow A_i(y))$ （外延性 ; extensionality）

(2) $i =_{I} j \rightarrow (\forall x : S)(A_i(x) \leftrightarrow A_j(x))$ （添字への依存性の外延性 ; extensionality of the dependence on the index）

(3) $(\exists x : S)(A_i(x) \& A_j(x)) \rightarrow i =_{I} j$ （相互排他性 ; mutual exclusiveness）

(4) $(\forall x : S)(\exists i : I)A_i(x)$ （網羅性 ; exhaustiveness）

(5) $(\forall i : I)(\exists x : S)A_i(x)$ （非空性 ; nonemptiness）

これらのデータが与えられると、公理は、以下の条件を満たす $S$ 上の命題関数 $S_1$ の存在を保証する。
(6) $x =_S y \rightarrow (S_1(x) \leftrightarrow S_1(y))$ （外延性 ; extensionality）

(7) $\forall i : I)(\exists ! x : S)(A_i \cap S_1)(x)$ （選択の一意性 ; uniqueness of choice）

(1) - (5) から (6) と (7) を証明しようとする明白な方法は、(5) に型理論的（構成的、内包的）選択公理を適用して、
$$(\forall i : I)A_i(f(i))$$ となるような関数 $f : I \rightarrow S$ を得て、次に $S_1$ を次の方程式で定義することである。
$$S_1 = \lbrace f(j)\ | \ j : I\rbrace = \lbrace x \ | \ (\exists j : I)(f(j) =_S x) \rbrace$$

このように定義されると、$S_1$ は明らかに外延的であり、すなわち (6) を満たす。 (7) はどうであろうか？命題
$$(A_i \cap S_1)(f(i)) = A_i(f(i)) \& S_1(f(i))$$が明らかに真であるため、
$$(\forall i : I)(\exists x : S)(A_i \cap S_1)(x)$$ も真であり、これは一意性条件のみが証明として残されていることを意味する。このために、命題
$$(A_i \cap S_1)(x) = A_i(x) \& S_1(x)$$が真である、つまり、2つの命題
$$\lbrace \begin{align}
&A_i(x), \\
&S_1(x) = (\exists j : I)(f(j) =_S x)
\end{align}
$$
が両方とも真であると仮定する。$j:I$ が $f(j)=_S x$ を満たすとする。すると、$(\forall i : I)A_i(f(i))$ が真であるため、$A_j(f(j))$ も真である。したがって、$=_S$

に関する $A_j$ の外延性により、$A_j(x)$ は真であり、これは仮定された $A_i(x)$ の真理性とともに、部分集合の族 $(A_i)_{i:I}$ の相互排他性によって $i =_I j$ を与える。

この段階で、$f(i) =_S x$ であると結論付けるためには、選択関数 $f$ が外延的であること、すなわち、
$$i =_I j \rightarrow f(i) =_S f(j)$$

であることを知る必要がある。しかし、これは、型理論における強 $\exists$-除去の規則から導かれる構成的、あるいは内包的な選択公理によっては保証されない。

かくして、ツェルメロの選択公理を証明しようとする我々の試みは、予想通り失敗した。

一方で、我々はツェルメロの選択公理が外延的選択公理（これを ExtAC と呼ぶ）
$$(\forall i : I)(\exists x : S)A_i(x) \rightarrow (\exists f : I \rightarrow S)(\texttt{Ext}(f) \& (\forall i : I)A_i(f(i)))$$
から導かれることを証明することに成功した。ここで、

$$\texttt{Ext}(f) = (\forall i,j : I)(i ={I} j \rightarrow f(i) ={S} f(j))$$ である。これの唯一の難点は、内包的選択公理のような自明性を欠いていることであるが、もちろん、その帰結を調査することを妨げるものではない。

定理 I. 構成的型理論において、以下のものは同値である。
(i) 外延的選択公理。
(ii) ツェルメロの選択公理。
(iii) エピ射が分裂する。すなわち、すべての全射な外延的関数は外延的な右逆写像を持つ。
(iv) 任意の与えられた同値関係の同値類から一意の代表元を選ぶことができる。

これら4つの同値な言明のうち、(iii) はトポス理論的な選択公理であり、したがって、構成的に妥当な型理論的選択公理ではなく、ツェルメロの選択公理と同値である。

証明. 推論関係 (i)→(ii)→(iii)→(iv)→(i) をこの順序で証明する。

(i)→(ii). これは、まさに本定理の定式化以前の考察の結果である。
(ii)→(iii). $S$, $=_S$ と $I$, $=_I$ を2つの外延的集合とし、$f : S \rightarrow I$ をそれらの間の外延的で全射な写像とする。
定義により、次のように置く。
$$A_i = f^{-1}(i) = \lbrace x \ | \ f(x) =_I i \rbrace$$
すると、
(1) $x =_S y \rightarrow (A_i(x) \leftrightarrow A_i(y))$ は $f$ の仮定された外延性により成り立ち、
(2) $i =_I j \rightarrow (\forall x : S)(A_i(x) \leftrightarrow A_j(x))$ は、$i =_I j$ であれば $f(x) =_I i$ が $f(x) =_I j$ と同値であることから成り立つ。また、
(3) $(\exists x : S)(A_i(x) \ \& \ A_j(x)) \rightarrow i =_I j$ は $f(x) =_I i$ と $f(x) =_I j$ が共に $i =_I j$ を含意することから成り立ち、

(4) $(\forall x : S)(\exists i : I)A_i(x)$ は任意の $x : S$ に対して $A_{f(x)}(x)$ であることから成り立ち、
(5) $(\forall i : I)(\exists x : S)A_i(x)$ は関数 $f$ の仮定された全射性から成り立つ。したがって、ツェルメロの選択公理を適用して、以下の条件を満たす $S$ の部分集合 $S_1$ を得ることができる。
$$(\forall i : I)(\exists ! x : S)(A_i \cap S_1)(x)$$

型理論において利用可能な構成的、あるいは内包的な選択公理は、$(A_i \cap S_1)(g(i))$ となるような $g : I \rightarrow S$ を与える。すなわち、
$$(f(g(i)) =_I i) \ \& \ S_1(g(i))$$であり、したがって $g$ は $f$ の右逆写像であり、かつ
$$(A_i \cap S_1)(x) \rightarrow g(i) =_S x$$が成り立つ。
残るは $g$ が外延的であることを示すことだけである。$i,j : I$ と仮定する。すると、
$$(A_i \cap S_1)(g(i))$$ および
$$(A_j \cap S_1)(g(j))$$ が得られる。もし $i =_I j$ であれば、
$$(A_i \cap S_1)(g(j))$$ が、添字 $i$ に関する $A_i$ の外延的依存性によって成り立つ $A_i \cap S_1$ の一意性により、所望の $g(i) =_S g(j)$ を結論付けることができる。

(iii)→(iv). $I$ を同値関係 $=_I$ を備えた集合とする。すると、$I$ 上の恒等関数は、$I,\texttt{Id}_I$ から $I,=_I$ への外延的な全射である。なぜなら、いかなる関数も恒等関係に関して外延的だからである。エピ射が分裂すると仮定すると、
$$g(i) =_I i$$ および $$i =_I j \rightarrow \texttt{Id}_I(g(i),g(j))$$ となるような関数 $g : I \rightarrow I$ が存在すると結論付けることができる。これは、$g$ が与えられた同値関係 $=_I$ の各同値類から一意の代表元を選ぶという奇跡的な（miraculous）特性を持っていることを意味する。

(iv)→(i). $I,=_I$ と $S,=$ を、それぞれ同値関係を備えた2つの集合とし、

$(A_i)_{i:I}$ を $S$ の外延的な部分集合の族とする。
$$x =_S y \rightarrow (A_i(x) \leftrightarrow A_i(y))$$ これは添字 $i$ に外延的に依存する。
さらに、
$$(\forall i : I)(\exists x : S)A_i(x)$$ が保持されると仮定する。構成的型理論で有効な内包的選択公理により、
$$(\forall i :I)A_i(f(i))$$ となるような選択関数 $f : I \rightarrow S$ が存在すると結論付けることができる。もちろん、$=_I$ が添字集合 $I$ 上の恒等関係でない限り、この選択関数は外延的である必要はない。しかし、各同値類の一意の代表元を選ぶという奇跡的な原理を同値関係 $=_I$ に適用すると、
$$g(i) =_I i$$ および
$$i =_I j \rightarrow \texttt{Id}_I(g(i),g(j))$$ となるような関数 $g : I \rightarrow I$ を得る。すると $f \circ g : I \rightarrow S$ は外延的になる。

$$i =_I j \rightarrow \texttt{Id}I(g(i),g(j)) \rightarrow \underbrace{f(g(i))}{(f \circ g)(i)} =S \underbrace{f(g(j))}{(f \circ g)(j)}$$

さらに、$(\forall i : I)A_i(f(i))$ から次が導かれる。
$$(\forall i : I)A_{g(i)}(f(g(i)))$$
しかし、
$$g(i) =I i \rightarrow (\forall x : S)(A{g(i)}(x) \leftrightarrow A_i(x))$$
であるため、

$$(\forall i : I)A_i(\underbrace{f(g(i))}_{(f \circ g)(i)})$$ となる。したがっては外延的な選択関数となり、これは外延的選択公理が満たされることを意味する。

外延的選択公理がツェルメロの選択公理の正しい型理論的表現であるというもう一つの兆候は、構成的集合論から得られる。ピーター・アクゼル（Peter Aczel）は、ツェルメロ＝フレンケル集合論の言語を構成的型理論において解釈する方法を示した。この解釈は累積的階層の自然な構成的バージョンであり、その解釈の下でどのような集合論的原理が妥当となるかを調査した¹⁷。しかし、逆に、特定の集合論的公理を妥当にするために、構成的型理論にどのような原理を付け加えなければならないかを問うこともできる。特に、これはツェルメロが自身の集合論の公理化の一部とした選択公理の形式化されたバージョンについて問うことができる。その答えは以下の通りである。

定理 II. 構成的型理論が外延的選択公理によって強化されるとき、集合論的選択公理はアクゼル解釈の下で妥当となる。

証明. 集合論的選択公理は、任意の2つの反復的集合 $\alpha$ と $\beta$、および反復的集合間の任意の関係 $R$ について、次のように述べる。
$$(\forall x \in \alpha)(\exists y \in \beta)R(x,y) \rightarrow (\exists \phi : \alpha \rightarrow \beta)(\forall x \in \alpha)R(x,\phi(x))$$
この含意の左辺のアクゼル解釈は、
$$(\forall x : \bar{\alpha}(\exists y : \bar{\beta})R(\tilde{\alpha}(x),\tilde{\beta}(x))$$
であり、これは型理論的選択公理によって、
$$(\exists f : \bar{\alpha} \rightarrow \bar{\beta})(\forall x : \bar{\alpha}) R(\tilde{\alpha}(x),\tilde{\beta}(f(x)))$$
を与える。さて、定義により、
$$\phi = \lbrace \langle \tilde{\alpha}(x),\tilde{\beta}(f(x)) \rangle \ | \ x : \bar{\alpha} \rbrace$$ と置く。我々は、$\phi$ が構成的集合論の意味で $\alpha$ から $\beta$ への関数であることを証明する必要がある。すなわち、
$$\tilde{\alpha}(x) = \tilde{\alpha}(x') \rightarrow \tilde{\beta}(f(x)) = \tilde{\beta}(f(x'))$$ である。 $\bar{\alpha}$ と $\bar{\beta}$ 上にそれぞれ同値関係を、
$$(x =_{\bar{\alpha}} x') = (\tilde{\alpha}(x)=\tilde{\alpha}(x'))$$

および

$$(y =_{\bar{\beta}} y') = (\tilde{\beta}(y)=\tilde{\beta}(y'))$$

と定義する。型理論における外延的選択公理により、選択関数 $f : \bar{\alpha} \rightarrow \bar{\beta}$ は、これら2つの同値関係に関して外延的であるように取ることができ、

$$x ={\bar{\alpha}} x' \rightarrow f(x) ={\bar{\beta}} f(x')$$

これは、上記のように定義された $\phi$ が構成的集合論の意味での $\alpha$ から $\beta$ への関数であることを保証する。

系. 構成的型理論（一つの宇宙と W-演算を含む）が外延的選択公理によって強化されるとき、それは ZFC のすべてを解釈する。

証明. 我々はすでにアクゼルから、ZF が CZF + EM に等価であることを知っている¹⁸。したがって、ZFC はに等価である。しかし、グッドマンとマイヒルによって構成的集合論に移転されたディアコネスクの定理¹⁹によれば、構成的集合論の文脈において、排中律は選択公理から導かれる。したがって、CZF + AC を CTT + ExtAC において解釈すれば十分であり、これはまさに前定理によってアクゼル解釈が行うことである。

同じ結論に達する別の方法は、今与えた証明の最後の2つのステップの順序を入れ替え、代わりに ZFC = CZF + EM + AC は前定理によって CTT + EM + ExtAC において解釈可能であると論じ、次に、構成的型理論の文脈において排中律が外延的選択公理から導かれるという型理論版のディアコネスクの定理²⁰に訴えることである。いずれにせよ、最終的な結論は、ZFC が CTT + ExtAC において解釈可能であるということである。

ツェルメロの選択公理がツェルメロ＝フレンケル集合論ではなく構成的型理論の文脈で定式化されるとき、それは外延的選択公理 ExtAC として現れる。
$$(\forall i : I)(\exists x : S)A(i,x) \rightarrow (\exists f : I \rightarrow S)(\texttt{Ext}(f) \& \forall i : I)A(i,f(i)))$$ここで、
$$\texttt{Ext}(f) = (\forall i,j : I)(i =_I j \rightarrow f(i) =_S f(j))$$であり、そのとき何が問題であるかが明白になる。それは、「何もないところから何かを得ることはできない」という原理を破っているのである。たとえ関係 $A(i,x)$ がその2つの引数に関して外延的であったとしても、前件 $(\forall i : I)(\exists x : S)A(i,x)$ の真理性は、$(\forall i : I)A(i,f(i))$ を満たす選択関数 $f : I \rightarrow S$ の存在を保証するものの、選択関数の外延性、すなわち $\texttt{Ext}(f)$ の真理性を保証するには不十分である。

したがって、ツェルメロの選択公理の問題は、選択関数の存在ではなくその外延性であり、これは、すべての関数が定義によって外延的であるツェルメロ＝フレンケル集合論のような外延的な枠組みの中では目に見えないものである。

もし選択関数の外延性を保証したいのであれば、外延的選択公理の前件句を強化しなければならない。これを行う自然な方法は、ExtAC を一意選択の公理（あるいは「選択なし」の公理）である AC! に置き換えることである。
$$(\forall i:I)(\exists ! x : S)A(i,x) \rightarrow (\exists f : I \rightarrow S)(\texttt{Ext}(f) \& (\forall i : I)A(i,f(i)))$$これは内包的選択公理と同じくらい妥当である。実際、$(\forall i : I)(\exists ! x : S)A(i,x)$ が真であると仮定する。すると、内包的選択公理により、$(\forall i :I)A(i,f(i))$ を満たす選択関数 $f : I \rightarrow S$ が存在する。一意性条件のため、そのような関数 $f : I \rightarrow S$ は必然的に外延的である。なぜなら、$i,j : I$ は $i =_I j$ が真であるようなものと仮定せよ。すると、$A(i,f(i))$ と $A(j,f(j))$ は両方とも真である。したがって、最初の引数における $A(i,x)$ の外延性により、$A(i,f(j))$ も真である。一意性条件は今や $f(i) =_S f(j)$ であること、すなわち $f : I \rightarrow S$ が外延的であることを保証する。一意選択公理 AC! は、正当化を欠く ExtAC とは対照的に、外延的選択の妥当な形式と見なすことができる。

内包的選択公理と外延的選択公理を区別できないことが、可算な集合の可算な列の和集合が再び可算であることや、有理数のコーシー列として定義される実数がコーシー完備であることなどを証明する際に選択公理が必要であることを、ツェルメロの選択公理の正当化として受け入れさせてきた。ツェルメロ自身、彼が最初に選択公理を導入した短い論文の最後の方で次のように書いている。

この論理的原理は、より単純なものに還元することはできないが、数学的演繹において至る所で何ら疑いなく適用されている²¹。

ツェルメロがここで数学的証明における選択公理の至る所での、そしてしばしば無意識の的使用について書いたことは、反論の余地がないが、それは、存在除去の強い規則からほぼ即座に導かれる構成的、あるいは内包的なバージョンのそれに関するものである。

それは、選択関数の外延性を含む彼自身のバージョンの選択公理の正当化として受け取ることはできない。

トポス理論や構成的集合論のような外延的な基礎的枠組みの中で、その内包的な性格にもかかわらず、構成的選択公理の対応物を定式化することは完全に不可能ではないが、それは複雑になる。トポス理論には、十分な射影子（projectives）が存在するという公理がある。これは、すべての対象が射影子対象の全射像であることを意味する。また、構成的集合論において、アクゼルはすべての集合が基底（base）を持つという類似の公理を導入した²²。大まかに言えば、これはすべての集合が、それに対して選択公理が保持されるような集合の全射像であると言うことである。これらの公理の技術的な複雑さは、私の考えでは、構成的型理論のような内包的な基礎的枠組みを支持するものである。そこでは、ブラウワー・ハイティング・コルモゴロフ解釈においてなぜ選択公理が保持されるのかという直感的な議論が容易に形式化され、必要とされるいかなる外延的な概念も、マルティン・ホフマンの学位論文の題名「内包的型理論における外延的構成物（Extensional Constructs in Intensional Type Theory）」²³と一致するように構築することができる。外延性は、ただ（for free）で手に入るものではない。

最後に、ツェルメロの選択公理の最初の定式化から100周年の数週間前であるため、ツェルメロ＝フレンケル集合論と構成的型理論の両方の形式化において、それが果たしてきた決定的な役割を思い出すことは場違いではないかもしれない。集合論の場合、ツェルメロには整列定理の証明を形式的に厳密な基礎の上に置く必要があった。一方で、型理論の場合、論理演算の構成的解釈において選択公理を自明なものとした直観的に説得力のある議論があったが、その議論はそれまでのいかなる形式体系においても忠実に形式化することはできなかったのである。

G. Cantor, Über unendliche lineare Punktmannigfaltigkeiten. Nr. 5, Math. Annalen, Vol. 21, 1883, pp. 545-591. （再録：Gesammelte Abhandlungen, Edited by E. Zermelo, Springer-Verlag, Berlin, 1932, pp. 165-208. ） ↩
G. H. Moore, Zermelo's Axiom of Choice: Its Origins, Development, and Influence, Springer-Verlag, New York, 1982, p. 51. ↩
E. Zermelo, Beweis, daß jede Menge wohlgeordnet werden kann. (Aus einem an Herrn Hilbert gerichteten Briefe.), Math. Annalen, Vol. 59, pp. 514-516. ↩
E. Zermelo, Neuer Beweis für die Möglichkeit einer Wohlordnung, Math. Annalen, Vol. 65, 1908, pp. 107-128. ↩
E. Zermelo, Untersuchungen über die Grundlagen der Mengenlehre. I, Math. Annalen, Vol. 65, 1908, pp. 261-281. ↩
G. H. Moore, op. cit., pp. 92-137. ↩
M. Zorn, A remark on method in transfinite algebra, Bull. Amer. Math. Soc., Vol. 41, 1935, pp. 667-670. ↩
R. Baire, É. Borel, J. Hadamard and H. Lebesgue, Cinq lettres sur la théorie des ensembles, Bull. Soc. Math. France, Vol. 33, 1905, pp. 261-273. ↩
É. Borel, Quelques remarques sur les principes de la théorie des ensembles, Math. Annalen, Vol. 60, 1905, pp. 194-195. ↩
L. E. J. Brouwer. Over de grondslagen der wiskunde, Maas & van Suchtelen, Amsterdam, 1907. （英訳：Collected Works, Vol. 1, Edited by A. Heyting, North-Holland, Amsterdam, 1975, pp. 11-101. ） ↩
E. Bishop, Foundations of Constructive Analysis, McGraw-Hill, New York, 1967, p. 9. ↩
R. Diaconescu, Axiom of choice and complementation, Proc. Amer. Math. Soc., Vol. 51, 1975, pp. 176-178. ↩
E. Zermelo, op. cit., footnote 3, p. 514. ↩
E. Zermelo, op. cit., footnote 4, p. 110. ↩
A. N. Whitehead, On cardinal numbers, Amer. J. Math., Vol. 24, 1902, pp. 367-394. ↩
B. Russell, On some difficulties in the theory of transfinite numbers and order types, Proc. London Math. Soc., Ser. 2, Vol. 4, 1906, pp. 29-53. ↩
P. Aczel, The type theoretic interpretation of constructive set theory, Logic Colloquium '77, Edited by A. Macintyre, L. Pacholski and J. Paris, North-Holland, Amsterdam, 1978, pp. 55-66. ↩
P. Aczel, op. cit., p. 59. ↩
N. D. Goodman and J. Myhill, Choice implies excluded middle, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, Vol. 24, 1978, p. 461. ↩
S. Lacas and B. Werner, Which choices imply the Excluded Middle? About Diaconescu's trick in Type Theory, Unpublished, 1999, pp. 9-10. ↩
E. Zermelo, op. cit., footnote 3, p. 516. ↩
P. Aczel, The type theoretic interpretation of constructive set theory: choice principles, The L. E. J. Brouwer Centenary Symposium, Edited by A. S. Troelstra and D. van Dalen, North-Holland, Amsterdam, 1982, pp. 1-40. ↩
M. Hofmann, Extensional Constructs in Intensional Type Theory, Springer-Verlag, London, 1997. ↩