前回解説した
再帰的集合論の公理を論理式で表現してみましょう。
まず、高階の集合論のことはとりあえず忘れて、与えられた理論 τ に対し、1変項述語記号 set と2変項述語記号 ∈ を追加し、更に次のような省略記号を導入します:
(1a) τ'(x) ≡ τ(x) ∨ set(x)
(1b) ∀x∈a
R(x) ≡ ∀x [ x∈a ⇒
R(x) ]
(1c) ∃x∈a
R(x) ≡ ∃x [ x∈a ∧
R(x) ]
(1d) a⊂b ≡ set(a) ∧ set(b) ∧ ∀x∈a ( x∈b )
(1e) a〜b ≡ a⊂b ∧ b⊂a
以上のもとで、次の公理群を追加します:
(2a) ∃
seta ∀
τx ( x∈a )
(2b) ∀
τ'a ∀
τ'b ∃
setc ( a∈c ∧ b∈c )
(2c) ∀
seta [ ∀x∈a set(x) ⇒ ∃
setb ∀x∈a ∀y∈x ( y∈b ) ]
(2d) ∀
seta ∃
setb ∀
setx⊂a ∃y∈b ( x〜y )
(2e) ∀
seta ∃
setb ∀x [ x∈b ⇔ ( x∈a ∧
R(x) ) ]
最後の (2e) は、いわゆる
分出公理です。そこで、新たな省略記号として
(3) {x∈
a|
R(x)} ≡ ε
setb ∀x [ x∈b ⇔ ( x∈
a ∧
R(x) ) ]
と定義します。
再帰的集合論には外延性公理が無いので、このような集合はただ一つに定まるわけではありません。ですから、ε量化記号を用いて、そのような集合(公理 (2E) によって少なくとも一つ存在することは保証される)の中の一つを特定するわけです。このためにも、ε量化記号の導入は必須なわけです。
また、(2b) はいわゆる
非順序対の公理で、任意のτ'項 a , b に対し、a と b を元に持つ集合が存在することが保証されるので、分出公理により、a と b
のみを元に持つ集合が存在します。これを {a, b} と書くことにします。すなわち
(4) {a, b} ≡ ε
setc ∀x [ x∈c ⇔ ( x=a ∨ x=b ) ]
ここでも外延性公理を持たないためにこのような集合の一意性は成り立ちません。
また (2c) はいわゆる
和集合の公理で、これも分出公理と組み合わせることによって、集合のみからなる任意の集合 a に対して a の元の元だけからなる集合が存在することがわかるので、これを ∪a と書きます:
(5) ∪a ≡ ε
setb ∀x [ x∈b ⇔ ∃y∈a ( x∈y ) ]
もちろん、和集合についても一意性は成り立ちません。
また、(2d) はいわゆる
冪集合の公理ですが、前回にも注意したように、ZF集合論の場合と異なり、集合 a の部分集合すべてからなる集合の存在は保証されず、ただ a の部分集合と元が共通な集合を必ず持つような集合の存在のみが保証されます。すなわち、a の
冪集合 P(a) を
(6) P(a) ≡ ε
setb ∀
setx [ ∃y∈b (y〜x) ⇔ x⊂a ]
で定義します。すなわち冪集合は
(7) x∈P(a) ⇔ x⊂a
というシンプルな関係ではなく、
(7)' [ ∃y∈P(a) y〜x ] ⇔ x⊂a
が成り立つことになります。
最後に、(2a) は、τ項の全体からなる集合の存在を保証するもので、ZF には無い公理です。この (2a) と分出公理の組み合わせにより保証される、τ項の全体からなる集合を [τ] と書くことにします:
(8) [τ] ≡ ε
seta ∀x [ τ(x) ⇔ x∈a ]
この集合 [τ] の元は、もとの理論における対象のことであり、再帰的集合論においては、いわば「集合ではない」数学的対象を表わしており、一般に集合論に集合ではない対象の存在を許す集合論においては、そのような集合でない対象を
urelement とよんでいます。
ただし、再帰的集合論では、[τ] の元は集合ではないとまでは主張しておらず、集合であってもかまいません。ただ集合であるとは限らない、というだけです。
更に言えば、通常の urelement を許す集合論では、urelement 以外の対象に対しては外延性公理を仮定することが多いですが、再帰的集合論ではそのようなこともありません。
以上のように、再帰的集合論は、ZF集合論と比べると、外延性公理と置換公理と無限公理と正則性公理を持たず、かわりに分出公理と urelement を持ちます。
また、後述するように、ε量化記号を持つために選択公理は定理として導出できます。更に、無限公理は、このままでは成立していませんが、再帰的集合論をうまく用いることによって、無限公理を成り立たせるようにできることがわかります。これも後で解説することにします。