数理科学と日本古代史のブログ

　さて、新しく導入した「冪項」という概念こそが、形式化の原理の観点による「素朴集合論」に他なりません。
　さて、この冪理論ですが、一つ注意しなければならないことがあります。
　それは、冪項については外延性公理：

(1) 2^τ(A) ∧ 2^τ(B) ∧ ∀x[x∈A ⇔ x∈B] ⇒ A = B

が成り立たないという事実です。

　すなわち、冪項間の等号を証明すべき公理も推論規則も無いのですから、(1) が導出できるはずがありません。

　これは、ある意味当然で、もともと冪項というのは、{x|R(x)} という記号列のことであり、それを理論内部の概念に形式化しただけなのですから、「元が共通なら両者は等しい」などということが成り立つはずがありません。それが成り立つのは、例えば両者が記号列として同一の命題 R(x) から作られた冪項の場合、すなわち、冪項に対してアプリオリに等号が成り立つのは

(2) {x|R(x)} = {x|R(x)}

という場合です。実際、(2) は等号に関する消去規則 (=導入) から導出することができます。

　さて、ZF だけでなく、他の公理的集合論では、多くの場合、外延性公理を前提にすることが多いようですが、ε量化記号を持つ推論体系のもとでは、実は外延性公理を仮定すると、一般に排中律が導かれてしまうのです。

　考察している理論 τ が相異なる２つのτ項、すなわち

(3) a≠b

を満たすτ項 a, b を持つとします。
　このとき、任意の命題 R を取り、冪項 A と B を

(4a) A ≡ { x | (x=a ∧ R) ∨ x=b }

(4b) B ≡ { x | x=a ∨ (x=b ∧ R) }

で定義します。このとき、明らかに

(5a) b∈A

(5b) a∈B

が成り立つので、τ項 s と t を

(6a) s ≡ εx(x∈A)

(6b) t ≡ εx(x∈B)

で定義すれば、

(7a) s∈A

(7b) t∈B

が成り立ちます。これは、冪項に関する推論規則に拠れば

(8a) (s=a ∧ R) ∨ s=b

(8b) t=a ∨ (t=b ∧ R)

が成り立つことを意味します。ゆえに、場合分けにより、

(9a) s=a ∧ R

(9b) t=b ∧ R

(9c) s=b ∧ t=a

のうちのいずれかが成り立ちます。
　ここで (9a) 又は (9b) の場合は明らかに R が成り立ちます。
　また、(9c) の場合は、命題 R を仮定すると、

(10) x∈A ⇔ [(x=a ∧ R) ∨ x=b] ⇔ [x=a ∨ x=b] ⇔ [x=a ∨ (x=b ∧ R)] ⇔ x∈B

となりますから、ここで外延性公理を用いると

(11) A=B

が成り立ちます。ここで命題 P(X) を

(12) P(X) ≡ εx(x∈A) = εx(x∈X)

で定義すると、まず等号の推論規則 (=導入) により

(13) εx(x∈A) = εx(x∈A)

が成り立ちますから、これは (12) の定義によれば

(14) P(A)

と書けます。従って、(14) と (11) から等号の推論規則 (=消去) を用いると、

(15) P(B)

が成り立つことになりますが、これは (12) の定義によれば

(16) εx(x∈A) = εx(x∈B)

を意味し、更にこれは、定義式 (6a), (6b) により

(17) s=t

を意味します。ここで、場合分けで今考えているのは (9c) が成り立つ場合であったことに注意すれば、

(18) a=b

が得られて (3) と矛盾します。
　すなわち (9c) が成り立つ場合は、R を仮定して矛盾が導けたのですから、¬R が得られます。
　以上により、ε量化記号を持つ推論体系では、集合論の公理として外延性公理を持つと、任意の命題 R に対して排中律：

(19) R ∨ ¬R

が導けることがわかりました。
　つまり、上記の証明で、外延性公理が、以前解説したε公理の役割を果たしているのです。

　以上の事実により、多くの構成的集合論において、外延性公理を仮定して、ε量化記号や選択公理を持たない、と規定することが多いようです（例えば直観主義的ZF集合論）。

　しかし、“形式化の原理”の立場から言うと、これはまさに“本末転倒”で、ε量化記号の導入は、形式化の原理に則った“根拠のある”理論拡大であるのに対し、集合論における外延性公理は、今回の議論の前半で見たように、形式化の原理としては何ら正当化すべき根拠が無いのです。

　外延性公理は、「集合とはモノの集まりのことである」という直感的イメージが「集合とは、そのメンバーによって完全に特徴付けられる」という印象を与えるためか、どうしても“自然な”公理であると思われがちですが、形式化の原理という立場で冷静に考えれば、別に自然でも何でもありません。

　なぜなら、外延性公理 (1) は、その形を見れば明らかなように、一種の「等号に関する導入規則」の形をしています。
　従って、もし (1) を公理に追加するのであれば、それに併せて、等号に関する推論規則が局所整合性を満たすように、等号の消去規則を変更する必要があるからです。
　実際、等号に関する推論規則が局所整合性を満たすためには、等号の消去規則

(20) P(S) と S=T から P(T) が導出できる。

の S=T のところを外延性公理 (1) の左辺に置き換えて得られる推論：

(21) P(S) と 2^τ(S) と 2^τ(T) と ∀x[x∈S ⇔ x∈T] から P(T) が導出できる。

が外延性公理を使わないで導出できなければなりませんが、これは一般に証明できないからです。
　例えば、τ項であってかつ 2^τ項であるような項の存在は別に否定されていません。そこで P(x) に τ(x) を代入すると、(21) は

(22) τ(S) と 2^τ(S) と 2^τ(T) と ∀x[x∈S ⇔ x∈T] から τ(T) が導出できる。

となりますが、外延性公理無しにこのような命題が証明できないことは明らかでしょう。

　もし外延性公理 (1) を導入して、しかも等号の推論規則が局所整合性を満たすようにしたければ、等号の消去規則を

(23) T∈A と A=B から T∈B が導出できる。

という形に変更しなければなりません。
　ところが等号の推論規則 (=消去) をこのように変更してしまうと、先述の排中律を導出した証明において、(14) と (11) から (15) を導いた推論が成り立たなくなり、この証明は無効になり、排中律の導出は不可能になります。

　さて、ここまで解説してきた冪理論は、大変素朴な集合論であることは間違いなく、ZF集合論のような、冪集合、和集合などを自由自在に構成できるような便利な集合論ではありません。この点について冪理論はどのように対応することができるのかについては次回に解説することにします。