arXiv · 1401.4002
Circular Proofs for G\"odel-L\"ob 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.
Explore related subjects
Keep this discovery
Daniyar Shamkanov. 2014-01-16. Circular Proofs for G\"odel-L\"ob Logic. https://doi.org/10.1134/s0001434614090326
Cite the original work for its findings. Save a collection to share your selection of sources.