2023.07.04
https://gyazo.com/b53a665ac803a6b654196d34f747a750
このサムネ怖すぎる
メモ
読んだ
だいぶ早いな
木原貴行の計算可能性に基づく数学の厳密化などの話しおもしろかった 思った
個人的にはイーロン・マスクが全ての元凶か?と言われればなんかそれも若干怪しい気はする このまま腐り落ちて突然死ぬよりかは,誰かがナタを振り下ろす必要があったのだとは思う.
それはそれとして態度が悪い?という問題はある
論理記号を$ \toと$ \lnotだけとして矛盾命題$ \botを$ \lnot(p_0→p_0)で導入する方法あまり好きではなくまた形式化にあたって面倒そうという気がして、
$ \toと$ \botで$ \lnot\varphiを$ (\varphi\to\bot)とする方を取るけど毎回何かしら失敗しているので実はあまり良くないのかも知れない
Lean 4のSetのSingleton意味不明にsimpを要求されてる気がする 色々面倒ですね
Henkin流の完全性定理?では極大無矛盾な集合を考えるけど,形式化してるときにあたってよく考えると極大性って本当にいるのか?と思って読み直してる.少なくとも命題論理においては $ \Gammaは無矛盾とする.
論理式は列挙出来るとする.
$ \varphi_0,\varphi_1,\varphi_2,\dots
$ \varphi_0 \equiv \bot
$ \varphi_{2k + 1} \equiv p_k
$ \varphi_{2k + 2} \equiv \varphi_{k_1} \to \varphi_{k_2}ただし$ k \coloneqq \lang k_1,k_2\rang
$ \Gamma_0 \coloneqq \Gamma
$ \Gamma_{n+1} \coloneqq \begin{cases} \Gamma_n + \varphi_n & \text{$\Gamma_n+\varphi_n$ is consistent} \\ \Gamma_{n} + \lnot\varphi_{n} & \text{otherwise} \end{cases}
若干定義を変えた($ \Gamma_n + \lnot\varphi_nについて).もしかしたらこれはよくないのかもしれない
かなり良くない気がしてきた.$ \varphi_{\lang n,0 \rang} \equiv \lnot\varphi_{n},$ n \leq \lang n,0\rangで無駄手間な気がする
このとき任意の$ nについて$ \Gamma_nは無矛盾.
$ \Deltaが無矛盾$ \implies任意の$ \varphiについて$ \Delta+\varphiまたは$ \Delta+\lnot\varphiのどちらかは無矛盾.などより
$ V_\Gamma(\varphi_{n}) = \mathbf{T} \iff \varphi_{n} \in \Gamma_{n+1}とすると
$ V_\Gammaは真理値関数としての性質を満たすか?
$ V_\Gamma(\lnot\varphi_n) = \mathbf{T} \iff V_\Gamma(\varphi_n) = \mathbf{F}?
$ V_\Gamma(\varphi_n \to \varphi_m) = \mathbf{T} \iff V_\Gamma(\varphi_n) = \mathbf{F} ~\text{or}~ V_\Gamma(\varphi_m) = \mathbf{T}?
SnO2WMaN.iconこれらを示せば良いはずなんだが
なお付値関数としては
$ v(p_k) = \mathbf{T} \iff \text{$\Gamma_{2k+1} + \varphi_{2k+1}$ is inconsistent}
とすれば良い.はず…
知った
Over the past weeks, we have been working on a user-editable wiki, DB, and discussion board for 音MAD/YTPMV, with hopes to make it the most complete archive to date, and provide the DB for anyone to download. When this is available, I will permanently be shutting down this bot.