クラスありの拡張言語が生の集合論と証明能力が変わらない

スマートコン @mr_konn

@alg_d なります。なるように公理が定められています。例えば {x | x ∈ { y | Ψ(y) } ∨ x ∈ { y | {z | Φ(z)} ∈ y }} は {x | Ψ(y) ∨ ∃w ((∀u (u ∈ w ⇔ Φ(u))) ∧ w ∈ y)} と同値で

スマートコン @mr_konn

@alg_d 中の論理式も同様にしてバラすことが出来ます。有限の書き換えステップで基本言語に辿り着けます。クラス変数を含んでいる場合は無限個の論理式からなるスキーマになりますが。

V-alg-d（ZZ） @alg_d

@mr_konn ｳｳ~~~~~基本言語にたどり着ける気がしないので助けてミスター ! !

スマートコン @mr_konn

@alg_d あ、今書き換えはクラス変数を含まないものについて行っているのが前提でした。失礼しました。で、後は帰納法をしっかり見ていけば納得出来ると思います。まず、原始式は α = β または α ∈ β の形ですが、α, βが共にクラス項を含まなければ、そのまま基本言語です。

スマートコン @mr_konn

@alg_d クラス項を含んでいた場合、y ∈ {x | Φ(x) } は Φ(y) のことで、これで一段階外れたのでこいつを更に基本化してやれば基本式に辿り着きます。同様に、{x | Φ(x)} = {y | Ψ(y)} は ∀z(Φ(z)⇔Ψ(z))、

スマートコン @mr_konn

@alg_d {x | Φ(x)} = y は ∀z(Φ(z) ⇔ z∈y)、{x | Φ(x)} ∈ {y | Ψ(y)} は ∃z (z = {x | Φ(x)} ∧ ψ(z))、……などと書き換えていけば、クラス変数はいないので必ず基本言語に辿り着きます

スマートコン @mr_konn

@alg_d まだあと二つありますよ！P と P* に基本言語の公理を後付け足しても両者の証明能力は変わらない、というのと、P* に拡張言語の公理を付け足したら、P にその基本言語でのインスタンスを付け加えれば大丈夫、という子です。

V-alg-d（ZZ） @alg_d

@mr_konn ﾋｮｴｰ https://t.co/cedRRWha　"P にその基本言語でのインスタンスを付け加えれば"　最後にこれなんですけど、どういう意味でしょう。

スマートコン @mr_konn

@alg_d あっこれはちょっと訂正があります。まず、P、P* に限らず、これら二つの命題は T ├ φ ⇔ T* ├ φ が成り立つ任意の基本言語の理論 T、拡張言語の理論 T* に関する命題に読み替えてください。

スマートコン @mr_konn

@alg_d その上で、「拡張言語の論理式 Φ(A_1,…,A_n) の、{x_i | Ψ_i(x_i)} に関する基本インスタンス」というのは、P*├Φ({x_1|Ψ_1(x_1)},…,{x_n|Ψ_n(x_n)}) と P ├φ が同値になるような基本言語の論理式の事です。

スマートコン @mr_konn

@alg_d こういった論理式が存在する事は、論理式の長さと、クラス項の重みつき出現回数のペアに辞書式順序を入れて、それについての帰納法で簡単に証明出来ます（面倒なのでこれは示しません）！

スマートコン @mr_konn

@alg_d つまり、件の命題の主張は、基本言語の命題に関して同等な証明能力を持つ体系 T, T* に対し、もし T* に拡張言語で書かれた公理を追加するのは、それの任意のクラス項に対する基本インスタンスを T にも追加するのと同じ効果を持つ、ということです

V-alg-d（ZZ） @alg_d

@mr_konn そんなものが存在するんですね、すごい ! ! 色々とありがとうございました。

スマートコン @mr_konn

@alg_d いえいえ、こちらこそあまり簡潔に説明出来ず済みません……！

V-alg-d（ZZ） @alg_d

@alg_d @mr_konn 最後に、連続ツイートするときはこうやって自分にリプすると話を追いやすいし、トゥギャりやすいのでトゥギャッタラーが喜びますよ。

スマートコン @mr_konn

@alg_d 途中で気付いたんですが、最初からやってなかったので後の祭でした！次からそうします！トゥギャ期待してます！

@ta_shim_at_nhn

@mr_konn @alg_d この証明は、ゲーデルの本にある体系の公理 E (global choice) を弱めたに体系に適用できるでしょうね。

スマートコン @mr_konn

@ta_shim_at_nhn そんな公理があるんですね……！

@ta_shim_at_nhn

@mr_konn NBG の他の公理で存在を保証されるクラスはクラス項の導入で記述できると思いますが、これは無理ですからね。

スマートコン @mr_konn

@ta_shim_at_nhn なるほどー。

@ta_shim_at_nhn

@mr_konn @alg_d この証明は次が元となっていると思います。 Joseph R. Shoenfield, A Relative Consistency Proof. JSL 19, No. 1 (1954) pp. 21-28.

@ta_shim_at_nhn

@ta_shim_at_nhn @mr_konn @alg_d Jech には、この方法で AC を除いた BG が ZF の conservative extension であることがわかる。BGC/ZFC については、さらに forcing を使って証明できるとあります。