Hostname: page-component-cd9895bd7-jn8rn Total loading time: 0 Render date: 2024-12-23T10:46:38.988Z Has data issue: false hasContentIssue false
  • English
  • Français

Abstract Beth definability in institutions

Published online by Cambridge University Press:  12 March 2014

Marius Petria  and
Răzvan Diaconescu
Marius Petria
Affiliation:
Şcoala Normală Superioară, Calea Giviţei 21, Bucharest 010702, Romania
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper studies definability within the theory of institutions, a version of abstract model theory that emerged in computing science studies of software specification and semantics. We generalise the concept of definability to arbitrary logics, formalised as institutions, and we develop three general definability results. One generalises the classical Beth theorem by relying on the interpolation properties of the institution. Another relies on a meta Birkhoff axiomatizability property of the institution and constitutes a source for many new actual definability results, including definability in (fragments of) classical model theory. The third one gives a set of sufficient conditions for ‘borrowing’ definability properties from another institution via an ‘adequate’ encoding between institutions.

The power of our general definability results is illustrated with several applications to (many-sorted) classical model theory and partial algebra, leading for example to definability results for (quasi-)varieties of models or partial algebras. Many other applications are expected for the multitude of logical systems formalised as institutions from computing science and logic.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 71 , Issue 3 , September 2006 , pp. 1002 - 1028
Copyright
Copyright © Association for Symbolic Logic 2006

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

REFERENCES

[1]Andréka, Hajnal and Németi, IstvÁn, Łoś lemma holds in every category, Studia Scientiarum Mathematicarum Hungarica, vol. 13 (1978), pp. 361–376.Google Scholar
[2]Andréka, Hajnal and Németi, IstvÁn, A general axiomatizability theorem formulated in terms of cone-injective subcategories, Universal algebra (Csakany, B., Fried, E., and Schmidt, E. T., editors), North-Holland, 1981, Colloquia Mathematics Societas JÁnos Bolyai, 29, pp. 13–35.Google Scholar
[3]Andréka, Hajnal and Németi, IstvÁn, Generalization of the concept of variety and quasivariety to partial algebras through category theory, Dissertationes Mathematicae, vol. CCIV (1983).Google Scholar
[4]Bergstra, Jan, Heering, Jan, and Klint, Paul, Module algebra, Journal of the Association for Computing Machinery, vol. 37 (1990), no. 2, pp. 335–372.CrossRefGoogle Scholar
[5]Bidoit, Michel and Hennicker, Rolf, On the integration of the observability and reachability concepts, Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'2002), Lecture Notes in Computer Science, vol. 2303, 2002, pp. 21–36.CrossRefGoogle Scholar
[6]Bidoit, Michel and Tarlecki, Andrzej, Behavioural satisfaction and equivalence in concrete model categories, Proceedings of the 21st Colloquium on Trees in Algebra and Programming, Lecture Notes in Computer Science, vol. 1059, Springer Verlag, 1996, pp. 241–256.Google Scholar
[7]Borzyszkowski, Tomasz, Higher-order logic and theorem proving for structured specifications, Workshop on Algebraic Development Techniques 1999 (Choppy, Christine, Bert, Didier, and Mosses, Peter, editors), Lecture Notes in Computer Science, vol. 1827, 2000, pp. 401–418.Google Scholar
[8]Borzyszkowski, Tomasz, Generalized interpolation in CASL, Information Processing Letters, vol. 76 (2001), pp. 19–24.CrossRefGoogle Scholar
[9]Burmeister, Peter, A model theoretic oriented approach to partial algebras, Akademie-Verlag, Berlin, 1986.Google Scholar
[10]Cerioli, Maura and Meseguer, José, May I borrow your logic? (transporting logical structures along maps), Theoretical Computer Science, vol. 173 (1997), pp. 311–347.CrossRefGoogle Scholar
[11]Chang, C. C. and Keisler, H. J., Model theory, North Holland, Amsterdam, 1990.Google Scholar
[12]Cîrstea, Corina, Institutionalising many-sorted coalgebraic modal logic, Coalgebraic Methods in Computer Science 2002, Electronic Notes in Theoretical Computer Science, 2002.Google Scholar
[13]Diaconescu, Răzvan, Extra theory morphisms for institutions: logical semantics for multiparadigm languages, Applied Categorical Structures, vol. 6 (1998), no. 4, pp. 427–453, a preliminary version appeared as JAIST Technical Report IS-RR-97-0032F in 1997.CrossRefGoogle Scholar
[14]Diaconescu, Răzvan, Institution-independent ultraproducts, Fundamenta Informaticæ, vol. 55 (2003),no. 3–4, pp. 321–348.Google Scholar
[15]Diaconescu, Răzvan, Elementary diagrams in institutions, Journal of Logic and Computation, vol. 14 (2004), no. 5, pp. 651–674.CrossRefGoogle Scholar
[16]Diaconescu, Răzvan, An institution-independent proof of Craig Interpolation Theorem, Studia Logica, vol. 77 (2004), no. 1, pp. 59–79.CrossRefGoogle Scholar
[17]Diaconescu, Răzvan, Interpolation in Grothendieck institutions, Theoretical Computer Science, vol. 311 (2004), pp. 439–461.CrossRefGoogle Scholar
[18]Diaconescu, Răzvan, Jewels of institution-independent model theory, Algebra, meaning and computation (Essays dedicated to Joseph A. Goguen on the occasion of his 65th birthday), Lecture Notes in Computer Science, vol. 4060, Springer, 2006.Google Scholar
[19]Diaconescu, Răzvan, Proof systems for institutional logic, Journal of Logic and Computation, vol. 16 (2006), pp. 339–357.CrossRefGoogle Scholar
[20]Diaconescu, Răzvan, Institution-independent model theory, to appear, book draft. Ask author for current draft at Google Scholar
[21]Diaconescu, Răzvan, Goguen, Joseph, and Stefaneas, Petros, Logical support for modularisation, Logical environments (Huet, Gerard and Plotkin, Gordon, editors), Cambridge, 1993, proceedings of a workshop held in Edinburgh, Scotland, May 1991, pp. 83–130.Google Scholar
[22]Dimitrakos, Theodosis and Maibaum, Tom, On a generalized modularization theorem, Information Processing Letters, vol. 74 (2000), pp. 65–71.CrossRefGoogle Scholar
[23]Fiadeiro, J. L. and Costa, J. F., Mirror, mirror in my hand: A duality between specifications and models of process behaviour, Mathematical Structures in Computer Science, vol. 6 (1996), no. 4, pp. 353–373.CrossRefGoogle Scholar
[24]Găină, Daniel and Popescu, Andrei, An institution-independent generalization of Tarski's Elementary Chain Theorem, Journal of Logic and Computation, to appear.Google Scholar
[25]Găină, Daniel and Popescu, Andrei, An institution-independent proof of Robinson consistency theorem, Studia Logica, to appear.Google Scholar
[26]Goguen, Joseph and Burstall, Rod, Institutions: Abstract model theory for specification and programming, Journal of the Association for Computing Machinery, vol. 39 (1992), no. 1, pp. 95–146.CrossRefGoogle Scholar
[27]Goguen, Joseph and Diaconescu, Răzvan, Towards an algebraic semantics for the object paradigm, Recent trends in data type specification (Ehrig, Harmut and Orejas, Fernando, editors), Lecture Notes in Computer Science, vol. 785, Springer, 1994, pp. 1–34.CrossRefGoogle Scholar
[28]Goguen, Joseph and Roşu, Grigore, Institution morphisms, Formal Aspects of Computing, vol. 13 (2002), pp. 274–307.CrossRefGoogle Scholar
[29]Grätzer, George, Universal algebra, Springer, 1979.CrossRefGoogle Scholar
[30]Hodges, Wilfrid, Model theory, Cambridge University Press, 1993.CrossRefGoogle Scholar
[31]Lambek, Joachim and Scott, Phil, Introduction to higher order categorical logic, Cambridge Studies in Advanced Mathematics, vol. 7, Cambridge, 1986.Google Scholar
[32]Lamo, Yngve, The institution of multialgebras—a general framework for algebraic software development, PhD thesis, University of Bergen, 2003.Google Scholar
[33]Lane, Saunders Mac, Categories for the working mathematician, second ed., Springer, 1998.Google Scholar
[34]Matthiessen, G., Regular and strongly finitary structures over strongly algebroidal categories, Canadian Journal of Mathematics, vol. 30 (1978), pp. 250–261.CrossRefGoogle Scholar
[35]Meseguer, José, General logics, Logic Colloquium, 1987 (Ebbinghaus, H.-D.et al., editors), North-Holland, 1989, pp. 275–329.Google Scholar
[36]Meseguer, José, Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, vol. 96 (1992), no. 1, pp. 73–155.CrossRefGoogle Scholar
[37]Meseguer, José, Membership algebra as a logical framework for equational specification, Proceedings of the WADT'97 (Parisi-Pressice, F., editor), Lecture Notes in Computer Science, no. 1376, Springer, 1998, pp. 18–61.Google Scholar
[38]Mossakowski, Till, Specification in an arbitrary institution with symbols, Recent trends in Algebraic Development Techniques, 14th International Workshop, WADT'99, Bonos, France (Choppy, C., Bert, D., and Mosses, P., editors), Lecture Notes in Computer Science, vol. 1827, Springer-Verlag, 2000, pp. 252–270.CrossRefGoogle Scholar
[39]Mossakowski, Till, Relating CASL with other specification languages: the institution level, Theoretical Computer Science, vol. 286 (2002), pp. 367–475.CrossRefGoogle Scholar
[40]Mossakowski, Till, Goguen, Joseph, Diaconescu, Răzvan, and Tarlecki, Andrzej, What is a logic?, Logica universalis (Beziau, Jean-Yves, editor), Birkh pp. 113–133.Google Scholar
[41]Németi, IstvÁn and Sain, Ildikó, Cone-implicational subcategories and some Birkhoff-type theorems, Universal algebra (Csakany, B., Fried, E., and Schmidt, E. T., editors), North-Holland, 1981, Colloquia Mathematics Societal JÁnos Bolyai, 29, pp. 535–578.Google Scholar
[42]Popescu, Andrei, Şerbănuţă, Traian, and Roşu, Grigore, A semantic approach to interpolation, submitted.Google Scholar
[43]Rodenburg, Pieter-Hendrik, A simple algebraic proof of the equational interpolation theorem, Algebra Universalis, vol. 28 (1991), pp. 48–51.CrossRefGoogle Scholar
[44]Sannella, Donald and Tarlecki, Andrzej, Specifications in an arbitrary institution, Information and Control, vol. 76 (1988), pp. 165–210, earlier version in Proceedings, International Symposium on the Semantics of Data Types, Lecture Notes in Computer Science, vol. 173, Springer, 1985.Google Scholar
[45]Schröder, Lutz, Mossakowski, Till, and Lüth, Christoph, Type class polymorphism in an institutional framework, Recent trends in Algebraic Development Techniques, 17th International Workshop (WADT 2004) (Fiadeiro, José, editor), Lecture Notes in Computer Science, vol. 3423, Springer, Berlin, 2004, pp. 234–248.CrossRefGoogle Scholar
[46]Shoenfield, Joseph, Mathematical logic, Addison-Wesley, 1967.Google Scholar
[47]Tarlecki, Andrzej, Bits and pieces of the theory of institutions, Proceedings, Summer Workshop on Category Theory and Computer Programming (Pitt, David, Abramsky, Samson, Poigneé, Axel, and Rydeheard, David, editors), Lecture Notes in Computer Science, vol. 240, Springer, 1986, pp. 334–360.CrossRefGoogle Scholar
[48]Tarlecki, Andrzej, On the existence of free models in abstract algebraic institutions, Theoretical Computer Science, vol. 37 (1986), pp. 269–304, preliminary version, University of Edinburgh, Computer Science Department, Report CSR-165-84, 1984.CrossRefGoogle Scholar
[49]Tarlecki, Andrzej, Quasi-varieties in abstract algebraic institutions, Journal of Computer and System Sciences, vol. 33 (1986), no. 3, pp. 333–360, original version, University of Edinburgh, Report CSR-173-84.CrossRefGoogle Scholar
[50]Tarlecki, Andrzej, Moving between logical systems, Recent trends in data type specification (Haveraaen, Magne, Owe, Olaf, and Dahl, Ole-Johan, editors), Lecture Notes in Computer Science, Springer, 1996, pp. 478–502.CrossRefGoogle Scholar
[51]Tarlecki, Andrzej, Towards heterogeneous specifications, Proceedings, International Conference on Frontiers of Combining Systems (FroCoS'98) (Gabbay, D. and Rijke, M. van, editors), Research Studies Press, 2000, pp. 337–360.Google Scholar
[52]Veloso, Paulo, On pushout consistency, modularity and interpolation for logical specifications, Information Processing Letters, vol. 60 (1996), no. 2, pp. 59–66.CrossRefGoogle Scholar