2023.10.27
https://gyazo.com/1a6ca2894ff2a3ea9723d464c4abbd5b
前：
2023.10.26
後：
2023.10.28
#日報
知った
様相論理GLS
$ \sf GLS
の
$ \sf S
は
Robert M. Solovay
に由来するらしい．
H. Kushida; "A proof theory for the logic of provability in true arithmetic"
メモ
行為が名前になっている料理
油揚げ
って行為なのに食材の名を冠してて無法すぎる
まとめた
ドナルド・マクドナルド in アニメ
アニメに出てくるドナルドの情報を
2
3件持ってる謎の人間なんなんだ
まとめた
様相論理の濾過法
証明可能性論理GLは決定可能
非反射性は正規様相論理で定義出来ない
連絡
東京に行きます．
LOLISTYLE GABBERS
のリリースパーティにだけ…
メモ
lambda.luma.dev
https://lambda.luma.dev/
Rust
による?
TaPL
の実装．
Calculus of Constructions
と
System Fω
，
型無しλ計算
がある．
https://twitter.com/lumc_/status/1717515559741571545
処理系の実装は
Rust
で、
wasm
で動いています
エディタは
monaco
です
メモ
R. Kashima, T. Kurahashi, S. Iwata; "Cut-free sequent calculi for the provability logic D"
証明可能性論理D
の
シークエント計算
と
カット除去定理
について
鹿島先生って
カット除去定理
のことしか考えてないの？
思った
証明体系
を表す記号を自分の中で統一したい．
鹿島 亮; "コンピュータサイエンスにおける様相論理"
では独自に論理
$ \Lambda
に対して
Hilbert流演繹体系
$ \mathcal{H}_\Lambda
，
シークエント計算
を
$ \mathcal{S}_\Lambda
としていた．
\cal
は
様相論理
などのモデルとして使いたいのでやめたい．
となると
\frak
あたりか？
様相論理GL
の
Hilbert流演繹体系
$ \mathfrak{H}_\mathsf{GL}
証明可能性論理GLのシークエント計算体系
$ \mathfrak{S}_\mathsf{GL}
ウ〜ム…
普通に
$ ()
で囲めばいいのでは
$ \mathfrak{S}(\mathsf{GL})
長いな
カットなし証明体系は
$ ^c
を添字付ける