Gödelと様相論理S4
References
数学における証明と真理 様相論理と数学基礎論
K. Gödel; 1933; "Eine Interpretation des intuitionistischen Aussagenkalküls"
Memo
証明可能性論理の萌芽において，Kurt Gödelは直観主義命題論理と様相論理S4の関係性を調べている．
Gödelは$ \Boxを実際の証明可能性と対応付けたらしい．
すなわち現代的な視座で言えば，解釈(証明可能性論理)$ f_Tを用いて$ \Box A \iff T \vdash f_T(A)
このとき，$ \Box\Box \varphiは$ T \vdash \mathrm{Pr}_T(\ulcorner f_T(A) \urcorner)を表している．
この解釈のもとで様相論理S4は証明可能性論理として使えると思えるが，
問題は$ \vdash_\mathsf{S4} \Box(\Box \bot \to \bot)，すなわち$ T \vdash \mathrm{Pr}_T(\ulcorner \bot \urcorner) \to \botが成り立ってしまう．
対偶を取れば$ T \vdash \lnot \mathrm{Pr}_T(\ulcorner \bot \urcorner)，すなわち$ T \vdash \mathrm{Con}_Tであるから，第2不完全性定理より明らかにおかしい．
よって様相論理S4を証明可能性論理とするのはマズい
現在では$ \Boxは証明可能性述語として解釈されている．
すなわち$ \Box A \iff \mathrm{Pr}_T(\ulcorner f_T(A) \urcorner)