2023.11.11
https://www.youtube.com/watch?v=UYnElsxZveY
Roller Skate Shoes
公開時当時はアーリーアダプターバージョンらしいが，ちょっとほしいなと思った．
前：2023.11.10
後：2023.11.12
#日報
いいね
Rollerblading w/ Montre Livingston
https://www.youtube.com/watch?v=sqodUS48U54
#ローラースケート
観るまで知らなかったけど，グラインドするためにはグラインド専用のパーツやホイールをシューズ側に取り付け/切り替えないと行けないのかと思った．
メモ
循環証明に関しては前チラッと見たので今見返している
循環シークエント計算と循環証明体系と区別しちゃったの良くない気がいしてくる
知った?
私はAmazonの購入履歴から推定するに最低でも600L以上コーラを飲んでいる人間だから全然知らなかったのですが、一般には炭酸の抜けたコーラは美味しくないものとして扱われるらしいです。そうなんですか？
https://twitter.com/SnO2WMaN/status/1723259789927661573
やった
循環シークエント計算について．
D. Shamkanov; 2018; "Circular Proofs for the Gödel-Löb Provability Logic"を読んだりした．
K4の循環シークエント計算体系とGLのシークエント計算は証明能力が同じ
知った
https://www.nagatoro.gr.jp/2023/11/%E3%80%8C姫坂乃愛誕生日イベント%E3%80%8D開催決定%EF%BC%81/
姫坂乃愛
なぜ？
メモ: 直観主義様相論理の慣習的な扱いの違いについて
直観主義様相論理iKについて，衝撃の事実が発覚した
A. Das, I. van der Giessen, S. Marin; 2023; "Towards Intuitionistic Gödel-Löb Logic (with a capital 'I')"より
出版的にA. Das, I. van der Giessen, S. Marin; "Intuitionistic Gödel-Löb logic, à la Simpson: labelled systems and birelational semantics"にも少し書いてあるかもしれない．
$ \Boxの他に$ \Diamondをどう扱うかによって直観主義様相論理としての扱い（や慣習的な表記が）変わるらしい．
intuitionistic modal logics. $ \sf i\Lambda
intuitionistic modal logics (often prefixed by a small $ \sf i), e.g., $ \sf iK. These logics are defined over the language with only $ \Box.
M. Božić & K. Došen; 1984; "Models for Normal Intuitionistic Modal Logics", F. Wolter, M. Zakharyashchev; 1997; "On the Relation between Intuitonistic and Classical Modal Logics"などが先行研究としてあり，T. Litak; 2015; "Constructive Modalities with Provability Smack"がサーベイ論文．
それぞれ$ \mathbf{IntK_\Box}, \mathbf{HK}_\Box, \mathsf{K^i}となっている．
今日日$ \sf iをprefixするのは10, 1, 7などの影響らしい．
区別するときどうするのだろう？少なくとも日本語だとどうしようもない気がする．素朴な直観主義様相論理とでも言えば良いのか？
Constructive modal logics. $ \sf C\Lambda
Constructive modal logics (often prefixed by a capital $ \sf C), e.g., $ \sf CK. These logics are defined over $ \Box and $ \Diamond and their $ \Box-fragment typically coincides with its small $ \sf i version
G. Bellin, V. de Paiva, E. Ritter; 2003; "Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic", M. Mandler, V. de Paiva; 2005; "Constructive CK for contexts"
Constructive Modal Logic（構成的様相論理とでも訳すのがいいだろうか？）
$ \Box断片は$ \sf iとして扱われる．
Intuitionistic modal logics. $ \sf I\Lambda
Intuitionistic modal logics (often prefixed by a capital $ \sf I), e.g., $ \sf IK. These logics are defined over the language with $ \Box and $ \Diamond. They typically validate the standard translation into first-order logics, intuitionistically, and the addition of excluded middle yields their classical counterpart. Their $ \Box-fragment extends the small i version.
G. Fischer-Servi; 1977; "On modal logic with an intuitionistic base"
より調査はA. K. Simpson; 1994; "The Proof Theory and Semantics of Intuitinistic Modal Logic"で行われている．
この場合でも，$ \Box断片は$ \sf iとして扱われる．