Hostname: page-component-cd9895bd7-gxg78 Total loading time: 0 Render date: 2024-12-18T15:01:38.608Z Has data issue: false hasContentIssue false
  • English
  • Français

NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC

Part of: General logic Proof theory and constructive mathematics

Published online by Cambridge University Press:  29 June 2020

YURY SAVATEEV  and
DANIYAR SHAMKANOV
YURY SAVATEEV
Affiliation:
STEKLOV MATHEMATICAL INSTITUTE OF RUSSIAN ACADEMY OF SCIENCESGUBKINA STR. 8, 119991 MOSCOW, RUSSIAE-mail: [email protected]: [email protected]
DANIYAR SHAMKANOV
Affiliation:
STEKLOV MATHEMATICAL INSTITUTE OF RUSSIAN ACADEMY OF SCIENCESGUBKINA STR. 8, 119991 MOSCOW, RUSSIAE-mail: [email protected]: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We present a sequent calculus for the Grzegorczyk modal logic $\mathsf {Grz}$ allowing cyclic and other non-well-founded proofs and obtain the cut-elimination theorem for it by constructing a continuous cut-elimination mapping acting on these proofs. As an application, we establish the Lyndon interpolation property for the logic $\mathsf {Grz}$ proof-theoretically.

Keywords

non-well-founded proofsGrzegorczyk logiccut-eliminationLyndon interpolationcyclic proofs

MSC classification

Primary: 03F05: Cut-elimination and normal-form theorems
Secondary: 03F07: Structure of proofs 03B45: Modal logic (including the logic of norms)
Type
Research Article
Information
The Review of Symbolic Logic , Volume 14 , Issue 1 , March 2021 , pp. 22 - 50
Check for updates
Copyright
© Association for Symbolic Logic, 2020

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

BIBLIOGRAPHY

Afshari, B. & Leigh, G. (2017). Cut-free completeness for modal mu-calculus. In LICS’17: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE Press, 1-12.Google Scholar
Avron, A. (1984). On modal systems having arithmetical interpretations. Journal of Symbolic Logic, 49(3), 935–942.CrossRefGoogle Scholar
Baedel, D., Doumane, A., & Saurin, A. (2016). Infinitary proof theory: the multiplicative additive case. In Talbot, J. M., and Regnier, L., editors. 25th EACSL Annual Conference on Computer Science Logic. Dagstuhl: Schloss Dagstuhl, pp. 42:1–42:17.Google Scholar
Baier, C. & Majster-Cederbaum, M. E. (1994). Denotational semantics in the cpo and metric approach. Theoretical Computer Science, 135, 171–220.CrossRefGoogle Scholar
Borga, M. & Gentilini, P.. (1986). On the proof theory of the modal logic Grz. Mathematical Logic Quarterly, 32(10–12), 145–148.CrossRefGoogle Scholar
Chagrov, A. & Zakharyaschev, M.. (1997). Modal Logic. Oxford: Oxford University Press.Google Scholar
Das, A. & Pous, D.. (2018). Non-wellfounded proof theory for (Kleene+action) (algebras+lattices). In Ghica, D. R., and Jung, A., editors. 27th EACSL Annual Conference on Computer Science Logic 2018. Dagstuhl: Schloss Dagstuhl, pp. 19:1–19:18.Google Scholar
Di Gianantonio, P. & Miculan, M. (2002). A unifying approach to recursive and co-recursive definitions. In Geuvers, H., & Wiedijk, F., editors. TYPES 2002: Types for Proofs and Programs. Lecture Notes in Computer Science, Vol. 2646. Berlin: Springer, pp. 148–161.Google Scholar
Dyckhoff, R. & Negri, S. (2016). A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel–McKinsey–Tarski embedding. Journal of Logic and Computation, 26(1), 169–187 CrossRefGoogle Scholar
Escardó, M. H. (1998). A metric model of PCF. Laboratory for Foundations of Computer Science, The University of Edinburgh.Google Scholar
Fortier, J. & Santocanale, L. (2013). Cuts for circular proofs: semantics and cut-elimination. In Della Rocca, S. R., editor. Computer Science Logic 2013. Dagstuhl: Schloss Dagstuhl, pp. 248–262.Google Scholar
Iemhoff, R. (2016). Reasoning in circles. In van Eijck, J, Iemhoff, R., and Joosten, J. J., editors. Liber Amicorum Alberti. A Tribute to Albert Visser. London: College Publications, pp. 165–176.Google Scholar
Kuznetsov, S. (2017). The Lambek calculus with Iteration: two Variants. In Kennedy, J., & de Queiroz, R., editors. Logic, Language, Information, and Computation. Berlin: Springer, pp. 182–198.CrossRefGoogle Scholar
Maksimova, L. L. (2008). On modal Grzegorczyk logic, Fundamenta Informaticae, 81(1–3), 203–210.Google Scholar
Maksimova, L. L. (2014). The Lyndon property and uniform interpolation over the Grzegorczyk logic. Siberian Mathematical Journal, 55(1), 118–124.CrossRefGoogle Scholar
Petalas, C. & Vidalis, T. (1993). A fixed point theorem in non-Archimedean vector spaces. Proceedings of the American Mathematical Society, 118(3), 819–821.CrossRefGoogle Scholar
Prieß-Crampe, S. (1990). Der Banachsche Fixpunktsatz für ultrametrische Räume. Results in Mathematics, 18(1–2), 178–186.CrossRefGoogle Scholar
Savateev, Y. & Shamkanov, D. (2017). Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs. In Kennedy, J., & de Queiroz, R., editors. Logic, Language, Information, and Computation. Berlin: Springer, pp. 321–335.CrossRefGoogle Scholar
Schörner, E. (2003). Ultrametric fixed point theorems and applications. In Kuhlmann, VF. V., Kuhlmann, S., and Marshall, M., editors. Valuation Theory and Its Applications, Volume II. Providence, RI: American Mathematical Society, pp. 353–359.CrossRefGoogle Scholar
Shamkanov, D. S. (2014). Circular proofs for the Gödel-Löb provability logic. Mathematical Notes, 96(3), 575–585.CrossRefGoogle Scholar
Simpson, A. (2017). Cyclic arithmetic is equivalent to peano arithmetic. In Esparza, J., & Murawski, A., editors. Foundations of Software Science and Computation Structures. Berlin: Springer, pp. 283–300.CrossRefGoogle Scholar
van Breugel, F. (2001). An introduction to metric semantics: operational and denotational models for programming and specfication languages. Theoretical Computer Science, 258, 1–98.CrossRefGoogle Scholar