構成的集合論

同義語：constructive set theory

概要

構成的集合論（constructive set theory）とは、排中律を仮定しない直観主義論理の上で展開する集合論で、冪集合と任意の論理式による分出をもつ IZF と、分出を有界な論理式に限り冪集合の代わりに fullness を置く CZF が代表的である。直観主義論理の上では、正則性公理も選択公理も排中律を導くので、正則性公理の代わりに $\in$ についての帰納法を置き、選択公理は仮定しない。fullness からは関数全体の集合が得られ、排中律を加えると冪集合も得られるので、CZF に排中律を加えた体系は ZF と同じ定理をもつ。IZF・CZF の公理はすべて ZF の定理である。

$$\newcommand{C}[0]{\mathbb{C}} \newcommand{div}[0]{\mathbin{÷}} \newcommand{N}[0]{\mathbb{N}} \newcommand{Q}[0]{\mathbb{Q}} \newcommand{R}[0]{\mathbb{R}} \newcommand{Z}[0]{\mathbb{Z}} $$

前提知識: ZFC公理系, 直観主義論理, 排中律, 構成的数学

構成的集合論（constructive set theory）は、排中律を仮定しない直観主義論理の上で展開する集合論である。言語はZFC公理系と同じく所属関係 $\in$ だけをもつが、公理の選び方が変わる。ZF の公理のいくつかは、直観主義論理の上で仮定すると排中律の例を導いてしまうからである。代表的な体系は二つある。冪集合公理と任意の論理式による分出をもつ IZF（intuitionistic Zermelo–Fraenkel）と、分出を有界な論理式に限り、冪集合の代わりに弱い公理を置く CZF（constructive Zermelo–Fraenkel）である（Cro24 §1.2、Shu18 §2, p. 8）。
この記事では二つの体系を定義し、正則性公理（基礎の公理）と選択公理がそれぞれ排中律を導くこと、そのために正則性公理を $\in$ についての帰納法に替えることを証明する。さらに、冪集合の代わりの公理（fullness）から関数の集合が得られること、CZF に排中律を加えると ZF と同じ定理をもつことを示す。

定義

直観主義論理では、「空でない」（$\lnot\forall y\ y\notin x$）と「元をもつ」（$\exists y\ y\in x$）は一般に同値でない。後者を満たす集合を inhabited な集合という。以下、$\Delta_0$ 論理式は量化がすべて有界（$\exists u\in v$、$\forall u\in v$ の形）な論理式を表す（内部モデルの定義「有界な論理式」）。

構成的集合論の公理

直観主義述語論理（等号を含む）の上で、次の原理を考える（Cro24 の補遺「Axioms of CZF and IZF」、Shu18 §2, pp. 5–7）。分出・収集・帰納法は論理式についての図式で、論理式はパラメータを含んでよい。

  1. 外延性：同じ元をもつ集合は等しい。
  2. 空集合：元をもたない集合 $\emptyset$ がある。
  3. 対：任意の $x,y$ について、$z\in\{x,y\}\leftrightarrow(z=x\lor z=y)$ を満たす集合 $\{x,y\}$ がある。
  4. 合併：任意の $a$ について、$\bigcup a$ がある。
  5. 無限：$\emptyset\in\omega$ かつ $x\in\omega\to x\cup\{x\}\in\omega$ を満たす集合 $\omega$ がある。
  6. 分出：任意の論理式 $\varphi$ と集合 $a$ について $\{x\in a\mid\varphi(x)\}$ がある。$\varphi$ を $\Delta_0$ 論理式に限ったものを $\Delta_0$ 分出という。
  7. 収集：$\forall x\in a\,\exists y\,\varphi(x,y)$ なら、集合 $b$ で $\forall x\in a\,\exists y\in b\,\varphi(x,y)$ を満たすものがある。さらに $\forall y\in b\,\exists x\in a\,\varphi(x,y)$ も満たす $b$ がとれるという形を 強い収集という。
  8. 冪集合：任意の $a$ について $\mathcal P(a)=\{x\mid x\subseteq a\}$ がある。
  9. $\in$ についての帰納法：$\forall a\,\bigl(\forall y\in a\,\varphi(y)\to\varphi(a)\bigr)\to\forall a\,\varphi(a)$。

$a$ から $b$ への関係 $r\subseteq a\times b$ が 全域的であるとは、各 $x\in a$ に対し $\langle x,y\rangle\in r$ となる $y\in b$ があることをいう。集合 $m$ が $a,b$ について full であるとは、$m$ の元がすべて $a$ から $b$ への全域的な関係で、$a$ から $b$ への任意の全域的な関係 $r$ に対し、$g\subseteq r$ となる $g\in m$ があることをいう。任意の $a,b$ について full な集合があるという公理を fullness という。

IZF と CZF

(a) IZF は、1〜9（分出は任意の論理式について、収集は 7 の弱い形）からなる体系である（Cro24 の補遺、Shu18 p. 8）。
(b) CZF は、1〜5、$\Delta_0$ 分出、強い収集、fullness、9 からなる体系である（Shu18 p. 8）。

Cro24 の補遺は CZF を fullness の代わりに「部分集合の収集」の図式で述べ、ほかの公理のもとで両者が同値であることを Aczel（1978）に帰している（この記事では証明しない）。CZF は冪集合公理も任意の論理式による分出ももたない。どちらも、作ろうとしている集合を含むすべての集合を量化する論理式を使って集合を作ること（非可述的な定義）を許す原理だからである（Cro24 §1.3）。
古典論理のもとでは、ZF は 1〜9 をすべて証明する（強い収集を含む。Shu18 p. 6 は ZF のほかの公理から収集が証明できることを述べる）。fullness は冪集合と $\Delta_0$ 分出から出る（下の prop-cst-fullness）。したがって IZF・CZF の公理はすべて ZF の定理である。

例：直観主義論理の上での小さな集合

$0:=\emptyset$、$1:=\{0\}$、$2:=\{0,1\}$ とおく。対の公理により $x\in2$ は $x=0\lor x=1$ と同値であり、$0\in1$ かつ $0\notin0$ から $0\neq1$ である。したがって $2$ の元どうしが等しいかは決定できる（$x,y\in2$ なら $x=y\lor x\neq y$）。
一方、論理式 $\varphi$ に対して分出で作った $\{x\in1\mid\varphi\}$ は $1$ の部分集合だが、それが $0$ に等しいか $1$ に等しいかは $\varphi$ の真偽で決まり、一般には決められない。$1$ の部分集合が $0$ と $1$ だけであることは、$\varphi\lor\lnot\varphi$ と同じ強さの主張である。構成的集合論で $\mathcal P(1)$ が古典論理のときより豊かになるのはこのためである。

正則性公理と排中律

ZF の基礎の公理は「inhabited な集合は $\in$ について極小な元をもつ」（正則性公理、正則性公理）という形で述べられる。直観主義論理の上では、この形は排中律を導く。

正則性公理は排中律を導く

外延性・空集合・対・$\Delta_0$ 分出のもとで、正則性公理
$$ \forall a\,\bigl(\exists y\,(y\in a)\to\exists y\in a\ \forall z\in y\ z\notin a\bigr) $$
を仮定すると、任意の $\Delta_0$ 論理式 $\varphi$ について $\varphi\lor\lnot\varphi$ が証明できる。分出を任意の論理式に許せば、任意の論理式 $\varphi$ について同じことが成り立つ。

$\varphi$ を論理式とし（前半では $\Delta_0$）、$y$ は $\varphi$ に自由に現れないとする。分出により
$$ A:=\{y\in2\mid y=1\lor(y=0\land\varphi)\} $$
をとる。$y\in2$ と $y=1\lor(y=0\land\varphi)$ は $\varphi$ が $\Delta_0$ なら $\Delta_0$ 論理式なので、前半では $\Delta_0$ 分出で足りる。$1\in A$ なので $A$ は inhabited であり、正則性公理により $A$ の元 $m$ で、$m$ のどの元も $A$ に属さないものがある。$m\in A$ なので $m=1\lor(m=0\land\varphi)$ であり、この選言で場合を分ける。

  • $m=0\land\varphi$ の場合：$\varphi$ が成り立つ。
  • $m=1$ の場合：$\lnot\varphi$ を示す。$\varphi$ を仮定すると、$0=0\land\varphi$ から $0\in A$ である。一方 $0\in1=m$ なので、$m$ の選び方から $0\notin A$ であり、矛盾する。よって $\lnot\varphi$ である。
    どちらの場合も $\varphi\lor\lnot\varphi$ が成り立つ。場合分けに使ったのは、すでに得られている選言だけである。$\square$

この議論は Cro24 の補遺「Set-theoretic Principles Incompatible with Intuitionistic Logic」と同じ筋である。正則性公理は「極小な元が存在する」と存在を主張するので、極小元が $0$ か $1$ かを見れば $\varphi$ の真偽が分かってしまう。構成的集合論では、正則性公理の代わりに、古典論理のもとで同値な $\in$ についての帰納法 9 を置く。直観主義論理のもとで帰納法から言えるのは、次の弱い形である。

$\in$ についての帰納法と極小元

直観主義論理の上で $\in$ についての帰納法 9 を仮定する。
(1) 集合 $a$ が $\in$ について極小な元をもたない（$\lnot\exists y\in a\ \forall z\in y\ z\notin a$）なら、$a$ は元をもたない。
(2) したがって、inhabited な集合 $a$ について $\lnot\lnot\exists y\in a\ \forall z\in y\ z\notin a$ が成り立つ。排中律を加えれば正則性公理が成り立つ。

  1. 論理式 $\psi(y):=y\notin a$ に帰納法を当てる。$\forall z\in y\ \psi(z)$、すなわち $y$ のどの元も $a$ に属さないとする。ここで $y\in a$ と仮定すると、$y$ は $a$ の極小な元になり、仮定に反する。よって $y\notin a$、すなわち $\psi(y)$ である。帰納法により、すべての $y$ について $y\notin a$ である。
  2. $a$ が inhabited だとし、$a$ が極小な元をもたないと仮定すると、(1) により $a$ は元をもたず、矛盾する。よって $\lnot\lnot\exists y\in a\,\forall z\in y\,z\notin a$ が成り立つ。排中律のもとでは $\lnot\lnot$ を外せる。$\square$

選択公理と排中律

選択公理が排中律を導くこと（Diaconescu の定理）は、排中律の定理「Diaconescu の定理」で証明されている。そこでの選択公理は「inhabited な集合からなる集合 $a$ に対し、各 $x\in a$ で $f(x)\in x$ となる $a$ 上の関数 $f$ がある」という形で、仮定は外延性・空集合・対・任意の論理式による分出である。元の論文はトポスの言葉で、部分対象が補元をもつことを示している（Dia75 Corollary, p. 178）。

CZF と IZF での選択公理
  1. IZF に選択公理を加えると、任意の論理式について排中律が成り立つ。
  2. CZF に選択公理を加えると、任意の $\Delta_0$ 論理式について排中律が成り立つ。
  1. IZF は 排中律の定理「Diaconescu の定理」の仮定をすべて含む。
  2. その証明で分出を使うのは、論理式 $\varphi$ から集合 $A=\{x\in2\mid x=0\lor\varphi\}$、$B=\{x\in2\mid x=1\lor\varphi\}$ を作る所だけである。$\varphi$ が $\Delta_0$ なら $x=0\lor\varphi$、$x=1\lor\varphi$ も $\Delta_0$ なので、$\Delta_0$ 分出で $A,B$ が得られ、残りの議論（対の公理、外延性、$f$ が関数であること、$2$ の元が $0$ か $1$ であること）はそのまま使える。$\square$

$\Delta_0$ 論理式についての排中律から任意の論理式についての排中律を得るには、任意の論理式による分出があれば足りる（Shu18 p. 6）。

理由を開く

論理式 $\varphi$ に対し、分出で $a:=\{x\in1\mid\varphi\}$ をとる。$0\in a$ は原子式なので $\Delta_0$ 論理式であり、$0\in a\lor0\notin a$ が成り立つ。$0\in a$ は $0\in1\land\varphi$、すなわち $\varphi$ と同値なので、$\varphi\lor\lnot\varphi$ が成り立つ。

冪集合の代わり：fullness と関数の集合

CZF は冪集合公理をもたないが、fullness から「$a$ から $b$ への関数全体」が集合になる。この原理（指数の公理）は、Myhill が Bishop 流の構成的数学に足りるとした冪集合の代わりである（Cro24 §1.3.2）。直積 $a\times b$ は CZF でも作れる（Cro24 の補遺「Two Examples」）。

fullness・指数・冪集合

直観主義論理の上で、外延性・空集合・対・合併・$\Delta_0$ 分出を仮定する。
(1) 冪集合公理があれば fullness が成り立つ。
(2) fullness があれば、任意の $a,b$ について、$a$ から $b$ への関数全体の集合 $b^a$ がある。
(3) 強い収集と、$a$ から $2$ への関数全体の集合 $2^a$ があり、さらに $\Delta_0$ 論理式についての排中律が成り立てば、$\mathcal P(a)$ がある。

「$r$ は $a$ から $b$ への全域的な関係」「$g$ は関数である」は、$\langle x,y\rangle\in r$ が $\exists p\in r\ (p=\langle x,y\rangle)$ と書けることから、どれも $\Delta_0$ 論理式である。
(1) 冪集合と $\Delta_0$ 分出で $a\times b\subseteq\mathcal P(\mathcal P(a\cup b))$ を作り（ZFC公理系の命題「直積の存在」と同じ。排中律は使わない）、$m:=\{r\in\mathcal P(a\times b)\mid r\text{ は全域的}\}$ とおく。全域的な関係 $r$ は $m$ に属するので、$g:=r$ ととればよい。
(2) $a,b$ について full な集合 $m$ をとり、$\Delta_0$ 分出で $F:=\{g\in m\mid g\text{ は関数}\}$ とおく。$F$ の元は全域的な関数、すなわち $a$ から $b$ への関数である。逆に $f$ を $a$ から $b$ への関数とすると、$f$ は全域的なので $g\subseteq f$ となる $g\in m$ がある。$\langle x,y\rangle\in f$ とすると、$g$ は全域的なので $\langle x,y'\rangle\in g\subseteq f$ となる $y'$ があり、$f$ は関数なので $y'=y$、すなわち $\langle x,y\rangle\in g$ である。よって $f=g\in F$ であり、$F=b^a$ である。
(3) 各 $\chi\in2^a$ に対し、$\Delta_0$ 分出で $S_\chi:=\{w\in a\mid\langle w,1\rangle\in\chi\}$ がただ一つ定まる。強い収集を論理式 $y=S_\chi$ に当てると、集合 $p$ で、各 $\chi\in2^a$ について $S_\chi\in p$、かつ $p$ の元はすべてある $S_\chi$ に等しいものがある。$p$ の元は $a$ の部分集合である。逆に $z\subseteq a$ をとる。直積 $a\times2$ は、強い収集を論理式 $y=\{\langle w,0\rangle,\langle w,1\rangle\}$（$w\in a$）に当てて得た集合の合併である。$\Delta_0$ 分出で
$$ \chi_z:=\{q\in a\times2\mid\exists w\in a\,\bigl((w\in z\land q=\langle w,1\rangle)\lor(w\notin z\land q=\langle w,0\rangle)\bigr)\} $$
とおく。$w\in a$ に対し、$\Delta_0$ 論理式 $w\in z$ についての排中律から $w\in z\lor w\notin z$ なので、$\chi_z$ は $w$ に値をもつ。$0\neq1$ なので値は一つである。よって $\chi_z\in2^a$ で、$S_{\chi_z}=z$ となり、$z\in p$ である。したがって $p=\mathcal P(a)$ である。$\square$

  1. の証明で排中律を使ったのは、部分集合 $z$ の特性関数 $\chi_z$ を作る所だけである。直観主義論理では $a$ の部分集合と $a$ から $2$ への関数は一致せず、部分集合のほうが多い（「例」の節の $\{x\in1\mid\varphi\}$）。
CZF に排中律を加えると ZF になる

CZF に排中律（任意の論理式について $\varphi\lor\lnot\varphi$）を加えた体系と ZF は、同じ定理をもつ。

ZF の公理が CZF＋排中律で証明できることを示す。外延性・対・合併・無限は共通である。強い収集は、関数を定める論理式に当てれば置換図式を与える。prop-cst-fullness の (2) により $2^a$ があり、排中律のもとで (3) により冪集合公理が成り立つ。任意の論理式による分出は、置換図式と排中律から、ZFC公理系の命題「置換から分出と対が出る」の (a) と同じ議論で得られる。正則性公理は prop-cst-induction-minimal の (2) から得られる。
逆に、ZF は古典論理の理論なので排中律を含み、CZF の公理を証明する。外延性・空集合・対・合併・無限・$\Delta_0$ 分出は ZF の公理またはその例である。収集は ZF で証明でき（Shu18 p. 6）、得た $b$ を $\{y\in b\mid\exists x\in a\,\varphi(x,y)\}$ に縮めれば強い収集になる。fullness は prop-cst-fullness の (1) による。$\in$ についての帰納法は正則性公理から得られる。

帰納法の確かめ

$\forall a\,(\forall y\in a\,\varphi(y)\to\varphi(a))$ を仮定し、$\lnot\varphi(a_0)$ となる $a_0$ があるとする。$a_0$ の推移閉包 $t$（$a_0\in t$ を満たす最小の推移的集合）をとり、$X:=\{y\in t\mid\lnot\varphi(y)\}$ とおく。$X$ は $a_0$ を含むので空でなく、正則性公理により $X$ の元 $m$ で $m\cap X=\emptyset$ となるものがある。$y\in m$ なら推移性から $y\in t$ で、$y\notin X$ なので $\varphi(y)$ である。仮定から $\varphi(m)$ となり、$m\in X$ に反する。$\square$

IZF に排中律を加えた体系も ZF と同じ定理をもつ（Cro24 の補遺。収集は置換を含み、冪集合と分出はそのまま ZF の公理である）。

強さとモデル

以下はこの記事では証明しない。

  • IZF の証明論的な強さは ZF と同じである（Friedman, 1973。Cro24 §1.3、§5.1）。
  • CZF の証明論的な強さは、1 回の帰納的定義の理論 $\mathrm{ID}_1$ と同じで、二階算術よりずっと弱い。それでも、CZF に排中律を加えるだけで ZF と同じ定理をもつ体系になる（Cro24 §5.1）。
  • CZF は Aczel（1978）によって Martin-Löf型理論 の中に解釈され、この解釈が CZF の公理の構成的な意味の根拠とされる（Cro24 §1.3.3 と補遺）。
  • IZF は 選言性（$\varphi\lor\psi$ が文として証明できるなら、$\varphi$ か $\psi$ が証明できる）をもつ（Beeson, 1985。Cro24 §5.3.1–5.3.2）。
    選言性から、IZF が排中律を証明しないことが分かる。
IZF は排中律を証明しない

ZFC が無矛盾なら、文 $\sigma$「$\mathbb R$ の任意の部分集合は可算であるか $\mathbb R$ と対等である」について、IZF は $\sigma\lor\lnot\sigma$ を証明しない。ここで $\mathbb R$ は IZF の中で一つの定義（たとえば有理数の Dedekind 切断の全体）に固定し、「可算」は「空であるか $\omega$ からの全射がある」と読む。古典論理のもとでは、これらは通常の実数の集合と可算性に一致する。

IZF が $\sigma\lor\lnot\sigma$ を証明すると、選言性により IZF は $\sigma$ か $\lnot\sigma$ を証明する。IZF の公理は ZF の定理であり、直観主義論理の推論は古典論理でも正しいので、ZF、したがって ZFC が $\sigma$ か $\lnot\sigma$ を証明する。ZFC のもとで $\sigma$ は連続体仮説と同値であり（連続体仮説の命題「連続体仮説の同値な言い換え」）、ZFC が無矛盾なら連続体仮説は ZFC から証明も反証もできない（同じ記事の定理「連続体仮説の独立性」）。これは矛盾である。$\square$

反例の表

外す条件反例成り立たなくなること
正則性公理（thm-cst-regularity-lem の仮定）を $\in$ についての帰納法に替えるIZF（ZFC が無矛盾なら）排中律（prop-cst-izf-no-lem）
選択公理（cor-cst-choice の仮定）を外すIZF（ZFC が無矛盾なら）排中律（prop-cst-izf-no-lem）
排中律（prop-cst-fullness (3) の証明で特性関数を作る段）IZF（ZFC が無矛盾なら）での $1$ の部分集合 $\{x\in1\mid\sigma\}$（$\sigma$ は prop-cst-izf-no-lem の文）部分集合がすべて特性関数をもつこと

1 行目と 2 行目の IZF は、正則性公理も選択公理も含まず、それ以外の thm-cst-regularity-lem・cor-cst-choice の仮定（外延性・空集合・対・分出）をすべて満たす。3 行目は、$\{x\in1\mid\sigma\}$ が特性関数 $\chi$ をもつことが IZF で証明できれば、$\chi(0)=1$ か $\chi(0)=0$ かで場合を分けて IZF が $\sigma\lor\lnot\sigma$ を証明してしまうことによる。IZF は冪集合公理をもつので、(3) の結論である $\mathcal P(a)$ の存在そのものは IZF で成り立つ。

注意

  • 構成的集合論の「構成的」は、冪集合や任意の論理式による分出を避ける可述的な体系（CZF など）を指し、IZF のようにそれらを許す体系は「直観主義的」と呼んで区別することが多い（Shu18 pp. 7–8）。
  • 選択公理は排中律を導くので構成的集合論では仮定しないが、可算選択公理や従属選択公理を加えることはある（Cro24 の補遺「Choice Principles」。可算選択公理、従属選択公理）。
  • 自然数の集合 $\omega$ の元どうしの等号は決定できるが、実数どうしの等号は一般に決定できない（構成的数学）。

関連項目

参考文献

[2]
Michael Shulman, Comparing material and structural set theories, arXiv:1808.05204v3, 2018, §2（pp. 5–8：基本公理、fullness、収集、IZF と CZF の定義、p. 6：任意の論理式の分出と $\Delta_0$ 論理式の排中律、ZF での収集、pp. 7–8：構成的と直観主義的の呼び分け）

Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する

Mathpediaを支援する
構成的集合論