Circular proofs for the Gödel-Löb provability logic (Q2343897)

A sequent calculus for the provability logic {\mathsf GL} is introduced by \textit{G. Sambin} and \textit{S. Valentini} [Stud. Log. 39, 245--256 (1980; Zbl 0457.03016); J. Philos. Log. 11, 311--342 (1982; Zbl 0523.03014)]. \textit{D. Leivant} introduced a sequent calculus for {\mathsf GL} in [J. Symb. Log. 46, 531--538 (1981; Zbl 0464.03019)], too. A syntactic proof of the cut-elimination theorem for the sequent calculus for {\mathsf GL} was given by \textit{S. Valentini} [J. Philos. Log. 12, 471--476 (1983; Zbl 0535.03031)]. In the paper under review, the notion of a circular proof in a sequent system for {\mathsf GL} is introduced. Circular proofs are represented by graphs allowed to contain cycles, rather than by finite trees. The author gives a syntactic proof of the Lyndon interpolation property.