数学基礎論 (数理論理学) 入門 by alg-d
https://www.youtube.com/watch?v=p3TLn8m3OGM&list=PLeBc8K3RvbSx0LPXBYDgZvE_uFcVhx7Ym&index=1
数学基礎論(数理論理学)入門【選択公理】
【数学基礎論入門】ZFCと形式的証明を定義する
【数学基礎論入門】ZF で ∃y∀x(x∉y) を証明する【形式的証明】
形式的証明における背理法【数学基礎論入門】
【数学基礎論入門】群論なども扱えるようにする回【モデル理論】
書いたmiyamonz.icon
【数学基礎論入門】定義による拡大
【数学基礎論入門】ZFCの公理を紹介します！
集合でない集まり(クラス)をどのように扱うのか【数学基礎論入門】
ZF での超限帰納法(超限再帰)【数学基礎論入門】
見たmiyamonz.icon
数学基礎論における選択公理(もしくは無限の扱いについて)
【ZFC】集合でないことをどうやって証明するか【数学基礎論】
【ZFCでない】クラスを扱える集合論「NBG」を紹介【大域選択公理】
集合でないものも認める集合論「ZFA」を紹介【選択公理】
Peano算術(自然数論)と超準モデル【数学基礎論】
超準モデルと超積とŁośの定理と超準解析【数学基礎論】
選択公理の話をするための「不完全性定理」【数学基礎論】
選択公理の独立性 part 1: 初心者向け説明
選択公理の独立性 part 2: Permutation Model
選択公理の独立性 part 3: Symmetric Model
【集合論】全ての実数の集合をLebesgue可測にする～Solovayモデル入門～【選択公理】
【数学基礎論】関手圏のHomは集合なのか?【圏論ではない】
【数学基礎論】local set theory【直観主義】
【数学基礎論】選択公理⇒排中律【local set theory】
圏論(トポス)と論理(local set theory)の関係【数学基礎論】
【トポス】∀は右随伴である（∃もあるよ！）【圏論】
【数学基礎論】local set theoryで自然数論
読んで勉強するmiyamonz.icon
数学を数学的に考えること
命題や証明などを数学的に定義する
「（ある定理が）選択公理無しで証明できないことを証明する」をやりたい
(ある定理が) ZF では証明できないことを証明する
この２つは違う
上記の使用可能文字の定義に登場する変数は、我々が普段数学で使っている変数 我々が普段やってる数学
ZFという体型の中に出てくる単なる記号としての変数
これから定義する体型 (ZF)
論理式に含まれる変数記号のうち
自由変数が現れない論理式のことを閉論理式 (もしくは文) という． 例
$ (\forall x ( x \in y) \land x = z
左側のxは束縛変数
andの右のxは自由変数
y,zは自由変数
ここらへんの説明はもっと丁寧に定義ができるが、略されている
ここまで動画３まで
形式的証明の背理法
矛盾の定義
定義
このとき、Tが矛盾する
ある閉論理式$ \varphi が存在して$ T \vdash \varphi \land \neg \varphiとなる
定理
Tが矛盾するならば
任意の論理式$ \varphi に対して、$ T \vdash \varphiとなる
つまり矛盾している仮定からは何でも証明できる
爆発律
証明
仮定より
ある閉論理式$ \psi が存在して$ T \vdash \psi \land \neg \psi
左は今の仮定
https://scrapbox.io/files/68eb887788b0bb0498056232.png
よって、$ T \vdash \psi
同様にして、$ T \vdash \neg \psi
https://scrapbox.io/files/68eb88c2c994513bd93f91e7.png
https://scrapbox.io/files/68eb88da88b0bb0498056393.png
~動画4
モデル理論
群の定義の式
３つの定義式から、積の可換性を証明できない
こういう話も数学基礎論で定式化できる
一般の理論を扱うように論理式を定義する
動画5
動画6
定義による拡大
https://gyazo.com/2eb571a7559b991eb2845cb8d855cff3
動画7
ZFCの公理の紹介
動画8
集合でない集まり(クラス)をどう扱うか
クラス
$ \{ x \mid \varphi(x)\}をクラスという
$ \varphi(x)は論理式
しかしこの表記は、論理式じゃない
略記だとみなす
$ x \in M ... $ \varphi_M(x)の略記
クラスを使った論理式的な何かは、クラスを使わない正式な論理式の略記と思うことができる
逆で、そう思える場合にしかクラスは使わない