2023.10.18 - Internet Explorer 2.0

2023.10.18

https://www.youtube.com/watch?v=UJiP8MwFmAw

メモ

https://nicothumb2img.vercel.app/image/sm8702#.png https://nico.ms/sm8702

Lzieのmixで聴いた覚えあるんだけどどこだったかなと思って必死に思い出した

知った

放送大学に図書館があること

一般の人は閲覧が可能で，卒業生は貸出も可能であること

メモ

これのpdfではGentzenのオリジナルのシーケント計算体系をシークエント計算体系G1$ \bf G1と読んでおり，それを少し改造した体系をシークエント計算体系G3$ \bf G3と読んでいる．

シークエント計算体系G2はなんなのか？そもそも誰が言ってるのか？はよくわからない．

タブロー計算に興味が出てきた．何が違うのだろうか？

ツイートまとめ

16bitセンセーション，今やってるアニメとは全く関係なくMOSAIC.WAVが歌ってる曲があるのどういうことなんだ

https://open.spotify.com/album/6jZUBpbo1MxxG75HvRXPQE?si=MMJquzsaR9ur9uMFnRlSsw

証明可能性述語が存在する算術が、不動点補題を満たし導出可能性条件/形式化された完全性定理などを満たすなら不完全性定理やLöbの定理などが証明できるという事実をLean 4で形式化していた（どうやって可証性述語をとったりそのような条件を満たすかを示すかは一切触れていない）