2024.09.04
https://gyazo.com/d895bff63cd8e54da80b757363693014
前：2024.09.03
後：2024.09.05
#日報
読んだ
R. Kashima, Y. Kato; 2022; "Semantical Cut-Elimination for the Provability Logic of True Arithmetic"
読んだけど証明がザックリすぎてあんまり分からないな…と思ってしまった
first-level sequentで$ \bf GLをやってsecond-level sequentで$ \bf KTを入れるというのはおもしろいなと思った
思った
「テスト文字列に”うんこ”と入れるな」の5倍ひどいものが内々のプロジェクトに突っ込まれているがやったのが自分でしかないから自分で頭抱えてる
メモ　
第2不完全性定理の形式化（すなわち$ T \nvdash \mathrm{Con}_Tと$ T \nvdash \lnot \mathrm{Con}_T）が終わったらしい。
めでたい
パッと見た感じCobhamの最弱の算術$ \mathbf{R_0}の上で議論しているように見えた。
詳しいことは後で見ることにしよう
思った
GLのデネセシテーション
デネセシテーションを持つ論理で$ \bf KTの拡張でない論理って$ \bf GL以外にもさすがにあると思うけど具体例を知らない
メモ
5年間もScrapboxで日報書いてるのに面倒すぎて日報作成用のボタンを設置しておらず、逆にみんな何故あるんだと思う
思った
R. Goré, R. Ramanayake; 2008; "Valentini's Cut-Elimination for Provability Logic Resolved"を読もうと思ってこれを実装しようと思ったけどそういえばもうこれ自体はあるんだった
R. Gore, R. Ramanayaka, I. Shillito; 2021; "Cut-Elimination for Provability Logic by Termination Proof-Search: Formalized and Deconstructing Using Coq"