「奥野幹也『理論から学ぶデータベース実践入門』はどこがダメなのか」のなかで、ピンクで「（詳細は別途記述予定。）」と書いてあるところが6箇所あります。これらの“ピンクの宿題”を順不同で片付けていくシリーズ第二弾です。
データベース理論などを展開するのにお手頃な集合論・述語論理について云々します。
[奥野さんが言う集合論・述語論理とは、]あくまでリレーショナルモデル界隈を説明・分析する道具・枠組みのことであって、一般的集合論と一般的述語論理の話ではありません。（詳細は別途記述予定。）
[奥野さんは、]述語論理のある特定の体系に対して、ある種の集合論（ZFCってことではない）の宇宙が健全な（ひょっとすると完全な）モデルになっている、ってことを言いたいのだと思います。（詳細は別途記述予定。）
これらの宿題の完全解決とは言い難いですが、思うところを述べます。
なお、ピンクの宿題解決の第一弾は：
内容：
述語論理と集合論
論理の体系（ナントカ論理と呼ばれるモノ）は、目的や趣味に応じて山のようにあります。多種多様なので、論理の分類学や論理の博物学が成立しそうです。しかし、典型的なものをひとつだけ選べと言われれば、一階古典述語論理を選ぶ人が大多数でしょう。
一階古典述語論理（first-order classical predicate logic/calculus）は、完成度が高く使いやすく強力な推論能力を持っています。一階古典述語論理を実際に使うときは、プレーンな体系ではなくて、定数記号／関数記号／述語記号／公理／推論規則を足してカスタマイズしてから使います。
例えば、自然数の理論を展開したいなら、定数記号'0'、1変数関数（単項演算子）記号's'、2変数述語（2項関係）記号'='を足して、それらしい公理（証明なしに認める命題）と数学的帰納法の推論規則も足します。足し算'+'や大小順序'≦'などは、あとから定義により導入できます。
特筆すべきは、ZFC公理的集合論（Zermelo–Fraenkel axiomatic set theory with Choice）も一階古典述語論理により記述されていることです。カスタマイズは自然数論よりむしろ簡単で、追加する記号は'∈'だけです。これに幾つかの公理を足して、あとは一階古典述語論理の推論能力を使って定理を証明していくだけです。
ZFC公理的集合論は、一階古典述語論理の上に構築できる理論の一例に過ぎません。しかし、特別なものだと見なされています。現状の全ての数学的理論は、ZFC公理的集合論の内部で展開できると信じられています。例えば、集合論とは独立に構築した自然数論も、ZFC公理的集合論のなかに埋め込める（集合論の言葉に翻訳できる）のです。
ZFC公理的集合論の万能性・普遍性は認めたとしても、だからと言って、何でもZFC公理的集合論のなかでやる必要はありません。つーか、そんなことはしません。自然数論は、集合論とは独立な体系内でやればいいのです。必要があれば、ZFC公理的集合論への埋め込み（翻訳）を作ればいいのです。
素朴集合論とは何か
集合概念が必要な場面では、ZFC公理的集合論が使われているのでしょうか？ -- 使われません。日常的にZFC公理的集合論を使う人なんていない、と言うと言い過ぎだけど、極めて少数です。
我々が日常的に使っている集合論は素朴集合論（naive set theory）です。要するに、直感的でイイカゲンでカジュアルな集合論です。
厳密な定義や公理系を持たない集合論を総称して素朴集合論と呼んでいるので、素朴集合論を定義するのは無理があります。が、素朴集合論を二種類に分けて考えたほうがよさそうです。ひとつはユーザーフレンドリーなZFC集合論、もうひとつは原始集合論です。
ユーザーフレンドリーなZFC集合論とは何か？ -- ソフトウェアで喩えてみましょう； シンプルで強力だが使いにくいプログラミング言語（例えば、仮想機械のアセンブラ言語）があったとします。そこに、スクリプト言語の処理系を載せて、ツールとライブラリもバンドルして、UIも備えたオールインワンのパッケージを作成したとしましょう。ユーザーは元の低水準言語を意識することはないでしょう。一部の好き者は低水準言語を触りたがります。
まー、そんな感じ。この意味の素朴集合論は、直感的かつ安直に使える集合論ですが、頑張ればZFC集合論に“コンパイル”して合理化できます。
もうひとつの原始集合論とは、集合論を学ぶ以前に知っている集合論とでも言えばいいでしょうか。人間が持つ認識能力の一種です。集合論や論理を学ぶ際に、この種の認識能力が事前にないと、そもそも学ぶことが出来ません。原始的な認識能力に僕は興味を持っているのですが、今日はこれ以上、この話はしません。
アトムと集合
以下、素朴集合論とはユーザーフレンドリーなZFC集合論の意味だとします。
素朴集合論には、集合でないモノがあります。例えば、整数3は集合でしょうか？ 普通の感覚では、3は集合ではありません。しかし、ZFC集合論では全てのモノが集合です。もちろん、整数3もZFC集合論における集合です。
要素を持たないモノをアトム（atom; 原子）と呼びます。素朴集合論で、3はアトムです。ZFC集合論では、3はアトムではありません。このギャップを埋める方法は、割とイイカゲンで、いくつかの集合を特定して、それらの集合の要素は「アトムと見なそう」と約束するだけです。
例えば、プログラミング言語の意味論を作るときなら、整数の集合／実数の集合／文字の集合／二値真偽値の集合あたりを特定して、その要素である整数／実数／文字／真偽値はアトム扱いする、とかです。
aとbがアトムのとき、ペア（順序対）(a, b)はアトムでしょうか？ ZFC集合論の標準的な構成だと、ペアはクラトフスキー・ペア {{a}, {a, b}} として定義されます。しかし、(a, b)もアトムだと見なすほうが都合が良いので、「アトムのペアはアトムである」と約束します。
アトムを認めると、何がアトムで何がアトムでないかイチイチ決めなくてはいけないので面倒になります。ですが、我々がプログラミング言語やデータベースの話をするときは、スカラー型、複合データ型、コレクション型のような区別をするので、アトムを認めたほうがよいでしょう。
宇宙と銀河
ZFC集合論の集合の全体からなる集まりをVとしましょう。オイッ、ちょっと待った！ Vって何だよっ?! って話ですが、「aは集合である」を記号的に a∈V と書くだけだと思ってください。Vはもちろん集合ではありませんから、 V∈V ではありません。「a∈V」と書くときの'∈'と、a, b∈V に対する「a∈b」の'∈'は意味が違いますが、同じ記号を使います。VはZFC集合論の宇宙（universe）と呼びます。
我々が日常的に使う集合論、特にプログラミング言語やデータベースの話をするときに使う素朴集合論の宇宙をUとします。前節の議論より、Uにはアトムも入っているとします。したがって、a∈U は、「aはアトム、または集合」という意味です。宇宙Uのアトムの全体をAtomU、集合の全体をSetUとします。U内に存在するモノはアトムか集合なので、U = AtomU∪SetU です。通常は、AtomU∩SetU = {} （
は空集合）とします。
我々の日常宇宙Uは、ZFCの宇宙Vに埋め込むことが出来るので、U⊆V です。それだけではなくて、日常宇宙Uは、ZFC宇宙Vの単一の集合とみなせるでしょうから、U∈V と考えていいでしょう。日常宇宙Uは小規模な宇宙で、外側に広がる大宇宙Vのなかでは普通の集合に過ぎないのです。
さて、日常宇宙Uのなかで、アトムの双対概念を考えます。aがアトムであることは次のように書けます。
- 論理式： ¬∃b∈U.b∈a
- 自然言語： aの要素となるbが、Uのなかには存在しない。
上の命題のaとbの役割を入れ替えます。
- 論理式： ¬∃a∈U.b∈a
- 自然言語： bを要素とするaが、Uのなかには存在しない。
この条件をbが満たすとき、bを銀河（galaxy）と呼びましょう。銀河はローカルな用語です。もちろん、宇宙から連想して選んだ言葉です。アトムの子（アトムに含まれる要素）は存在しないし、銀河の親（銀河を含む集合）は存在しないのです。bが銀河であっても、b∈U ですが、この意味で使う'∈'は要素と集合の所属関係ではなくて、「bは宇宙U内のモノです」を略記しただけです。
通常、ZFC集合論でも素朴集合論でも、銀河の存在を認めてません。次の命題のほうを認めているのです。
- 論理式： ∀b∈U.∃a∈U.b∈a
- 自然言語： U内の任意のbに対して、bを要素とするaが、Uのなかには存在する。
外側に広がる大宇宙Vに関しては、上記命題（のUをVに置き換えたもの）が必須でしょうが、日常宇宙Uでは銀河を認めてもいいと思います。銀河を認めると、単元集合の構成 a|→{a} や、ベキ集合の構成 a|→Pow(a) が自由に出来ないことになります。不便ちゃ不便ですが、強烈過ぎる集合論的構成を制限したいこともあります。銀河は、そのような制限に使えます。
宇宙Uは銀河を持ち、U内のすべてのモノ（アトムでも集合でも）が、いずれかの銀河内に在るとします。これは、a0∈a1∈... という系列が無限に続くことはなくて、銀河で終端することを意味します。この性質を、∈-系列の有界性と呼び、すべての∈-系列が有界な宇宙を有界宇宙（bounded universe）と呼びましょう。
有界素朴集合論
有界宇宙Uを持つような素朴集合論を有界素朴集合論（bounded naive set theory）と呼ぶことにします。アトムも銀河も許します。そのため、ZFC集合論では認められない（否定が証明できる）次の命題が成立します。
有界素朴集合論に対する宇宙Uは、ZFC集合論の宇宙（非有界素朴集合論の宇宙でもある）Vのなかの集合なので、普通の集合概念／集合操作で作れます。
例えば、N = {0, 1, ...} として、次の宇宙Uを考えます。
- U = N∪Pow(N)∪{Pow(N)}
自然数がUのアトム*1、Nの部分集合がUの集合、Pow(N)がUの銀河になります。この宇宙はアトムを可算個、銀河を1個持ちます。
- AtomU = N∪{
}
- SetU = Pow(N)∪{Pow(N)}
宇宙Uのなかで、親の集合を持つモノを要素（element）と呼び、要素の全体をElmU、銀河の全体はGalUとすれば：
- ElmU = N∪Pow(N)
- GalU = {Pow(N)}
いま定義した AtomU, SetU, ElmU, GalU は、単一の大宇宙だけを考えているときは意味ありませんが、様々な小宇宙を考えるときは、宇宙の性質として意味を持ちます。
ZFC宇宙Vに関して言えば：
- AtomV = {
- SetV = V
- ElmV = V
- GalU = {}
有界素朴集合論の使い途
リレーショナルモデルでは、ドメイン（RDB用語のドメイン）の要素はアトムであり、タプル（RDB用語のタプル）を要素とする有限集合だけが集合（リレーション）であり、それより高階の集合は考えない、という態度を取ります。こういう態度が良いか悪いかはともかくとして、この態度に対応する集合論と述語論理が必要でしょう。それが有界宇宙に関する有界素朴集合論です。
僕の意見としては、上記のごとき制限を付け過ぎるのは良くないと思ってますが、「何がどう良くない」かを説明しようとすると、制限付き（＝有界）集合論という概念を導入せざるを得ません。定義もしてないナニカに対しては、「それは良くない」とさえ言えないじゃないですか。
リレーショナルモデルとは別な話で、型理論において、型の全体の型Typeを導入して、Type : Type という循環を作ることがあります。または、Type1 : Type2 : Type3 ... のような人為的な無限チェーンを想定したりします。このような細工も、銀河を認めない態度からだと思われます。
ある一定の階数以上の高階なモノが不要なら、階層を打ち切って銀河（＝最上階）にしてしまえばいいと思います。自己言及が必要なら、レイフィケーション機構を導入して、Type : Type を合理化すればいいでしょう。
