×

zbMATH — the first resource for mathematics

Circular proofs for the Gödel-Löb provability logic. (English. Russian original) Zbl 1329.03092
Math. Notes 96, No. 4, 575-585 (2014); translation from Mat. Zametki 96, No. 4, 609-622 (2014).
A sequent calculus for the provability logic \mathsf GL is introduced by G. Sambin and S. Valentini [Stud. Log. 39, 245–256 (1980; Zbl 0457.03016); J. Philos. Log. 11, 311–342 (1982; Zbl 0523.03014)]. D. Leivant introduced a sequent calculus for \mathsf GL in [J. Symb. Log. 46, 531–538 (1981; Zbl 0464.03019)], too. A syntactic proof of the cut-elimination theorem for the sequent calculus for \mathsf GL was given by S. Valentini [J. Philos. Log. 12, 471–476 (1983; Zbl 0535.03031)]. In the paper under review, the notion of a circular proof in a sequent system for \mathsf GL is introduced. Circular proofs are represented by graphs allowed to contain cycles, rather than by finite trees. The author gives a syntactic proof of the Lyndon interpolation property.

MSC:
03F45 Provability logics and related algebras (e.g., diagonalizable algebras)
03F07 Structure of proofs
Software:
Cyclist
PDF BibTeX XML Cite
Full Text: DOI arXiv
References:
[1] Negri, S, Proof analysis in modal logic, J. Philos. Logic, 34, 507-544, (2005) · Zbl 1086.03045
[2] Poggiolesi, F, A purely syntactic and cut-free sequent calculus for the modal logic of provability, Rev. Symb. Log., 2, 593-611, (2009) · Zbl 1189.03071
[3] Goré, R; Ramanayake, R, Valentini’s cut-elimination for provability logic resolved, Rev. Symb. Log., 5, 212-238, (2012) · Zbl 1254.03113
[4] Brotherston, J; Gorogiannis, N; Petersen, R L, A generic cyclic theorem prover, 350-367, (2012), Berlin
[5] Benthem, J, Modal frame correspondences and fixed-points, Studia Logica, 83, 133-155, (2006) · Zbl 1106.03017
[6] Visser, A, Löb’s logic meets the µ-calculus, 14-25, (2005), Berlin · Zbl 1171.03314
[7] Alberucci, L; Facchini, A, On modal µ-calculus and Gödel-Löb logic, Studia Logica, 91, 145-169, (2009) · Zbl 1201.03008
[8] Shamkanov, D S, Interpolation properties for provability logics GL and GLP, Trudy Mat. Inst. Steklov, 274, 329-342, (2011)
[9] Sambin, G; Valentini, S, A modal sequent calculus for a fragment of arithmetic, Studia Logica, 39, 245-256, (1980) · Zbl 0457.03016
[10] Sambin, G; Valentini, S, The modal logic of provability. the sequential approach, J. Philos. Logic, 11, 311-342, (1982) · Zbl 0523.03014
[11] Leivant, D, On the proof theory of the modal logic for arithmetic provability, J. Symbolic Logic, 46, 531-538, (1981) · Zbl 0464.03019
[12] Tait, W W, Normal derivability in classical logic, 204-236, (1986), Berlin
[13] Valentini, S, The modal logic of provability: cut-elimination, J. Philos. Logic, 12, 471-476, (1983) · Zbl 0535.03031
[14] J. Brotherston, Sequent Calculus Proof Systems for Inductive Definitions, PhD Thesis (Univ. of Edinburgh, Edinburgh, 2006).
[15] Jacobs, B; Rutten, J, A tutorial on (co)algebras and (co)induction, Bull. EATCS, 62, 222-259, (1997) · Zbl 0880.68070
[16] Lindström, P, Provability logic-A short introduction, Theoria, 62, 19-61, (1996) · Zbl 0897.03055
[17] Smoryński, C, Modal logic and self-reference, 441-495, (1984), Dordrecht · Zbl 0875.03049
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.