2024.01.17
https://gyazo.com/3ad59cfa303149f31eb13eb618001b13
前：
2024.01.16
後：
2024.01.18
#日報
メモ
T. Litak, A. Visser; "Lewis meets Brouwer: constructive strict implication"
https://arxiv.org/abs/1708.02143
直観主義様相論理
ではUnaryな
様相演算子
$ \Box
よりBinaryな
厳密含意
$ \to^\Box
を採用したほうが上手くやれる．ということが書いてあるらしい．
余談：
[$ \strictif]
が無いので，今後この
Scrapbox
では厳密含意を
$ \to^\Box
と表記する．
全然考えたこともなかったが，
$ \Box A \equiv \top \to^\Box A
と定義出来るということが言われて確かにと思った．
知った
様相論理S5のカノニカルモデルを構成しない完全性定理
教えてもらったが，
$ \bf S5
の
完全性定理
は
カノニカルモデル
を構成しなくても証明出来るらしい．
G. H. Hughes, M. J. Cresswell; "A New Introduction to Modal Logic"
に書いてあるそうな