「数学における証明と真理」の第４部の途中まで読んだけど、
様相とKripke意味論の関係の面白さを存分に伝える本だと思う。

小野先生の「情報科学における論理」にも様相論理の章はあるけど、
シーケント計算で定式化してる為にS4とかS5しか綺麗に扱えない点で問題だと思う。
Prawitzの本は自然演繹の本もS4、S5とかしか扱ってない。

様相論理は演繹定理が大域的に成立しないこと自体がポイントの一つなので
Hilbert流に定式化するのがおそらく最善なのだと思う。
様相に関する公理は、論理的な規則よりも寧ろ
数学的概念についての公理に近い性格を持つものだという事を示しているように思う。