K4の循環シークエント計算体系とGLのシークエント計算は証明能力が同じ
Claim
$ \sf GLのシークエント計算体系を$ \mathfrak{S}_\mathsf{GL}，K4の循環シークエント計算体系を$ \mathfrak{S}^\mathrm{circ}_\mathsf{K4}とし，$ Sをシーケントとする．
このとき，$ \mathfrak{S}_\mathsf{GL} \vdash S \iff \mathfrak{S}^\mathrm{circ}_\mathsf{K4} \vdash Sが成り立つ．
proof
$ \impliesの証明はD. Shamkanov; 2018; "Circular Proofs for the Gödel-Löb Provability Logic"#654ec63813a1580000cd1845によって為されている．
より強い主張$ \iffの証明はR. Iemhoff; 2022; "Reasoning in Circles"に書かれている．
memo
この事実を一般化したものをCircular Companionと呼ぶ．当該記事参照．
#K4の循環シークエント計算体系
#証明可能性論理GLのシークエント計算体系