デネセシテーション
定義
$ \vdash_\Lambda \Box A \implies \vdash_\Lambda A
成り立つ論理
様相論理の公理T：$ \mathsf{T} \equiv \Box A \to Aを含む論理体系 木モデルに対する操作によって意味論的に証明できる
興味深い事実として$ \bf GLは$ \sf Tを持たない。
メモ
様相選言特性$ \vdash \Box A \lor \Box B \implies \vdash A ~\text{or}~ \vdash B $ \vdash \Box A \implies \vdash \Box A \lor \Box A \implies \vdash A