Reasoning in circles

TL;DR

This paper proves that a formula belongs to the provability logic GL if and only if it has a circular proof in sequent calculus, extending the result to intuitionistic logic without using infinitary proofs.

Contribution

It establishes the equivalence between circular proofs and provability in GL using sequent calculus, simplifying previous infinitary proof approaches and generalizing to intuitionistic logic.

Findings

Circular proofs characterize provability in GL.

Sequent calculus can be used instead of infinitary systems.

The result extends to intuitionistic logic.

Abstract

Circular proofs, introduced by Daniyar Shamkanov, are proofs in which assumptions are allowed that are not axioms but do appear at least twice along a branch. Shamkanov has shown that a formula belongs to the provability logic GL exactly if it has a circular proof in the modal logic K4. Shamkanov uses Tait style proof systems and infinitary proofs. In this paper we prove the same result but then for sequent calculi and without the detour via infinitary systems. We also obtain a mild generalisation of the result, implying that its intuitionistic analogue holds as well.