Circular Proofs for the G\"odel--L\"ob Provability Logic

D. S. Shamkanov

Matematičeskie zametki, Tome 96 (2014) no. 4, pp. 609-622.

Résumé

Sequent calculus for the provability logic $\mathsf{GL}$ is considered, in which provability is based on the notion of a circular proof. Unlike ordinary derivations, circular proofs are represented by graphs allowed to contain cycles, rather than by finite trees. Using this notion, we obtain a syntactic proof of the Lyndon interpolation property for $\mathsf{GL}$.

Détail

Keywords: provability logic, sequent calculus, circular proof, the Gödel–Löb logic, the Lyndon interpolation property, split sequent.

Bibliographie

[1] S. Negri, “Proof analysis in modal logic”, J. Philos. Logic, 34:5-6 (2005), 507–544 | DOI | MR | Zbl

[2] F. Poggiolesi, “A purely syntactic and cut-free sequent calculus for the modal logic of provability”, Rev. Symb. Log., 2:4 (2009), 593–611 | DOI | MR | Zbl

[3] R. Goré, R. Ramanayake, “Valentini's cut-elimination for provability logic resolved”, Rev. Symb. Log., 5:2 (2012), 212–238 | DOI | MR | Zbl

[4] J. Brotherston, N. Gorogiannis, R. L. Petersen, “A generic cyclic theorem prover”, Programming Languages and Systems, Lecture Notes in Comput. Sci., 7705, Springer-Verlag, Berlin, 2012, 350–367 | DOI

[5] J. van Benthem, “Modal frame correspondences and fixed-points”, Studia Logica, 83:1-3 (2006), 133–155 | DOI | MR | Zbl

[6] A. Visser, “Löb's logic meets the $\mu$-calculus”, Processes, Terms and Cycles: Steps on the Road to Infinity, Lecture Notes in Comput. Sci., 3838, Springer-Verlag, Berlin, 2005, 14–25 | DOI | Zbl

[7] L. Alberucci, A. Facchini, “On modal $\mu$-calculus and Gödel–Löb logic”, Studia Logica, 91:2 (2009), 145–169 | DOI | MR | Zbl

[8] D. S. Shamkanov, “Interpolyatsionnye svoistva logik dokazuemosti $\mathbf{GL}$ i $\mathbf{GLP}$”, Algoritmicheskie voprosy algebry i logiki, Sbornik statei. K 80-letiyu so dnya rozhdeniya akademika Sergeya Ivanovicha Adyana, Tr. MIAN, 274, MAIK, M., 2011, 329–342 | MR

[9] G. Sambin, S. Valentini, “A modal sequent calculus for a fragment of arithmetic”, Studia Logica, 39:2-3 (1980), 245–256 | DOI | MR | Zbl

[10] G. Sambin, S. Valentini, “The modal logic of provability. The sequential approach”, J. Philos. Logic, 11:3 (1982), 311–342 | DOI | MR | Zbl

[11] D. Leivant, “On the proof theory of the modal logic for arithmetic provability”, J. Symbolic Logic, 46:3 (1981), 531–538 | DOI | MR | Zbl

[12] W. W. Tait, “Normal derivability in classical logic”, The Syntax and Semantics of Ifinitary Languages, Lecture Notes in Math., 72, Springer-Verlag, Berlin, 1986, 204–236 | DOI

[13] S. Valentini, “The modal logic of provability: cut-elimination”, J. Philos. Logic, 12:4 (1983), 471–476 | DOI | MR | Zbl

[14] J. Brotherston, Sequent Calculus Proof Systems for Inductive Definitions, Ph.D. Thesis, Edinburgh, 2006

[15] B. Jacobs, J. Rutten, “A tutorial on (co)algebras and (co)induction”, Bull. EATCS, 62 (1997), 222–259 | Zbl

[16] P. Lindström, “Provability logic – a short introduction”, Theoria, 62:1-2 (1996), 19–61 | DOI | MR | Zbl

[17] C. Smoryński, “Modal logic and self-reference”, Handbook of Philosophical Logic, Vol. II. Extensions of Classical Logic, Synthese Lib., 165, Reidel, Dordrecht, 1984, 441–495 | MR | Zbl