「集合\(A\)が有限集合であるとは、ある自然数\(n\)に対し、\(A\)と\(\{0,1,\dotsc,n-1\}\)の間に全単射が存在することである。一方、有限集合ではない集合は無限集合である。」
「存在量化子\(\exists\)の有限回の除去は通常の論理でできるので、選択公理が力を発揮するのはもっぱら無限集合が相手の時である。」
……本当にそうだろうか？
「集合は有限集合か無限集合のどちらかだ」という考え方は排中律的であり、構成的数学では考え直す必要がある。
この記事では、「無限」ではないが「有限」とも言えない集合について考えたい。有限集合の定義は最初に書いたものとする。無限集合のちゃんとした定義はしない。
有限集合からの全射を持つ集合
2つの記号A, Bからなる集合に同値関係\(\sim\)を入れて割った集合\(X=\{\mathtt{A},\mathtt{B}\}/{\sim}\)を考える。ただし、同値関係\(\sim\)は\[\mathtt{A}\sim\mathtt{B}\Leftrightarrow\text{リーマン予想が成り立つ}\]で生成されるものと定める。「リーマン予想が成り立つ」の部分は、今の人類にとって未知であれば正直何でも良い。構成主義者は薄情なので、リーマン予想が解決したら別の未解決問題を題材にするだけである。
とにかく、この集合\(X\)は明らかに無限集合ではない。では有限集合か？というのが問題となる。
仮に、ある\(n\)に対して、集合\(\{0,1,\dotsc,n-1\}\)（以後これを\([n]\)と書くことにする）との全単射\(f\colon [n]\to X\)が存在したとしよう。構成的数学であっても自然数についての場合分けはできる。当然、\(n=0\)あるいは\(n>2\)の場合はありえない。消去法で、\(n=1\)または\(n=2\)だ。
\(n=1\)の場合は、\(\mathtt{A}\sim\mathtt{B}\)が成り立つということなので、リーマン予想が成り立つということになる。一方、\(n=2\)の場合は、\(\mathtt{A}\sim\mathtt{B}\)が否定されるので、リーマン予想が成り立たないということになる。
我々はリーマン予想を解決してしまったのだろうか？もちろん違う。これはただの排中律だ。そう、「\(X\)が有限集合である」と仮定したことで排中律が導かれたのだ。\(\sim\)の定義を差し替えれば、同じ論法を使って好きな命題について排中律を導出できる。
こうなったのは\(X\)が有限集合であると仮定したせいだ。そういうわけで、構成的数学では\(X\)が有限集合であることも無限集合であることも言えなさそうだ。nLabでは、このような「有限集合からの全射を持つ集合」のことをfinitely indexed setと呼んでいる（finite set in nLab）。
構成的数学の基本的な事実として、「フルの選択公理は認められない（フルの選択公理から排中律が導かれる）」というものがある。この定理は（実際の初出はともかくとして）Diaconescuに紐づけられる（Diaconescu’s theorem – Wikipedia）。この定理の証明で使っているのがまさに「有限集合からの全射を持つ集合」である。なので、「選択公理が力を発揮するのは無限集合の場合」というのは視野が狭く、「選択公理が力を発揮するのは有限集合ではない場合」と言うべきだろう。
もちろん、排中律が使えるのであれば「有限集合からの全射を持つ集合は有限集合である」ことが言える。\(f\colon[n]\to X\)に対し、\(f(i)=f(j)\)かどうかを排中律でテストしていけば\(X\)の正確な個数がわかる。
有限集合への単射を持つ集合
また適当な命題\(P\)を取る。\(P\)はリーマン予想でもゴールドバッハ予想でも何でもいい。\([1]\)の部分集合\(X\)を\(X=\{x\mid x=0\land P\}\)と定義する。\(X\)は有限集合だろうか？
例によって、有限集合ならば元の個数について場合分けができる。\(n=0\)の場合は\(P\)は成り立たない、\(n=1\)の場合は\(P\)が成り立つ、ということになる。やはり、\(X\)が有限集合だと仮定すると排中律\(P\lor \lnot P\)が導出できてしまう。
nLabでは、このような「有限集合への単射を持つ集合」のことをsubfinite setと呼んでいる。日本語に訳すなら部分有限集合か、劣有限集合となるだろうか。
もちろん、排中律が使えるのであれば「有限集合への単射を持つ集合は有限集合である」ことが言える。\(f\colon X\to [n]\)に対し、\(f^{-1}(i)\)が空かどうかを排中律でテストしていけば、\(X\)の元を列挙できる。
有限集合からの全射を持つ集合への単射を持つ集合／有限集合への単射を持つ集合からの全射を持つ集合
nLabで言うところのsubfinitely indexed setは、有限集合からの全射を持つ集合への単射を持つ集合、あるいは、有限集合への単射を持つ集合からの全射を持つ集合のことだ。ここでは、この2条件が同値であることだけ確認しておく。
集合\(X\), \(Y\)に対し、有限集合\([n]\)からの全射\(f\colon [n]\to X\)と、単射\(g\colon Y\to X\)が存在するとする。\(Y\)が問題の集合で、\(Y\)が「有限集合への単射を持つ集合からの全射を持つ集合」であることを言いたい。そのために\(Z:=\{(i,y)\in[n]\times Y\mid f(i)=g(y)\}\)とおく。\(Z\)からの射影\(Z\to[n]\)が単射であることは、\(g\)の単射性から言える。\(Y\)から\(Z\)への全射が存在することは、\(f\)の全射性から言える。なので、\(Y\)はそういう集合である。
逆を示そう。集合\(Y\), \(Z\)に対し、有限集合\([n]\)への単射\(a\colon Z\to[n]\)と、全射\(b\colon Z\to Y\)が存在するとする。この時、非交和\([n]\sqcup Y\)に同値関係\(\sim\)を入れた集合を\(X\)とする。ただし、\(\sim\)は次の関係で生成されるものとする：\(i\in[n]\)および\(y\in Y\)に対し、\[i\sim y\Leftrightarrow \exists z\in Z.\ i=a(z)\land y=b(z).\]すると、\(b\)の全射性より\([n]\to X\)が全射であることが言える。また、\(a\)の単射性より\(Y\to X\)が単射であることが言える。よって、\(Y\)はそういう集合である。
これで、subfinitely indexed setの2つの定義が同値であることが言えた。
まとめ
古典論理に基づいた数学では、「有限集合」「無限集合」という用語の定義にそこまでこだわる必要はなかった（選択公理を仮定しないと「無限集合」の概念が分裂するような話はあるようだが）。しかし、構成的数学では「有限集合」の概念が複数に分裂する（私は「分裂」と言っているが、文献ではbifurcate（分岐する）と書かれているのを見たことがある）。このような現象のある世界を、白黒はっきりしない厄介な世界と考えるか、グラデーションや色彩があって豊かな世界と考えるかは、人によるだろう。
この記事では「有限」の周辺について語ったが、「可算無限」の周辺にもそういう区別がありそうである。
書いていて思ったが、記事タイトルの「有限になれない」というのは「有限集合だと仮定すると非構成的な原理（排中律とか）が導かれる」という意味であって、「有限集合だと仮定すると矛盾する」という意味ではない。Bishop, Bridges「Constructive Analysis」では斜体の「not」にそういう意味を込めていたが、構成的数学について書く際はその辺を混同しないようにしたい。