Institution-independent Ultraproducts

• Autorzy: Diaconescu R.
• Języki publikacji: EN

Abstrakty

EN

We generalise the ultraproducts method from conventional model theory to an institution-independent (i.e. independent of the details of the actual logic formalised as an institution) framework based on a novel very general treatment of the semantics of some important concepts in logic, such as quantification, logical connectives, and ground atomic sentences. Unlike previous abstract model theoretic approaches to ultraproducts based on category theory, our work makes essential use of concepts central to institution theory, such as signature morphisms and model reducts. The institution-independent fundamental theorem on ultraproducts is presented in a modular manner, different combinations of its various parts giving different results in different logics or institutions. We present applications to institution-independent compactness, axiomatizability, and higher order sentences, and illustrate our concepts and results with examples from four different algebraic specification logics. In the introduction we also discuss the relevance of our institution-independent approach to the model theory of algebraic specification and computing science, but also to classical and abstract model theory.

Słowa kluczowe

EN

institutions; model theory; algebraic specification; ultraproducts

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2003
• Tom: Vol. 55, nr 3,4
• Strony: 321--348
• Opis fizyczny: bibliogr. 36 poz.

Twórcy

autor

Diaconescu R.

• Institute of Mathematics "Simion Stoilow", PO Box 1-764, Bucharest 014700, Romania,

Bibliografia

• [1] Adamek, J., Herrlich, H., Strecker, G.: Abstract and Concrete Categories, John Wiley, 1990.
• [2] Adamek, J., Rossicki, J.: Locally Presentable and Accessible Categories, Number 189 in London Mathematical Society Lecture Notes, Cambridge Univ. Press, 1994.
• [3] Andréka, H., Németi, I.: Łoś Lemma Holds in Every Category, Studia Scientiarum Mathematicarum Hungarica, 13, 1978, 361-376.
• [4] Andréka, H., Németi, I.: A General Axiomatizability Theorem Formulated in Terms of Cone-Injective Subcategories, in: Universal Algebra (B. Csakany, E. Fried, E. Schmidt, Eds.), North-Holland, 1981, 13-35, Colloquia Mathematics Societas J´anos Bolyai, 29.
• [5] Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P., Sannella, D., Tarlecki, A.: CASL: The Common Algebraic Specification Language, Theoretical Computer Science, 286(2), 2002, 153-196.
• [6] Burmeister, P.: A Model Theoretic Approach to Partial Algebras, Akademie Verlag Berlin, 1986.
• [7] C.C.Chang, H.J.Keisler: Model Theory, North Holland, Amsterdam, 1990.
• [8] Diaconescu, R.: Institution-independent Model Theory, 2003, To appear.
• [9] Diaconescu, R.: An institution-independent proof of Craig Interpolation Theorem, Studia Logica, 76(3), 2004, To appear.
• [10] Diaconescu, R., Futatsugi, K.: Behavioural Coherence in Object-Oriented Algebraic Specification, Universal Computer Science, 6(1), 2000, 74-96, First version appeared as JAIST Technical Report IS-RR-98-0017F, June 1998.
• [11] Diaconescu, R., Futatsugi, K.: Logical Foundations of CafeOBJ, Theoretical Computer Science, 285, 2002, 289-318.
• [12] Diaconescu, R., Goguen, J., Stefaneas, P.: Logical Support for Modularisation, in: Logical Environments (G. Huet, G. Plotkin, Eds.), Cambridge, 1993, 83-130, Proceedings of a Workshop held in Edinburgh, Scotland, May 1991.
• [13] Diaconescu, R., Stefaneas, P.: Possible Worlds Semantics in arbitrary Institutions, 2003, Submitted to publication.
• [14] Frayne, T., Morel, A., Scott, D.: Reduced direct products, Fundamenta Mathematica, 51, 1962, 195-228.
• [15] Goguen, J., Burstall, R.: Institutions: Abstract Model Theory for Specification and Programming, Journal of the Association for Computing Machinery, 39(1), January 1992, 95-146.
• [16] Goguen, J., Malcolm, G., Kemp, T.: A Hidden Herbrand Theorem: Combining the Object, Logic and Functional Paradigms, Journal of Logic and Algebraic Programming, 51(1), 2002, 1-41.
• [17] Goguen, J., Meseguer, J.: Completeness of Many-sorted Equational Logic, Houston Journal of Mathematics, 11(3), 1985, 307-334.
• [18] Goguen, J., Ros¸u, G.: Hiding more of Hidden Algebra, FM’99 – Formal Methods (J. M. Wing, J. Woodcock, J. Davies, Eds.), 1709, Springer, 1999.
• [19] Grätzer, G.: Universal Algebra, Springer, 1979.
• [20] Hennicker, R., Bidoit, M.: Observational Logic, Algebraic Methodology and Software Technology (A. M. Haeberer, Ed.), number 1584 in LNCS, Springer, 1999, Proc. AMAST’99.
• [21] Hodges, W.: Model Theory, Cambridge University Press, 1993.
• [22] Łoś, J.: Quleques remarques, théor`emes et problèmes sur les classes définissables d’algèbres, in: Mathematical Interpretation of Formal Systems, North-Holland, Amsterdam, 1955, 98-113.
• [23] MacLane, S.: Categories for the Working Mathematician, Second edition, Springer, 1998.
• [24] Makkai, M.: Ultraproducts and Categorical Logic, in: Methods in Mathematical Logic (C. DiPrisco, Ed.), vol. 1130 of Lecture Notes in Mathematics, Springer Verlag, 1985, 222-309.
• [25] Makkai, M.: Stone Duality for First Order Logic, Advances in Mathematics, 65(2), 1987, 97-170.
• [26] Matthiessen, G.: Regular and strongly finitary structures over strongly algebroidal categories, Canad. J. Math., 30, 1978, 250-261.
• [27] Meseguer, J.: General Logics, in: Proceedings, Logic Colloquium, 1987 (H.-D. Ebbinghaus, et al., Eds.), North-Holland, 1989, 275-329.
• [28] Meseguer, J.: Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, 96(1), 1992, 73-155.
• [29] Meseguer, J.: A Logical Theory of Concurrent Objects and Its Realization in the Maude Language, in: Research Directions in Concurrent Object-Oriented Programming (G. Agha, P. Wegner, A. Yonezawa, Eds.), The MIT Press, 1993.
• [30] Reichel, H.: Structural Induction on Partial Algebras, Akademie Verlag Berlin, 1984.
• [31] Salibra, A., Scollo, G.: Interpolation and compactness in categories of pre-institutions, Mathematical Structures in Computer Science, 6, 1996, 261-286.
• [32] Sannella, D., Tarlecki, A.: Specifications in an Arbitrary Institution, Information and Control, 76, 1988, 165-210, Earlier version in Proceedings, International Symposium on the Semantics of Data Types, Lecture Notes in Computer Science, Volume 173, Springer, 1985.
• [33] Shoenfield, J.: Mathematical Logic, Addison-Wesley, 1967.
• [34] Tarlecki, A.: Bits and Pieces of the Theory of Institutions, in: Proceedings, Summer Workshop on Category Theory and Computer Programming (D. Pitt, S. Abramsky, A. Poignè, D. Rydeheard, Eds.), Springer, 1986, 334-360, Lecture Notes in Computer Science, Volume 240.
• [35] Tarlecki, A.: On the Existence of Free Models in Abstract Algebraic Institutions, Theoretical Computer Science, 37, 1986, 269-304, Preliminary version, University of Edinburgh, Computer Science Department, Report CSR-165-84, 1984.
• [36] Tarlecki, A.: Quasi-Varieties in Abstract Algebraic Institutions, Journal of Computer and System Sciences, 33(3), 1986, 333-360, Original version, University of Edinburgh, Report CSR-173-84.