Circular Proofs for G\"odel-L\"ob Logic
Logic
2015-01-05 v1 Logic in Computer Science
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.
Cite
@article{arxiv.1401.4002,
title = {Circular Proofs for G\"odel-L\"ob Logic},
author = {Daniyar Shamkanov},
journal= {arXiv preprint arXiv:1401.4002},
year = {2015}
}
Comments
13 pages