表示調整
閉じる
挿絵表示切替ボタン
▼配色
▼行間
▼文字サイズ
▼メニューバー
×閉じる

ブックマークに追加しました

設定
0/400
設定を保存しました
エラーが発生しました
※文字以内
ブックマークを解除しました。

エラーが発生しました。

エラーの原因がわからない場合はヘルプセンターをご確認ください。

ブックマーク機能を使うにはログインしてください。
エルフに数学を装備するだけ  作者: めいぜんおーえす
五章:そして集合へ
51/51

⊆と外延性公理

〇健全な研究室


さトぅー

「先に道具を揃えるわ。

 ペアノ算術のときに、証明の終盤で∀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」


天々城

「最初に全部紹介するのかと思ってたが、確かにそっちの方が楽だナ」


さトぅー

「空集合や和集合があると記述が便利だからね。

 準備ができればまとめるつもり」


天々城

「なるほどナ」


さトぅー

「まずは部分集合を定義する」




部分集合(subset)⊆の定義

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]




エーリル

「反射性と推移性はすぐ証明できるのか。

 確かに言われてみればそうだ」


さトぅー

「ここで公理を追加する。

 集合論の初期装備って感じかしら」



外延(axiom)( of )(extensi)(onality)

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]



天々城

「実家のような安心感で使うナ、これ」


さトぅー

「ホントよく使うわよね」


クアトロドルフ

「いや、自明だろう?」


さトぅー

「証 明 で き る な ら ね」


クアトロドルフ

「アッハイ」

評価をするにはログインしてください。
ブックマークに追加
ブックマーク機能を使うにはログインしてください。
― 新着の感想 ―
このエピソードに感想はまだ書かれていません。
感想一覧
+注意+

特に記載なき場合、掲載されている作品はすべてフィクションであり実在の人物・団体等とは一切関係ありません。
特に記載なき場合、掲載されている作品の著作権は作者にあります(一部作品除く)。
作者以外の方による作品の引用を超える無断転載は禁止しており、行った場合、著作権法の違反となります。

この作品はリンクフリーです。ご自由にリンク(紹介)してください。
この作品はスマートフォン対応です。スマートフォンかパソコンかを自動で判別し、適切なページを表示します。

↑ページトップへ