Circular Proofs for G\"odel-L\"ob Logic
Daniyar Shamkanov
TL;DR
This paper introduces a sequent-style proof system for G"odel-L"ob logic that allows circular proofs with cyclic graphs, enabling new syntactic proofs of Lindon interpolation.
Contribution
It develops a novel proof system for GL with circular proofs and proves Lindon interpolation syntactically, advancing proof theory for provability logic.
Findings
Circular proof system for GL established
Syntactic Lindon interpolation proved for GL
Graph structure of proofs can contain cycles
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Algebra and Logic · semigroups and automata theory · Formal Methods in Verification