GLSの算術的完全性定理
様相論理GLSは以下の意味で真の算術(True Arithemtic)の証明可能性論理と呼ばれる． Thm 1
以下は同値．
1. $ \vdash_\mathbf{GL} \bigwedge R(A) \to A
2. $ \vdash_\mathbf{GLS} A
3. 任意の$ Tへの算術的解釈$ *_Tについて$ \mathbb{N} \vDash A^{*_T}
ただしここで$ R(A) := \{ \Box B \to B \mid B \in \mathrm{Sub}(A) \}