何を今更な話をします。この記事は、他の記事から参照することを主な目的にしています。
モノに対してその種別と相対役割りを区別しましょう； 区別しないとダメです。例えば、人というモノ（「モノ」は広義、人も一種のモノと考える）について、未成年と成人の区別は社会的に必要でしょう。実際に、未成年／成人は区別できます。特定の人が未成年か成人かは、その人だけを見れば（調べれば）区別できます。そのモノだけを見れば（調べれば）分かる特徴付け／分類がモノの種別です。
今、男ばかりの三人兄弟がいたとします。長男から見ると、次男は弟です。が、三男から見れば、次男は兄です。モノ（この場合人）だけを見ても、「弟」か「兄」かは決定できません。他の兄弟との関係性で「弟」か「兄」かが決定されます。「弟」「兄」は相対役割りの一例です。
ZF集合論〈ツェルメロ／フレンケル集合論〉において、すべてのモノは集合です。ZF集合論の世界では「なんでも集合（集合以外のモノは存在しない）」です。つまり、「集合」は唯一の種別です。それに対して、「要素」は相対役割り（に付けられた名前）なのです。所属関係〈membership relation〉を使った次の形があったとき、
$`\quad x \in y`$
所属記号 '$`\in`$' の左側に置いた集合の相対役割りが要素です。要素という種別はありません。$`x`$ だけを出されたとき、$`x`$ をいくら入念に調べても、それが要素かそうでないかを決定することは出来ません（だって、種別じゃないからな）。
それに対して、型理論では、型とインスタンスを種別にしようとします（うまくいかないときもありますが）。居住記号 '$`:`$' （「型・インスタンス・宇宙とタルスキ宇宙系列 // 居住関係」参照）の左側の役割りをインスタンスと呼ぶ以前に、インスタンスという種別があり、それは型とは別な種別だと考えたいのです。しかし、「型の型」という概念を入れると、困ったことになります。$`x`$ の型が $`y`$ で、型 $`y`$ の形が $`z`$ だとすると、次のように書けます。
$`\quad x : y : z`$
$`y`$ は型ですが、$`y`$ は $`z`$ に居住するのでインスタンス〈居住者〉でなくてはなりません。$`y`$ の種別は型〈居住地〉なのかインスタンス〈居住者〉なのか？ 決定できなくなります。また、$`z`$ の種別もよくわからなくなります。
対策として、インスタンス、型、宇宙の種別を設けると：
- インスタンスは型に居住できる。型はインスタンスをホストする（「ホストする」については「型・インスタンス・宇宙とタルスキ宇宙系列 // 居住関係」参照）。
- 型は宇宙に居住できる。宇宙は型をホストする。
これで一件落着のようですが、「型の型の型」を考えると、また種別を増やす必要があり、だんだん煩雑になってきます。「要素は相対役割りに過ぎない」と割り切ってしまい単一の種別で済ませる集合論とは違って、型理論では、種別と相対役割りの関係をシリアスに考える必要があるのです。
標準的なZF集合論では、要素をまったく持たない集合は空集合だけです。空集合ではないが要素を持たないモノを認める立場もあるにはあります。要素を持たないモノを原子〈atom〉と呼びます*1。空集合以外に原子があってもいいとするZF集合論の変種をZFA集合論といいます。"A" は "atom" からです。
ZFA集合論は話が複雑になって、それに見合うメリットもないので集合論として使われることはほとんどありません。が、多くの人は直感的に原子を想定しているのかも知れません。もし原子を許した集合論で考えるなら、原子は種別です。「要素」という相対役割りを表す言葉を、「原子」という種別を表す言葉と誤認して使っている可能性もあります。仮に原子を認めたとしても、それでも「要素」と「原子」はまったく別な概念です。
*1:ur-element, urelement と呼ぶこともあります。
