Forcing, Transition Algebras, and Calculi

Authors Go Hashimoto , Daniel Găină , Ionuţ Ţuţu



PDF
Thumbnail PDF

File

LIPIcs.ICALP.2024.143.pdf
  • Filesize: 0.84 MB
  • 17 pages

Document Identifiers

Author Details

Go Hashimoto
  • Kyushu University, Fukuoka, Japan
Daniel Găină
  • Kyushu University, Fukuoka, Japan
Ionuţ Ţuţu
  • Simion Stoilow Institute of Mathematics of the Romanian Academy, Bucharest, Romania

Cite AsGet BibTex

Go Hashimoto, Daniel Găină, and Ionuţ Ţuţu. Forcing, Transition Algebras, and Calculi. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 143:1-143:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ICALP.2024.143

Abstract

We bring forward a logical system of transition algebras that enhances many-sorted first-order logic using features from dynamic logics. The sentences we consider include compositions, unions, and transitive closures of transition relations, which are treated similarly to the actions used in dynamic logics in order to define necessity and possibility operators. This leads to a higher degree of expressivity than that of many-sorted first-order logic. For example, one can finitely axiomatize both the finiteness and the reachability of models, neither of which are ordinarily possible in many-sorted first-order logic. We introduce syntactic entailment and study basic properties such as compactness and completeness, showing that the latter does not hold when standard finitary proof rules are used. Consequently, we define proof rules having both finite and countably infinite premises, and we provide conditions under which completeness can be proved. To that end, we generalize the forcing method introduced in model theory by Robinson from a single signature to a category of signatures, and we apply it to obtain a completeness result for signatures that are at most countable.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Proof theory
  • Theory of computation → Equational logic and rewriting
Keywords
  • Forcing
  • institution theory
  • calculi
  • algebraic specification
  • transition systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Egidio Astesiano, Michel Bidoit, Hélène Kirchner, Bernd Krieg-Brückner, Peter D. Mosses, Donald Sannella, and Andrzej Tarlecki. CASL: The common algebraic specification language. Theoretical Computer Science, 286(2):153-196, 2002. URL: https://doi.org/10.1016/S0304-3975(01)00368-1.
  2. Tomasz Borzyszkowski. Generalized interpolation in CASL. Information Processing Letters, 76(1-2):19-24, 2000. URL: https://doi.org/10.1016/S0020-0190(00)00120-4.
  3. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott, editors. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of LNCS. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71999-1.
  4. Mihai Codescu, Till Mossakowski, Adrián Riesco, and Christian Maeder. Integrating Maude into Hets. In Michael Johnson and Dusko Pavlovic, editors, Algebraic Methodology and Software Technology - 13th International Conference, AMAST 2010, Lac-Beauport, QC, Canada, June 23-25, 2010. Revised Selected Papers, volume 6486 of LNCS, pages 60-75. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-17796-5_4.
  5. Paul J. Cohen. The independence of the continuum hypothesis. Proceedings of the National Academy of Sciences of the United States of America, 50(6):1143-1148, December 1963. URL: https://doi.org/10.1073/pnas.50.6.1143.
  6. Paul J. Cohen. The independence of the continuum hypothesis, II. Proceedings of the National Academy of Sciences of the United States of America, 51(1):105-110, January 1964. URL: https://doi.org/10.1073/pnas.51.1.105.
  7. William Craig. Linear reasoning. A new form of the Herbrand-Gentzen theorem. Journal of Symbolic Logic, 22(3):250-268, 1957. URL: https://doi.org/10.2307/2963593.
  8. Pierpaolo Degano, Fabio Gadducci, and Corrado Priami. A causal semantics for CCS via rewriting logic. Theoretical Computer Science, 275(1-2):259-282, 2002. URL: https://doi.org/10.1016/S0304-3975(01)00165-7.
  9. Răzvan Diaconescu. Institution-Independent Model Theory. Studies in Universal Logic. Birkhäuser, 2008. Google Scholar
  10. Răzvan Diaconescu. Three decades of institution theory. In Jean-Yves Béziau, editor, Universal Logic: An Anthology, pages 309-322. Springer, 2012. URL: https://doi.org/10.1007/978-3-0346-0145-0_25.
  11. Răzvan Diaconescu and Kokichi Futatsugi. Logical foundations of CafeOBJ. Theoretical Computer Science, 285(2):289-318, 2002. URL: https://doi.org/10.1016/S0304-3975(01)00361-9.
  12. Steven Eker, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, and Alberto Verdejo. The Maude strategy language. Journal of Logical and Algebraic Methods in Programming, 134:100887, 2023. URL: https://doi.org/10.1016/j.jlamp.2023.100887.
  13. Joseph Goguen and José Meseguer. Completeness of many-sorted equational logic. ACM SIGPLAN Notices, 17(1):9-17, 1982. URL: https://doi.org/10.1145/947886.947887.
  14. Joseph Goguen and José Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science, 105(2):217-273, 1992. URL: https://doi.org/10.1016/0304-3975(92)90302-V.
  15. Joseph Goguen, Timothy Winkler, José Meseguer, Kokichi Futatsugi, and Jean-Pierre Jouannaud. Introducing OBJ, pages 3-167. Springer, 2000. URL: https://doi.org/10.1007/978-1-4757-6541-0_1.
  16. Joseph A. Goguen and Rod M. Burstall. Institutions: Abstract model theory for specification and programming. J. ACM, 39(1):95-146, 1992. URL: https://doi.org/10.1145/147508.147524.
  17. Daniel Găină. Forcing, downward Löwenheim-Skolem and omitting types theorems, institutionally. Logica Universalis, 8(3-4):469-498, 2014. URL: https://doi.org/10.1007/S11787-013-0090-0.
  18. Daniel Găină. Forcing and calculi for hybrid logics. Journal of the Association for Computing Machinery, 67(4):1-55, 2020. URL: https://doi.org/10.1145/3400294.
  19. Daniel Găină, Guillermo Badia, and Tomasz Kowalski. Robinson consistency in many-sorted hybrid first-order logics. In David Fernández-Duque, Alessandra Palmigiano, and Sophie Pinchinat, editors, Advances in Modal Logic, AiML 2022, Rennes, France, August 22-25, 2022, pages 407-428. College Publications, 2022. URL: http://www.aiml.net/volumes/volume14/25-Gaina-Badia-Kowalski.pdf.
  20. Daniel Găină, Guillermo Badia, and Tomasz Kowalski. Omitting types theorem in hybrid dynamic first-order logic with rigid symbols. Annals of Pure and Applied Logic, 174(3):103212, 2023. URL: https://doi.org/10.1016/J.APAL.2022.103212.
  21. Daniel Găină and Marius Petria. Completeness by forcing. Journal of Logic and Computation, 20(6):1165-1186, 2010. URL: https://doi.org/10.1093/LOGCOM/EXQ012.
  22. Daniel Găină and Andrei Popescu. An institution-independent proof of the Robinson consistency theorem. Studia Logica, 85(1):41-73, 2007. URL: https://doi.org/10.1007/S11225-007-9022-4.
  23. Go Hashimoto, Daniel Găină, and Ionuţ Ţuţu. Forcing, transition algebras, and calculi (extended version), 2024. URL: https://arxiv.org/abs/2404.16111.
  24. Narciso Martí-Oliet and José Meseguer. Rewriting logic as a logical and semantic framework. In José Meseguer, editor, First International Workshop on Rewriting Logic and its Applications, RWLW 1996, Asilomar Conference Center, Pacific Grove, CA, USA, September 3-6, 1996, volume 4 of Electronic Notes in Theoretical Computer Science, pages 190-225. Elsevier, 1996. URL: https://doi.org/10.1016/S1571-0661(04)00040-4.
  25. José Meseguer. Conditional rewriting logic: Deduction, models and concurrency. In Stéphane Kaplan and Mitsuhiro Okada, editors, Conditional and Typed Rewriting Systems, 2nd International CTRS Workshop, Montreal, Canada, June 11-14, 1990, Proceedings, volume 516 of LNCS, pages 64-91. Springer, 1990. URL: https://doi.org/10.1007/3-540-54317-1_81.
  26. Robin Milner. A Calculus of Communicating Systems, volume 92 of LNCS. Springer, 1980. URL: https://doi.org/10.1007/3-540-10235-3.
  27. Robin Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989. Google Scholar
  28. J. Donald Monk. Mathematical Logic, volume 37 of Graduate Texts in Mathematics. Springer-Verlag New York, 1976. Google Scholar
  29. Marius Petria. An institutional version of Gödel’s completeness theorem. In Till Mossakowski, Ugo Montanari, and Magne Haveraaen, editors, Algebra and Coalgebra in Computer Science, Second International Conference, CALCO 2007, Bergen, Norway, August 20-24, 2007, Proceedings, volume 4624 of LNCS, pages 409-424. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73859-6_28.
  30. Abraham Robinson. Forcing in model theory. Symposia Mathematica, 5:69-82, 1971. Google Scholar
  31. Donald Sannella and Andrzej Tarlecki. Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-17336-3.
  32. Bruce Schechter. My Brain is Open: The Mathematical Journeys of Paul Erdös. Simon & Schuster, 2000. Google Scholar
  33. Andrzej Tarlecki. Bits and pieces of the theory of institutions. In Klaus Drosten, Hans-Dieter Ehrich, Martin Gogolla, and Udo W. Lipeck, editors, Proceedings of the 4st Workshop on Abstract Data Type, 1986. University of Braunschweig, Germany, 1986. Google Scholar
  34. Alberto Verdejo and Narciso Martí-Oliet. Implementing CCS in Maude 2. In Fabio Gadducci and Ugo Montanari, editors, Fourth International Workshop on Rewriting logic and Its Applications, WRLA2002, Pisa, Italy, 19-21, 2002, volume 71 of Electronic Notes in Theoretical Computer Science, pages 282-300. Elsevier, 2002. URL: https://doi.org/10.1016/S1571-0661(05)82540-X.