2025.11.02
https://gyazo.com/7d0f0f59e6eaa2eb15c50b165e8f9540
前：
2025.11.01
後：
2025.11.03
#日報
やった
↑
もっとある
分離するには
Veltman意味論
および
Verbrugge意味論
を用意しなければならない．さらに言えばいくつかの公理は
Veltman意味論
では分離できない：その意味で不完全．
やった
J.M. Rovira; "Interpretability logics and generalized Veltman semantics in Agda"
これ手元で動かしてみようとおもって
Agda
触ってみたけど普通に環境構築するの
Lean
に比べて面倒すぎる，流行らせる気あるのか？
思った
understeer Pt.1
めっちゃ良かったらしい，行きたかったなー
すいません各々再現ミックスや映像を上げてください；；
メモ
https://www.youtube.com/watch?v=aiIkaUjhgqw
これわかってないの？
メモ
@Kory__3
に
Kripkeゲーム
の
Lean
による解析の記事を
定理証明支援系 Advent Calendar 2025
に書くように頼んでみた．
思った
やることが多い！