Circular Proofs for Gödel-Löb Logic

Abstract

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.

13 pages

Cited by in corpus (4)

• Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses
• On structural proof theory of the modal logic K+ extended with infinitary derivations
• The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
• Cyclic Proofs for iGL via Corecursion