Circular proofs for provability logic

We present a circular proof system for the Gödel-Löb provability logic GL. In contrast to the ordinary proofs, a circular proof can be formed from an ordinary derivation tree by identifying each open assumption with an identical interior sequent. We prove that the circular proof-system is sound and complete with respect to the standard sequent-style formulation of GL, that it is contraction-free and cut-free, and that its logical rules are invertible. As an application, we give a syntactic proof of Lyndon interpolation for GL.