... レーヴェンハイム・スコーレムの定理により、 そもそも何らかのモデルが存在するならばその加算モデルが存在する と確信できること、は確かにその通りである。 しかしそのような加算モデルが存在すると信じる直接的理由を、 我々はもたないままである。 なぜ我々がそれらの公理系の無矛盾性、充足可能性を確信するのかと言えば、 その公理系が当初記述しようとしていた非加算モデルが明瞭だ と思われるからなのである。
マイケル・ダメット「プラトニズム」
「意図されなかった」解釈 -- たとえば、非可算と「想定されていた」集合が、 そのなかでは「実際には」可算であるようなモデル -- の存在の意義について、 ある点までは論者のあいだの一致がある。 こうしたモデルの存在が示すことは 「意図された」解釈、もしくはある人々の好む表現では「集合の直観的概念」、 が形式的体系によっては「捉え」られないということだという点で、 すべての論者は一致している。 しかし、公理が「集合の直観的概念」を捉えられないとするならば、 いったい、何ならできると言うのだろうか。
ヒラリー・パトナム「モデルと実在」
あらかじめの注: 以下では、たぶん「解釈」「構造」「モデル」とか その他の色々な用語とかを相当いいかげんに使う。 定理が成り立つ条件とかも、たぶんいいかげんに述べられる。
レーヴェンハイム・スコーレムの定理は 「公理系Tは、モデルを持つなら加算モデルを持つ」 というものだけど、なんとなく変な事を言っているようにも見える。
「加算」というのは自然数で番号付けできるという事で、 例えば整数とか有理数は可算で自然数の冪集合とか実数は非可算になる。
で、公理系としてZF集合論の公理系を取ってみる。 この公理系を普通に解釈すると、 解釈領域(モデル)には無限集合やその冪集合が含まれている。 非可算集合も含まれているし、解釈領域自体も非可算になっている。
また非可算集合が存在する事は、ZFで証明できる。
でもレーヴェンハイム・スコーレムの定理によると、 (ZFが無矛盾なら、と一応条件が付くけど)ZFの可算モデルがある事になる。 これは何か変な事のようにも見える。
ZF集合論(とか実数論とか)に可算モデルによる解釈があるというのは、 いまいち納得できないという気分になるかもしれない。 以下では、どうしてそんな解釈があり得るのか、といった話になる(と思う)。
計算機プログラムが文字の単なる並びであるのと同じ意味で、 論理式は記号の単なる並びである。
文字の並びのうちでプログラムになっているものがどれなのかを BNFとかを使って定義するように、 論理学では記号の並びのうちどれが論理式なのかを始めに定義する。 ただしこの部分は論理学の本題ではなく前置きみたいなものなので、 プログラム言語の場合と比べると非常に単純化されている。 例えば形式的には論理式のカッコは一切省略できない。
(本当にカッコを全く省略できないと見にくいので、 普通は表記上はカッコを省略する。 プログラム中にカッコを省略した式があっても正しいプログラムであるのとは違い、 普通の論理学での定義では、 カッコを省略した論理式は正式な論理式ではなく疑似コードみたいなものになる)
どういう記号列が論理式になるかが決まった後、2つのやり方がある。
ひとつは証明論・構文論的な手法で、 証明の前提(始まり)として使える「論理公理」とか、 どんな形の論理式からどんな論理式を導く事ができるかを表す「推論規則」を定めて、 どの論理式が「証明できる」かなどを考察する。 こちらの手法では論理式の形だけを注目して、 論理式の各記号が何を表しているのかは考えない (実際には、論理式の表している内容とかを考えないと、 定めた「論理公理」や「推論規則」を納得できないかもしれないけど)。
もうひとつはモデル論・意味論的な手法で、 こちらは論理式中の各記号が何を表しているかという事を考える。 つまり各記号や各論理式に解釈を与えてやる。
まず解釈領域を決める(例えば、自然数の集合とか)。 で、関数記号・述語記号等の解釈を決める。 定数記号は解釈領域の要素、関数記号は解釈領域上の関数、 述語記号は解釈領域上の関係を表すと解釈する。 「∧」とかの論理記号には自然な解釈を与える (量化記号「∀」「∃」の解釈は幾らか面倒)。 そうすると各論理式には「真」または「偽」という解釈が与えられる。 こちらの手法では、 論理式の「恒真性」だとか「充足可能性」とかを考察する。
(ちなみに(1階)述語論理の健全性・完全性により、 「証明できる」事と「恒真である」事は一致する)
構文論とか意味論とかの言葉は、 分野とか文脈によって使われ方が微妙に違っている。
例えば、次のような説明がある。
(前略)むしろ、モリスに始まりカルナップによって広められた 「構文論・意味論・語用論」という三分法による意味論の定義と合致する。 この伝統的三分法によれば、 構文論とは、言語をその使用者とも言語外の対象とも独立に考察する分野であり、 意味論とは、言語と言語外の対象とのあいだの関係を考察する分野であり、 最後に、語用論とは、 言語・言語外の対象・言語使用者の三者のあいだの関係を考察する分野である。
飯田隆「言語哲学大全III」
この分類の仕方からすれば、例えば証明論は構文論の一部になる。
でも、プログラミング言語の場合に構文論・シンタックスと言えば、 たいていはプログラムの字面上の話(字句解析・構文解析の対象になる部分) の事を指している。 なので、プログラム言語の意味論と言った場合、証明論的なものも含まれている。 (例えばHoare論理は証明論的なプログラム意味論で、 「構文論的意味論」とか呼ばれる事がある)。
論理式の集合Tの事を「理論」とか「公理系」とか呼ぶ (理論と呼ぶ方が普通だと思うけど、以下では公理系の方を使う)。
例えば
T_g = {
∀x∀y∀z((x*y)*z = x*(y*z)),
∀x(e*x = x),
∀x(inv(x)*x = e),
}
は公理系である(郡論の公理系)。
そして、Tに含まれる各論理式を真にするような構造 (解釈領域と解釈を組にしたもの)Mを「Tのモデル」と呼ぶ (MがTのモデルである事を、「M |= T」と書く。「MでTが真である」ということ)。
例えば解釈領域 Uとして整数の集合Zを取り、 解釈Iとして、 「e」を整数0、「*」を整数の足し算、 「inv」をマイナス(整数の符合を反対にする)というものを考えると、 T_gのどの論理式も真となる。 したがってこの(U,I)はT_gのモデルになっている(つまり、(U,I)|=T_g)。
あるいは領域としてU={甲,乙}と取る(「甲」「乙」という記号が、Uの要素)。 そして解釈Iは次のようにする。
e ... 甲
* ... (甲,甲) -> 甲
(甲,乙) -> 乙
(乙,甲) -> 乙
(甲,甲) -> 甲
となる関数
inv ... 甲 -> 乙
乙 -> 甲
となる関数
領域U、解釈Iを上のようにした場合でも、T_gの各論理式は真になるので、 この構造もT_gのモデルとなる。
公理系Tは、別に有限集合である必要はなく、 論理式のどんな集合を公理系としても良い (けれども実際に使う公理系は、 再帰的集合(集合に含まれているかどうかを判定するアルゴリズムがあるような集合) になっている。 再帰的集合という事でついでに書くと、第1不完全性定理は 「ロビンソン算術Qを(実質的に)含む無矛盾で再帰的な公理系」 に対して成り立つ。もう少しゆるい条件でも成り立つけど (注1))。
例えばペアノ算術の公理系PAには、 数学的帰納法の公理が含まれているけど、これは1つの論理式では無く、
∀y_1 ... ∀y_n(ψ(0)∧∀x(ψ(x)->ψ(s(x))) -> ∀x(ψ(x)))
という形のあらゆる論理式が公理になっている (ψは任意の論理式で、y_1 ... y_nはψに出てくるすべての自由変数)。
上の数学的帰納法みたいに、 1つの論理式ではなく論理式のパターンを表しているものを図式(Scheme)と呼ぶ。 そして図式を使って公理を表したものを公理図式と呼ぶ (したがって、上のは「数学的帰納法の公理図式」である)。 でも、公理図式の事も公理と呼んだりする。
一般的に公理系Tに対してそのモデルはいくつもある。 公理系に含まれる論理式を多くすればモデルは少なくなる。 1つもモデルが無い場合もある。 例えばT={A,￢A}とすると、Tのモデルは無い (Aと￢Aの両方を真にするような解釈は無いから)。
そして 「公理系Tが(領域の要素が無限である)モデルを持つならば、 Tは可算モデルを持つ」 というのが、レーヴェンハイム・スコーレムの定理である。
例えば実数論の公理系は、標準的なモデルを持っている (解釈領域を実数の集合として、各記号も普通に解釈する)。 このモデルは可算ではない(実数集合は非可算だから)。 でもレーヴェンハイム・スコーレムの定理によると、 実数論の公理系は可算モデル(領域が可算であるモデル)を持っている。 実数は非可算なのに、可算なモデルを持っているというのは、 おかしな気もする。
あるいは集合論の公理系(例えばZF)を考える。 ZFには、無限集合の存在公理があり、冪集合の公理もある。 なのにレーヴェンハイム・スコーレムの定理により、可算モデルを持っている。 これもやっぱり変な感じがする。
にもかかわらず、論理学的に矛盾が起こるわけではない。
以下ではZFの公理系を説明しつつ、 ZFの可算モデルによる解釈がどうしてあり得るのかを説明する(たぶん、そうなる)。
ZFには「∈」という述語記号がある。 まず、この記号は「含まれる」と解釈する (とにかく、関係「∈」が成り立つ事を「含まれる」と呼んでしまえば良い)。
以下、必要な公理をどんどん付け加えていくような感じで説明していく。
外延公理は、集合の基本的な性質に関するもので
∀x∀y(x=y <-> ∀z(z∈x <-> z∈y))
という公理である。 これは、集合が等しいかどうかは含んでいる要素が同じかどうかで決まる、 という事を表している。
外延公理は集合の性質を表しているけど、 どんな集合が存在するかについては何も言っていない。 そのため他の公理が必要になる。
空集合の存在公理は
∃x∀y(￢(y∈x))
という公理で、要素を1つも含まない集合が存在する事を表している。 この集合を空集合と呼ぶ。 外延公理から空集合はただ1つしかないので、そのただ1つの空集合をφと表す。
空集合の存在公理により 集合が少なくとも1つある事が保証されたので、 次に、既に存在する事が解っている集合を元にして 別の集合の存在を保証する公理を付け加える。
対集合公理は次のような論理式である。
∀x∀y∃z∀w(w∈z <-> (w=x∨w=y))
これは、集合xと集合yがあれば、xとyだけを要素とする集合zがある、 という事を表している。 外延公理から、xとyだけを要素とする集合は1つしかないので、 それを{x,y}と表す。 xとyが等しい場合は、{x}と表す。 これも外延公理により1つしかない (以下でも外延公理が効いてくる場所が出てくるけど、 もうその事はあまり述べない)。
空集合の存在と対集合の公理から、 例えば{φ}とか{φ,{φ}}とか{φ,{φ,{φ}}}とか {{{{{φ}}}}}とか・・・といった集合が存在する。
和集合公理は次のような論理式である。
∀x∃y∀z(z∈y <-> ∃w(z∈w∧w∈x))
これは集合xがあれば、 xの要素の要素になっているものからなる集合yがある、という事を表している。 この集合yを∪xと書く。 xとして{A,B}を取ると、Aの要素とBの要素をあわせたものがyとなる。 xが対集合{A,B}の場合、∪{A,B}をA∪Bと書く。
例えば、空集合公理と対集合公理から存在が保証される {{φ},{{φ},{{φ}}}}に対して和集合公理を使うと
∪{{φ},{{φ},{{φ}}}} = {φ}∪{{φ},{{φ}}}
= {φ,{φ},{{φ}}}
という集合がある事がわかる。
対集合公理と和集合公理を繰り返し使うと、 集合x_1, x_2, ... , x_nがあったら、 それらだけを含んでいる集合{x_1, x_2, ... , x_n}もある事がわかる。
和集合公理に似た冪集合公理というのがあるけど、 この時点ではいらないのでそれは後に回す。
空集合公理、対集合公理、和集合公理だけから 様々な有限集合が存在している事がわかる。 でもこの3つだけでは、無限集合の存在については何も言っていない。 そこで無限集合の存在を保証する無限集合公理を公理に加える。
∃x(φ∈x∧∀y(y∈x -> (x∪{x})∈x))
ここであると言っている集合xには、
φ
{φ}
{φ,{φ}}
{φ,{φ},{φ,{φ}}}
{φ,{φ},{φ,{φ}},{φ,{φ},{φ,{φ}}}
等々
が含まれている。 このxは、有限集合ではあり得ない。
集合論のなかで自然数を扱いたい場合、 次のようにして各自然数に集合を対応させたりする。
0 ... φ
1 ... 0∪{0} = φ∪{0} = {0} = {φ}
2 ... 1∪{1} = {0}∪{1} = {0,1} = {φ,{φ}}
3 ... 2∪{2} = {0,1}∪{2} = {0,1,2} = {φ,{φ},{φ,{φ}}}
4 ... 3∪{3} = {0,1,2}∪{3} = {0,1,2,3}
= {φ,{φ},{φ,{φ}},{φ,{φ},{φ,{φ}}}
以下同様
この対応を使って無限集合公理を読み変えると、 無限集合公理は すべての自然数を含んでいるような集合が存在している事を表している (一応書くと、無限集合公理で存在すると言っている集合に 自然数以外を含んでいるかどうかについては何も言っていない)。
無限集合公理により少なくとも1つは無限集合が存在する事になる。 そこからさらに大きな集合を導くために冪集合公理を加える。
∀x∃y∀z(z∈y <-> z⊆x)
この公理で存在すると言われているyの事をxの冪集合と呼び、P(x)とか2^xと書く。 この公理を自然に解釈すると、 xのすべての部分集合を要素とするような集合が存在する事を表している。 でもこの公理自体は、xに対してどんな部分集合が存在するのかについては 何も言っていない。 「もしzがxの部分集合だったら、zはyの要素だ」と言っているだけで、 xの部分集合にどんなものがあるのかはこの公理からだけではわからない。
例えば無限集合公理により、全ての自然数を含んだ集合がある事はわかる。 でもその部分無限集合として奇数は含まないようなものがあるかどうかは、 今までの公理だけからでは何も言えない。 そういう集合があっても別にかまわないけど、 そういった集合を含まない解釈を与えたって(今のところは)良い。
ある集合の冪集合は、必ず元の集合より濃度は高くなる。 当然、可算集合の冪集合は非可算になる。
でも冪集合公理は、どんな部分集合があるかについては何も言っていない。 だから、集合Aの冪集合(Aの部分集合となっているものをみんな含んだ集合) の濃度が集合Aより大きくならない解釈だって可能かもしれない。
一応これが、ZFが可算モデルを持ち得る理由の1つになる。
集合があってもその部分集合の存在が保証できないというは困る。 そのために次の分出公理図式を考える。 本当は分出公理では弱くて置換公理というのが使われるのだけど、 分出公理の方が説明しやすいのでこれを考える。
∀x∃y∀z(z∈y <-> (z∈x∧ψ(z))) (ψは、yを自由変数として含まない論理式)
(本当はψに含まれている各自由変数に対して全称量化が必要だけど、 それは省略。本当には「∀x」の前に「∀w1∀w2...」みたいなのを付ける)
これは集合xの要素zのうちで ψ(z)を満たすものだけからなる集合yがある事を表している。 この集合は{z∈x| ψ(z)}と書かれる。 様々な論理式に対して分出公理を使って、様々な集合の存在が言える事になる (注2)。
でも論理式は可算個しか無い。 つまり分出公理を使って存在が保証される集合も可算個しか無い、という事になる。 可算個の要素しか保証していないわけだから、可算モデルもあり得る。
(あり得るだけで、あるとは限らない。 公理で存在が保証されるのが可算しか無いからといってそれだけでは、 可算個の要素だけからなる解釈ができるとは判断できない。 可算個の要素だけを考えていては、 すべての公理が成り立つような解釈ができないかもしれない。 レーヴェンハイム・スコーレムの定理によれば、実際にはできるけど)
あと実際にはZFには分出公理ではなく、代わりに置換公理が採用されている。 置換公理があれば分出公理はそこから導く事ができる。 でも面倒なので置換公理の説明はしない。
(置換公理図式は次のようなものである。
∀x∀y∀z(ψ(x,y)∧ψ(x,z) -> y=z) -> ∀u∃v∀y( y∈v <-> ∃x(x∈u∧ψ(x,y)))
まず前半の「∀x∀y∀z(ψ(x,y)∧ψ(x,z) -> y=z)」の部分で ψ(x,y)に対する条件を言っている。 この式は、 xに対してψ(x,y)を満たすようなyはあったとしても1つしかない、 という事を表している。
つまりこの条件を満たすψ(x,y)は、ある部分関数 y=f(x)を表している (ψ(x,y)を満たすyが無い場合、そこでは未定義と考える)。
そして公理の後半では、部分関数をあらわしているψ(x,y)に対して、
∀u∃v∀y( y∈v <-> ∃x(x∈u∧ψ(x,y)))
であると言っている。
まず任意の集合uをとる。 uに含まれる要素xに対してψ(x,y)を満たすy(つまりy=f(x)となるy)を考える。 そのようなyはあるかもしれないし無いかもしれない。
ここでuの各要素xに対してψ(x,y)となるyがあったり無かったりしても、 そうしたyすべてを集めた集合があるかとは限らない。
そして上の式は、 そのようなyすべてを集めた集合vが存在するという事を表している。
分出公理はある集合に対する部分集合の存在を言っているのに対して、 置換公理はある集合に対するその像集合の存在を言っている。
置換公理で、
ψ(x,y) ≡ ψ'(x)∧(x=y)
を取ってみる。 この式は、
f(x) = x (xがψ'(x)を満たす場合) f(x) = 未定義 (xがψ'(x)を満たさない場合)
という関数を表している。 すると、 集合uのψ(x,y)の像集合はuの要素でψ'(x)を満たすものの集合となる。 これは、分出公理で存在が保証されている集合と同じである。 したがって置換公理があれば、分出公理はいらない事になる。 (もっとちゃんと置換公理の式から分出公理の式を導く事もできる)。
ツェルメロが初めに示した公理系には置換公理ではなく分出公理を採用していて、 それでは充分でないとしてフレンケルやスコーレムが置換公理を提出した。 )
正則性公理は次のように書ける。
∀x(∃y(y∈x) -> ∃y(y∈x∧∀z(z∈x -> ￢(z∈y))))
次のように書いた方が見やすいかもしれない。
∀x(x≠φ -> ∃y(y∈x∧(x∩y=φ)))
例えば集合{a}に対して正則性公理を使ってみる。 すると{a}は空集合では無いので
∃y(y∈{a}∧({a}∩y=φ))
となり、{a}の要素はaだけなので
{a}∩a = φ
となる。
ここで、もしもa∈aが成り立っているとすると、
a ∈ {a}∩a ≠ φ
となる。
つまり正則性公理を満たしつつ、 自分自身を要素に持つ集合があるような解釈は行なえない事がわかる。
正則性公理から導かれる他の性質とかは省略。
ZFに選択公理を含める場合、ZFCと言ったりする。 選択公理の説明は面倒なのでやらない。 一応、本題はレーヴェンハイム・スコーレムの定理だし。
外延公理 ∀x∀y(x=y <-> ∀z(z∈x <-> z∈y))
空集合公理 ∃x∀y(￢(y∈x))
対集合公理 ∀x∀y∃z∀w(w∈z <-> (w=x∨w=y))
和集合公理 ∀x∃y∀z(z∈y <-> ∃w(z∈w∧w∈x))
無限集合公理 ∃x(φ∈x∧∀y(y∈x -> (x∪{x})∈x))
冪集合公理 ∀x∃y∀z(z∈y <-> z⊆x)
置換公理図式 ∀x∀y∀z(ψ(x,y)∧ψ(x,z) -> y=z)
-> ∀u∃v∀y( y∈v <-> ∃x(x∈u∧ψ(x,y)))
(分出公理図式) ∀x∃y∀z(z∈y <-> (z∈x∧ψ(z)))
正則性公理 ∀x(x≠φ -> ∃y(y∈x∧(x∩y=φ)))
(選択公理) ∀x(∀y(y∈x -> y≠φ)∧∀y∀z(y∈x∧z∈x∧y≠z ->x∩y=φ)
->∃y∀z∃w(z∈x -> y∩z = {w}))
本来、ある集合の冪集合は必ず元の集合より濃度が大きくなるはず。 でも冪集合公理は、 ある集合にどんな部分集合が存在するかについては何も言っていないし、 分出公理や置換公理では可算の部分集合の存在しか保証していない。
だから、要素が可算であるような解釈をする事が可能になる (可算個の論理式では非可算の存在を保証できない、という事なのか?)。
ZFは可算モデルを持っている。 でもその一方で、非可算集合が存在する事や 冪集合の濃度が元の集合の濃度より大きくなる事は、 ZFで証明する事ができる。 これもそれだけ聞くと変に思える。 これは次のように説明される。
集合AとBの濃度が等しいという事がどういう事だったかというと、 AからBへの全単射(上への1対1)関数が存在する、という事だった。 逆に全単射関数が存在しなければ、AとBの濃度は異なる。 したがって濃度の事を考えるには、 ZFで関数がどう定義されるかを見る必要がある。
まずZFで集合A、B上の関係というは、直積集合A×Bの部分集合として定義される (ZFに限らず一般的に行なわれているやり方)。 で、AからBへの関数というのは、A、B上の関係(A×Bの部分集合)Rで
<x,y>∈R∧<x,z>∈R -> y=z
となるもの(つまりx∈Aに対してy∈Bが高々1つだけ決まるような関係) として定義される。
関数が上のように定義されるので、 「集合AとBの濃度が等しい」というのは 「AからBへの全単射関数になるようなA×Bの部分集合がある」 という事になる。 逆に「集合AとBの濃度が異なる」というのは、 「A×Bのどんな部分集合も、AからBへの全単射関数にはならない」 という事になる。
可算モデルでは、 無限集合Aとその冪集合B=P(A)はどちらも(解釈から見ると)可算集合になる。 したがって(外から見ると)AからBへの全単射関数が存在する。
一方、ZFの内部ではAからBへの全単射関数というのは、 A×Bの部分集合(で、ある性質を満たすもの)だった。 しかし可算モデルによる解釈では、 A×Bのすべての部分集合が解釈領域の要素になっているわけでは無い。
そのため、AもBも可算で従ってAからBへの全単射関数があるけど、 その関数はZFでの関数(A×Bの部分集合)では無い、という事が起こりうる。
だから、 ZFには可算モデルがあるのに非可算集合の存在を証明できる、 といった変に見える事が起こっても、 それは何か問題がある事が起こっているわけでは無い。
(こういう話は、 論理式に対する証明と解釈との区別とかをわかっていれば それほどわかりにくい事では無いはずだけど、 ここでの説明はその辺の区別がいいかげんでわかりにくい)
注1: ロビンソン算術Qは、おおざっぱに言って足し算・掛け算ができるような体系で
Q = {
∀x∀y(s(x)=s(y) -> x = y),
∀x￢(s(x) = 0),
∀x(￢(x=0) -> ∃y(x=s(y))),
∀x(x+0 = x),
∀x∀y(x+s(y) = s(x+y)),
∀x(x*0 = 0),
∀x∀y(x*s(y) = (x*y)+x)
}
という公理系になる(これとは違う定義の仕方もある)。 これにさらに帰納法の公理を付け加えたものを、 (1階)ペアノ算術PAの公理系という
不完全性定理に 「ロビンソン算術Qを(実質的に)含む無矛盾で再帰的な公理系」 みたいな条件があるのは、だいたい次のような理由になる。
不完全性定理を証明する時に、 論理式(つまり記号を並べたもの)を自然数でコード化する、という事を行なう。 その時、足し算とか掛け算ができるくらい公理系が強くないと、 コードに対する操作を定義したりコードの性質を証明したりする事ができない。 そのため「ロビンソン算術Qを含む」という条件がつく。 それより弱い場合、 例えば足し算しか持っていないプレースバーガー算術では、 不完全性定理は成り立たない。 他にも、k個の後者関数を持つ単項2階論理 (monadic second-order logic with k successors, M2kS)とか。
さらに公理系をコード化する必要もある。 公理系が有限個だったらそれぞれコード化すれば良いし、 有限個でない場合でも 論理式が公理系に含まれるかどうかを判定するアルゴリズムがあれば、 それをコード化できる(再帰関数はロビンソン算術で扱える)。 でも公理かどうか判定するアルゴリズムが無いような公理系の場合、 コード化を行なえないので不完全性定理の証明も行なえない事になる。 公理かどうかを判定するアルゴリズムが無いなら、 そんな公理系を実際に利用する事もできないけど。
注2: 見ためが分出公理に似ていてもっと強力な(強力すぎる)内包公理というのがある。
∃y∀z(z∈y <-> ψ(z))
内包公理には、分出公理の「xの部分集合で」という条件が無くて、 ψ(z)を満たす要素だけからなる集合が存在するという事を表している。 つまり性質(それも論理式で表せるような性質)ψがあったら、 それに対応する集合もある、と言っている。
一見自然な事を表しているようにも思えるけど、この公理には問題がある。 論理式ψ(z)として「￢(z∈z)」という式を考える。 この式は「自分自身を含まない」という事を表している。 この式に内包公理を使うと 「自分自身を含まない集合の集合」がある事になり、 ラッセルのパラドックスが生じてしまう。
一方分出公理に対して「￢(z∈z)」を与えても、 xの要素のうちで自分自身を含まないものの集合となって問題は起こらない。
内包公理が認められないという事は、 {x|ψ(x)}で表されるような集合は一般には存在しない事になる。 もしある集合uがあってψ(x)を満たすxは必ずx∈uとなっているなら、 分出公理から{x|ψ(x)}はある集合を表していると考える事ができる。
でもそういう条件とかを考えず{x|ψ(x)}みたいなものを考えたい場合がある。 そこで
{x|ψ(x)}
を、ψで定義されたクラスと呼ぶ。 これは略記とかマクロみたいなもので、 a∈{x|ψ(x)}というのはψ(a)を表していると考える。 例えば
{x|x=x}
というのを考えると、
∀y( y∈{x|x=x})
が成り立つ(∀y(y=y)と同じ事になるので)。 これはすべての集合からなるクラスという事になる (すべての集合からなる集合というのを認めるのは問題があるけど、 すべての集合からなるクラスを認めても問題にはならない)。
2つのクラスが等しい
{x|P(x)} = {x|Q(x)}
というのは、
∀y(y∈{x|P(x)} <-> y∈{x|Q(x)})
に展開され、さらに
∀y(P(y) <-> Q(y))
に展開される。