Pure Logic of Necessitation
Remark
非正規様相論理
．
$ \sf N
としてよく表記される
M.C.Fitting, V.W.Marek, M.Truszczyński; "The pure logic of necessitation"
で導入．
非単調論理
の文脈で．
証明可能性述語
として満たされるべき最も本質的な性質である
導出可能性条件
D1を特徴づける論理としても使うことが出来る．
すなわち
$ T \vdash \varphi \implies T \vdash \mathrm{Pr}_T(\ulcorner \varphi \urcorner)
T. Kurahashi, "Rosser Provability and Normal Modal Logics"
全ての証明可能性述語についての証明可能性論理
訳は別に無いと思う．強いて訳すなら
ネセシテーションのみの論理
？
Def
公理
古典命題論理のトートロジー
推論規則
モーダス・ポネンス
$ \varphi,\varphi\to\psi \mid \psi
ネセシテーション
$ \varphi \mid \Box\varphi
remark:
要するに，公理として
$ \mathsf{K} \equiv \Box(\varphi \to \psi) \to (\Box\varphi \to \Box\psi)
が無いので
正規様相論理
ではない．
Remark
Kripkeモデル
は使えない．
Pure Logic of Necessitationの擬Kripkeモデル
を考える．