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

スマートコン @mr_konn

集合論ゼミ、クラスありの拡張言語が生の集合論と証明能力が変わらない、と云う事の証明を何処まで追うべきか迷ってる。あんま細かくやると証明論だし、本筋そこじゃないからまあAppendixに書いてあるんでってことで概略だけにしよう

V-alg-d（ZZ） @alg_d

@mr_konn ミスターその証明教えて～～～～～

スマートコン @mr_konn

@alg_d 頑張るとわかる■

V-alg-d（ZZ） @alg_d

@mr_konn 深い!!

スマートコン @mr_konn

@alg_d えっへん

V-alg-d（ZZ） @alg_d

ミスターの証明が天才的過ぎて今の僕には理解できない。

V-alg-d（ZZ） @alg_d

@mr_konn 頑張り方を詳しく。

スマートコン @mr_konn

@alg_d 証明図の気持ちになって頑張る■

V-alg-d（ZZ） @alg_d

@mr_konn ミスターは証明図の気持ちも分かるの、すごい。

スマートコン @mr_konn

@alg_d この証明図は正規化されたがってます！！！感じるんです！！！！

V-alg-d（ZZ） @alg_d

@mr_konn ｷｪｪｪｪ

V-alg-d（ZZ） @alg_d

@mr_konn 実際の所どうやって証明するんでしょう。

スマートコン @mr_konn

@alg_d 恰度いまアウトライン纏めおわったので簡単に説明します。記述力が同等なのは明らかなので証明力ですね。以下、P を生の集合論、P* を自由クラス変数を認めた拡張言語の理論とします。特に、集合論の公理としては外延性公理くらいしか仮定しないです

スマートコン @mr_konn

@alg_d 以下、P の論理式は小文字ギリシャ文字、P* の論理式は大文字ギリシャ文字で表します。まず P ├ φ ⇔ P* ├ φ を示しますが、(⇒) は公理や適切な置換規則からすぐ出て来ます。(⇐) は、P* での証明木を考えて、それを「正規化」して考えます。

スマートコン @mr_konn

@alg_d 正規な証明木というのは、公理から出発して前半でに置換規則（P(A) から P(x) を推論するような）を、後半でModusPonensと汎化規則を適用するような証明木です。

スマートコン @mr_konn

@alg_d 一般に、P* で証明可能な命題は P* で正規な証明木を持ちます。置換規則より上に出て来るMPと汎化規則の回数に関する帰納法でこれは容易に示せます。これを使って逆向きが示せます。

スマートコン @mr_konn

@alg_d P* ├ φ とします。正規な証明木があるので、そいつを持ってきます。出発点の公理群に一通り置換規則を適用し終えて、残ったクラス変数を {x | x = x} に置き換えてクラス変数を無くした状態にして、これを source formula とよぶことにします。

スマートコン @mr_konn

@alg_d クラス変数を含まない論理式 Γ に対して、再帰的に書き換えて基本言語の論理式にしたものを、Γ の基本化 b(Γ) と呼ぶことにします。クラス項を含まなければそのままだし、含む原始式なら Γ(y∈{x|Φ(x)}) = Γ(Φ(y)) みたいにして、結合子はバラす。

スマートコン @mr_konn

@alg_d そうして、P* における φ の証明図に出て来る論理式を基本化します。これは P での証明図の骨格みたいなものになっています。source formula の基本化は実は P の定理になっているので、これで P での証明図が得られました■

V-alg-d（ZZ） @alg_d

@mr_konn ふぇぇ

スマートコン @mr_konn

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

スマートコン @mr_konn

@alg_d 二番目のは簡単で、T ∪ Q ├ φ というのは有限個の基本言語の論理式 χ_i で T ∪ {χ_1,…,χ_n} ├ φ とかけることと同値で、これは T ├ χ_1∧…∧χ_n→φ と同値。仮定から T* ⊦ が云えて……と云う感じです。逆も同様。

スマートコン @mr_konn

@alg_d 最後の命題についても殆んど同様の議論で示せます。はい。

スマートコン @mr_konn

あるごどぅーパイセンに明日のゼミの練習をしてもらったぞ(((o(^^)o)))