2025.09.03
https://gyazo.com/6a577449e59a35101430d406d9bb0701
ｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗ
https://studenttheses.uu.nl/bitstream/handle/20.500.12932/49881/master-thesis.pdf
Bram Swaanen; "Formalizing Axiomatic Theories of Truth"
今見たら上は
Bertrand Russell
で下の
Sorensen
と
Urzyczyn
は
Lectures on the Curry-Howard Isomorphism
の著者だった．めちゃくちゃだ
前：
2025.09.02
後：
2025.09.04
#日報
メモ
Valentini & Solitro 1983, Theorem 2
$ \bf GL
はletterlessな
$ \sf .w3
を証明できる．このことを使うと以下は同値になる．
1. 任意の
0-代入
$ s
で
$ \mathbf{GL} \vdash s(\varphi)
2.
$ \bf GL.3 \vdash \varphi
その事実を使えば2から1は簡単．逆は
Kripke意味論
の議論が必要で面倒？
思った
仮眠したら6時間寝ちゃって終わった