Circular Proofs for Gödel-Löb Logic
Daniyar Salkarbekovich Shamkanov · 2014
We present a sequent-style proof system for provability logic GL that admits so-called circular proofs. For these proofs, the graph underlying a proof is not a finite tree but is allowed to contain cycles. As an application, we establish Lindon interpolation for GL syntactically.