Circular Proofs for G\"odel-L\"ob Logic
classification
🧮 math.LO
cs.LO
keywords
proofscircularlogicproofadmitsallowedapplicationcontain
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.