Circular proofs for the Gödel-Löb provability logic
Daniyar Salkarbekovich Shamkanov · Mathematical Notes · 2014
Sequent calculus for the provability logic GL is considered, in which provability is based on the notion of a circular proof. Unlike ordinary derivations, circular proofs are represented by graphs allowed to contain cycles, rather than by finite trees. Using this notion, we obtain a syntactic proof of the Lyndon interpolation property for GL.