⊆と外延性公理
〇健全な研究室
さトぅー
「先に道具を揃えるわ。
ペアノ算術のときに、証明の終盤で∀inを連続して使う局面が何回かあったわよね」
エーリル
「あったあった」
さトぅー
「面倒くさいから、一気に∀を付けられるようにする。
天々城がAAelとか適当に名前を付けちゃったからそれに合わせてAAinって呼ぶことにするわね」
■meta thm3.0(AAin)
T:公理系
φ:論理式
すべての自然数nについて、
T |- φ で φを結論とする仮定かつ公理の自由変数に変数記号x_0,...,x_nが含まれない
ならば
T |- (∀x_n ...(∀x_0 φ)...)
proof
数学的帰納法で証明する。
・n = 0のとき、
T |- φ で φを結論とする仮定かつ公理の自由変数に変数記号x_0が含まれないとすると
1 φ [Tの定理]
2 (∀x_0 φ) [∀in 1]
よって、T |- (∀x_0 φ)。
・n = kのとき、
T |- φ で φを結論とする仮定かつ公理の自由変数に変数記号x_0,...,x_kが含まれない
ならば
T |- (∀x_k ...(∀x_0 φ)...)
とする。
n = (k+1)のとき、
T |- φ で φを結論とする仮定かつ公理の自由変数に変数記号x_0,...,x_k,x_(k+1)が含まれないとすると、φを結論とする仮定かつ公理の自由変数に変数記号x_0,...,x_kが含まれない。
ゆえにT |- (∀x_k ...(∀x_0 φ)...)だから、
1 (∀x_k ...(∀x_0 φ)...) [Tの定理]
2 (∀x_(k+1) (∀x_k ...(∀x_0 φ)...)) [∀in 1]
よってT |- (∀x_(k+1) (∀x_k ...(∀x_0 φ)...))。
数学的帰納法から、すべての自然数nについて、
T |- φ で φを結論とする仮定かつ公理の自由変数に変数記号x_0,...,x_nが含まれない
ならば
T |- (∀x_n ...(∀x_0 φ)...)
■
さトぅー
「これで仮定を確認して問題なければ一気に∀を付けられるわね」
エーリル
「すごい楽だ」
さトぅー
「集合論の公理系は結構長い。
道具が揃えばちょっと短くできるから、ひとまず道具を揃えることを優先したいと思う」
エーリル
「OK」
天々城
「最初に全部紹介するのかと思ってたが、確かにそっちの方が楽だナ」
さトぅー
「空集合や和集合があると記述が便利だからね。
準備ができればまとめるつもり」
天々城
「なるほどナ」
さトぅー
「まずは部分集合を定義する」
■部分集合⊆の定義
x,A,B:変数記号
∈:項数2の関係記号
(A⊆B) :⇔ (∀x ((x∈A)⇒(x∈B)))
さトぅー
「(A⊆B)を『AはBの部分集合』とか読むけど、要はBの一部分になってるってだけ」
エーリル
「そのままって感じ」
さトぅー
「特に公理系がなくても⊆でわかることがある」
■thm3.1(⊆の反射性)
S:変数記号
{} |- (∀A (A⊆A))
proof
x:変数記号
1 ((x∈A)⇒(x∈A)) [⇒の反射性]
2 (∀x ((x∈A)⇒(x∈A))) [∀in 1]
3 (A⊆A) [def⊆ in 2]
4 (∀A (A⊆A)) [∀in 3]
■
■thm3.2(⊆の推移性)
A,B,C:変数記号
{ } |- (∀A (∀B (∀C (((A⊆B)∧(B⊆C))⇒(A⊆C)))))
proof
x:変数記号
1 ((A⊆B)∧(B⊆C)) [ax]
2 (A⊆B) [∧elR 1]
3 (∀x ((x∈A)⇒(x∈B))) [def⊆ el 2]
4 ((x∈A)⇒(x∈B)) [∀el 3]
5 (B⊆C) [∧elL 1]
6 (∀x ((x∈B)⇒(x∈C))) [def⊆ el 5]
7 ((x∈B)⇒(x∈C)) [∀el 6]
8 ((x∈A)⇒(x∈C)) [⇒の推移性 4,7]
9 (∀x ((x∈A)⇒(x∈C))) [∀in 8]
10 (A⊆C) [def⊆ in 9]
11 (((A⊆B)∧(B⊆C))⇒(A⊆C)) [⇒in 10 el 1]
12 (∀A (∀B (∀C (((A⊆B)∧(B⊆C))⇒(A⊆C))))) [AAin 11]
■
エーリル
「反射性と推移性はすぐ証明できるのか。
確かに言われてみればそうだ」
さトぅー
「ここで公理を追加する。
集合論の初期装備って感じかしら」
■外延性公理
x,A,B:変数記号
(∀A (∀B ((∀x ((x∈A)⇔(x∈B)))⇒(A = B))))
さトぅー
「外延性公理はAとBの中身が全部一緒なら、AとBは同じって感じかな」
クアトロドルフ
「それは自明じゃないのかい？
中身が全部一致したら同じ集合だと思うんだ」
天々城
「中身が一緒でも、入れ物がビニール袋とダンボール箱じゃ入れ物が違うだろ？
外延性公理を採用したら、それが起きないと言っている」
クアトロドルフ
「ああ、今のでわかったよ。
中身の状態が入れ物まで影響するんだね」
さトぅー
「まあ、そんな感じでいいんじゃない？」
■thm3.3(⊆の反対称性)
A,B:変数記号
{外延性公理} |- (∀A (∀B (((A⊆B)∧(B⊆A))⇒(A = B))))
proof
1 ((A⊆B)∧(B⊆A)) [ax]
2 (A⊆B) [∧elR 1]
3 (∀x ((x∈A)⇒(x∈B))) [def⊆ el 2]
4 ((x∈A)⇒(x∈B)) [∀el 3]
5 (B⊆A) [∧elL 1]
6 (∀x ((x∈B)⇒(x∈A))) [def⊆ el 5]
7 ((x∈B)⇒(x∈A)) [∀el 6]
8 ((x∈A)⇔(x∈B)) [⇔in 4,7]
9 (∀x ((x∈A)⇔(x∈B))) [∀in 8]
10 (∀A (∀B ((∀x ((x∈A)⇔(x∈B)))⇒(A = B)))) [外延性公理]
11 ((∀x ((x∈A)⇔(x∈B)))⇒(A = B)) [AAel]
12 (A = B) [⇒el 9,11]
13 (((A⊆B)∧(B⊆A))⇒(A = B)) [⇒in 12 el 1]
14 (∀A (∀B (((A⊆B)∧(B⊆A))⇒(A = B)))) [AAin 13]
■
エーリル
「外延性公理から⊆の反対称性もできた」
さトぅー
「⊆の反対称性から外延性公理も証明できるんだけどね。
自明だけど、外延性公理の⇒を⇔にできる」
■thm3.4
x,A,B:変数記号
∈:項数2の関係記号
{外延性公理} |- (∀A (∀B ((∀x ((x∈A)⇔(x∈B)))⇔(A = B))))
proof
1 (∀A (∀B ((∀x ((x∈A)⇔(x∈B)))⇒(A = B)))) [外延性公理]
2 ((∀x ((x∈A)⇔(x∈B)))⇒(A = B)) [AAel 1]
3 (A = B) [ax]
4 ((x∈A)⇔(x∈B)) [論理式の代入原理 3]
5 (∀x ((x∈A)⇔(x∈B))) [∀in 4]
6 ((A = B)⇒(∀x ((x∈A)⇔(x∈B)))) [⇒in 5 el 3]
7 ((∀x ((x∈A)⇔(x∈B)))⇔(A = B)) [⇔in 2,6]
8 (∀A (∀B ((∀x ((x∈A)⇔(x∈B)))⇔(A = B)))) [AAin 7]
■
エーリル
「ただの代入ゲーだった」
さトぅー
「こっちを集合論の公理に採用するときもあるけど、できるだけ弱い公理になると⇒のバージョンかしらね。
あとは、証明でよく使う道具でこれじゃないかな」
■thm3.5
x,A,B:変数記号
∈:項数2の関係記号
{} |- (∀A (∀B (∀x (((x∈A)∧(A⊆B))⇒(x∈B)))))
proof
1 ((x∈A)∧(A⊆B)) [ax]
2 (A⊆B) [∧elL 1]
3 (∀x ((x∈A)⇒(x∈B))) [def⊆ el 2]
4 ((x∈A)⇒(x∈B)) [∀el 3]
5 (x∈A) [∧elR 1]
6 (x∈B) [⇒el 5,4]
7 (((x∈A)∧(A⊆B))⇒(x∈B)) [⇒in 6 el 1]
8 (∀A (∀B (∀x (((x∈A)∧(A⊆B))⇒(x∈B))))) [AAin 7]
■
天々城
「実家のような安心感で使うナ、これ」
さトぅー
「ホントよく使うわよね」
クアトロドルフ
「いや、自明だろう？」
さトぅー
「証 明 で き る な ら ね」
クアトロドルフ
「アッハイ」
