2024.12.09
https://gyazo.com/d8624fa39ffddf1854f254a4c1d539eb
業務連絡
がんばるぞーがんばるぞー
寄せられた数々の期待のコメント
やった
$ Tは無矛盾とする．以下，解釈は標準的な証明可能性述語$ \mathrm{Pr}_T上のものを考えるとする．．
木モデル$ M := \lang \{0,\dots,n - 1\}, R, V\rangとする．
任意の$ Mに対してSolovay sentences$ \varphi_0,\dots,\varphi_nが構成できる．
remark:Solovay sentencesは$ Mのworldの数 + 1個作る．
proof
がんばれ！
補題1（証明済み）
$ MのSolovay Sentencesを$ \Phi := \varphi_0,\dots,\varphi_nとし，$ i \neq 0とする．$ *を$ \Phiに基づく解釈とする． 1. $ i - 1 \vDash A \implies T \vdash \varphi_i \to A^*
2. $ i - 1 \nvDash A \implies T \vdash \varphi_i \to \lnot A^*
補題2（証明済み）
$ 0 \vDash A \implies T \vdash \varphi_1 \to \lnot A^*
proof:補題1で$ i = 1とすればよい．
補題3
$ Mの単純拡張モデル$ M' := \lang \{-1,0,\dots,n-1\}, R', V' \rangとする．
$ M'のSolovay Sentences$ \Phi := \varphi_{-1},\varphi_0,\dots,\varphi_nを取り，$ *は$ \Phiに基づく解釈とする． $ M, 0 \nvDash Aなら，$ T \nvdash A^*．
proof
まず$ M'は単純拡張モデルなので，$ M, 0 \nvDash Aなら$ M',-1 \nvDash A．
補題2より$ T \vdash \varphi_0 \to \lnot A^*．
ここで1つズレているのでよい．
仮に$ T \vdash A^*だと仮定すると，$ Tは無矛盾なので$ T \vdash \lnot \varphi_0．
Solovay sentencesの条件4より$ -1 R' 0なので$ T \vdash \mathrm{Pr}_T(\ulcorner \lnot \varphi_{0} \urcorner) \to \lnot \varphi_{-1}．
条件4: $ i R j \implies T \vdash \mathrm{Pr}_T(\ulcorner \lnot \varphi_j \urcorner) \to \lnot \varphi_i
導出可能性条件D1より$ T \vdash \mathrm{Pr}_T(\ulcorner \lnot \varphi_{0} \urcorner)なので上と合わせて$ T \vdash \lnot \varphi_{-1}．
Solovay sentencesの条件1を踏まえると，$ T \vdash \bigvee_{-1 R' i} \varphi_i．
条件1: $ T \vdash \bigvee_i \varphi_i
$ -1 R' iな任意の$ iについて，$ d(i) \leq d(0)に注意すると，$ M', i \vDash \Box^{d(0) + 1} \botが成り立つ．
$ d(w)は$ wから行ける最も遠いworldまでのステップ数とする．
$ \Box^{d(0) + 1}の評価には$ iから$ d(0) + 1歩先のworldを見る必要があるが，今そのようなworldは存在しないので，無条件に$ \Box^{d(0) + 1} \botが成り立つ．
補題1より，$ T \vdash \varphi_i \to (\Box^{d(0) + 1} \bot)^*．
これと$ T \vdash \bigvee_{-1 R' i} \varphi_iと$ iの取り方を合わせると，$ T \vdash (\Box^{d(0) + 1} \bot)^*が言える．
さて，$ (\Box^{d(0) + 1} \bot)^* \equiv \underbrace{\mathrm{Pr}_T \cdots (\ulcorner \mathrm{Pr}_T (\ulcorner}_{d(0) + 1} \bot \urcorner) \cdots \urcorner)は$ \Sigma_1文であるから，$ \Sigma_1健全性より$ T \vdash (\Box^{d(0)} \bot)^*が言える．同様に包んでいる証明可能性述語をどんどん外していくと，最終的に$ T \vdash \botが言える．
しかし$ Tは無矛盾だったので，これはおかしい．❏ 定理: $ \bf GLの算術的完全性
任意の解釈$ *で$ T \vdash A^*なら，$ \mathbf{GL} \vdash A．
proof
対偶を示す．
$ \mathbf{GL} \nvdash Aならばある木モデル$ Mが存在してその根$ 0で$ M,0 \nvDash A．
補題3の解釈$ *の上では$ T \nvdash A^*が成り立つ．よって示された．❏ ちょっと中身書いた
英語を書くのは面倒くさいのでやめたい
メモ
否定が証明出来ることと証明できないことについて
$ \vdash \lnot \varphi \stackrel{?}{\iff} \nvdash \varphi
排中律$ \varphi \lor \lnot \varphiがあったとしてもこれは出ない（はず？）
$ \implies側はキャンセル則$ \vdash \varphi \lor \psi, \nvdash \varphi \implies \vdash \psiによって出る
キャンセル則という規則はない．
思った
もう廃棄したプロジェクトのつもりだったのだけどもこうなってくるとやる気が出てくる
思った
手が8個無いと足りないぐらい忙しくなりつつある
思った
なんか下手にやると帰納法めっちゃ面倒くさいことになる気がするのだが…
でもやらないと$ \bf Kのシークエント計算しか出来ませんよ
う～ん…
思った
Vercelに$30払わないとOTOMADBのWebフロント側を動かせない（しかも移行作業がある）のにAPIが動いているVultrのサーバーを動かしっぱなしにして$10ぐらい取られたの普通に不愉快になってきた
メモ
証明論シンポジウム2024の「証明論」が指す温度感がわかっていなくて行くのを止めたのだけども，今プログラム見たら面白そうな内容が並んでいたので予定を組み直して行こうかなという気持ちになっている とりあえず明日決めよう
行くことにしました
メモ
こんな大体に2極化するんだ