デネセシテーション
定義
$ \vdash_\Lambda \Box A \implies \vdash_\Lambda A
成り立つ論理
様相論理の公理T
:
$ \mathsf{T} \equiv \Box A \to A
を含む論理体系
構文論的な証明で直ちに成り立つ
証明可能性論理GL
GLのデネセシテーション
木モデルに対する操作によって意味論的に証明できる