正規様相論理K
よく知られている
様相論理
で，必然性の演算子
$ \Box
と可能性の演算子
$ \Diamond
（必須ではない．）を導入したもの
様相論理の公理K
と
ネセシテーション
がある論理と考えれば良い