様相論理GLS
Memo
真の算術に対応する証明可能性論理
$ \bf GLの定理と$ \sf Tを公理として持ち，モーダスポネンスに閉じた論理．
ネセシテーションを持たない
ネセシテーションを持たない様相論理
Memo
最後の$ \sf SはRobert M. Solovayに由来する．
H. Kushida; "A proof theory for the logic of provability in true arithmetic"
GLSの算術的完全性定理