ZFでの空集合の存在
https://www.youtube.com/watch?v=wbgLmx1jNtU&list=PLeBc8K3RvbSx0LPXBYDgZvE_uFcVhx7Ym&index=3
$ ZF \vdash \exist y \forall x ( x\notin y )
これを「空集合が存在する」と読めるのは、勝手にそう読んでるだけ
実際は単なる有限文字列
形式的証明の存在を確認する
命題
$ \varphiがTの元のとき、$ T \vdash \varphi
証明
注意
$ \vdash の左側は集合を書くが、元を置く書き方もする
$ \varphi \vdash \psi \rarr \varphi
これは、厳密には
$ \{ \varphi \} \vdash \psi \rarr \varphi
命題
$ \varphi \vdash \psi \rarr \varphiである
証明
有限列
$ \varphi, \varphi \rarr (\psi \rarr \varphi), \psi \rarr \varphi
これがその証明
$ \varphiは公理
$ \varphi \rarr (\psi \rarr \varphi)は基本公理 命題
$ \neg \varphi \vdash \varphi \rarr \psi
証明
1. $ \neg \varphi 公理
2. $ \neg \varphi \rarr (\neg \psi \rarr \neg \varphi) 基本公理
3. $ \neg \psi \rarr \neg \varphi 直ちに導かれる 1,2より
4. $ (\neg \psi \rarr \neg \varphi) \rarr (\psi \rarr \varphi) 基本公理
5. $ \psi \rarr \varphi 3,4より直ちに導かれる
https://scrapbox.io/files/68eb7671c5b4c7553ade1590.png
命題
$ \neg \psi \to \neg \varphi \vdash \varphi \to \psi
要するに対偶
証明
証明図をインデントで表現してみるかmiyamonz.icon
$ \varphi \to \psi MP
$ \neg \psi \to \neg \varphi 公理
$ (\neg \psi \to \neg \varphi ) \vdash (\varphi \to \psi) 基本公理
命題
$ \varphi \to \psi, \psi \to \chi \vdash \varphi \to \chi
https://scrapbox.io/files/68eb780da5e84ba8bb5c8b57.png
他にも
https://gyazo.com/4650bbaf88fc56240230aa6e0701d27d
排中律
同じ仮定は複数でも１つでも同じ
仮定の順番は関係ない
命題
$ \varphi 閉論理式のとき
$ T \cup \{\varphi\} \vdash \psiならば$ T \vdash \{\varphi\} \to \psi
逆もMPから成り立つ
特に$ \varphi \vdash \psiと$ \vdash \varphi \to \psiは同じ
証明
$ T \cup \{\varphi\} \vdash \psiの証明図を考える
https://scrapbox.io/files/68eb79349eb74b7a10392eec.png
これに$ \varphi \toをつけたもの
https://scrapbox.io/files/68eb794b6913155efff9bfda.png
なぜなら
途中の部分は、「直ちに導かれる」を表している
よって２通りの場合を示せばいが
https://scrapbox.io/files/68eb7968ca742e031a1ff219.png
前者
https://scrapbox.io/files/68eb799fb246680525ec38b4.png
基本公理の部分は、$ \psiが閉論理式という仮定があるから使える
後者
https://scrapbox.io/files/68eb79af9a64fb1861656e2c.png
略
以上より
https://scrapbox.io/files/68eb79f7fec205fb24413bf0.png
一番上の部分は
$ \varphi_i \equiv \varphiのとき$ \vdash \varphi \to \varphi_iである
$ \varphi_iがTの元のとき,$ \varphi_i \vdash \varphi \to \varphi_iより$ T \vdash \varphi \to \varphi_i
よって$ T \vdash \varphi \to \psi
以上の命題の、閉論理式の仮定は、証明中にhttps://scrapbox.io/files/68eb7aba8c1ff308bbe046dc.pngが登場したから
よって、これがなければ、閉論理式の仮定は不要
命題
$ \vdash \neg \varphi \to (\varphi \to \psi)
証明
$ \neg \varphi \vdash (\varphi \to \psi)はすでに示した
ここには$ \chi \vdash^{\forall} \forall x \chiはでてこない
前命題と同様にして
$ \vdash \neg \varphi \to (\varphi \to \psi)
https://gyazo.com/afc477b2d9b7bafaf10086d1789fd9a4
または$ \land
二重否定
対偶（さっきのやつの逆向き
かつ$ \land
公理からのかつ
命題
$ \vdash \forall x \varphi \to \varphi
したがって、$ \forall \varphi \vdash \varphi
証明
基本公理
$ \forall \varphi \to \varphi[ x \rightsquigarrow y] より
命題
$ \varphi \to \psi \vdash \forall x \varphi \to \forall x \psi
https://gyazo.com/01ecce18a092d0e4385a900163003db4
否定についても言える
命題
$ \vdash \varphi \leftrightarrow \psi ならば$ \vdash \neg \varphi \lrarr \neg\psi
系
$ \vdash \varphi \leftrightarrow \psi ならば$ \vdash \exists \varphi \lrarr \exists\psi
$ \exists x は$ \neg \forall x \neg という定義だったから
ここまで準備して、やっと空集合の存在を示せる
https://gyazo.com/06b866b2ddb0d01e8b8f81120690936f
まず$ \vdash \varphi_0 \lrarr x \notin yを示す
$ \vdash \varphi_0 \to x \notin y
https://gyazo.com/077a53bd56976f6668b6a0f7aa31dd2f
$ \vdash x\notin y \to \varphi_0
https://gyazo.com/b09755fc8c891bcb31dab48f3c4787f4
https://gyazo.com/f8be64d612da451df5aaa8096b81a4c3
従って$ \vdash \exists y \forall x \varphi_0 \lrarr \exists y \forall x (x\notin y )
右が示したい論理式。よって左を示す
$ \forall z \exists y \forall x ( x \in y \lrarr x \in z \land \varphi )の全称閉包
ここで$ \varphiとして$ x \ne xを考えると
$ \forall z \exist y \forall x \varphi_0となる
https://scrapbox.io/files/68eb7f3320552d8a4f66a0cd.png
途中の定理は別ページにしたいが、良いタイトルがわからんmiyamonz.icon