 An intriguing new proof-theoretical development is Shamkanov’s expansion of sequent-style proof systems by allowing circular proofs (Shamkanov 2014). Consider a sequent system for K4, the modal system resulting from GL by replacing the axiom GL by the weaker axiom \(\Box A \rightarrow \Box\Box A\) (axiom 4). However, suppose that open hypotheses are allowed, provided that the same sequent occurs strictly below that hypothesis in the proof tree. Formulated more technically, one can find a circular derivation from an ordinary derivation tree by linking each of its non-axiomatic leaves with an identical interior node. Shamkanov (2014) proved that the resulting system is consistent and that moreover, in general, each sequent has a GL-derivation if and only if it has a circular K4-derivation. Circular proofs also provide a method to show proof-theoretically that Lyndon’s interpolation theorem holds for GL. Standard interpolation for GL  had already been proved before by different methods (Boolos 1979;  Smoryński 1978; Rautenberg 1983).  (For more information about Lyndon’s interpolation theorem for first-order logic, see also the entry  first-order model theory ).