Abstract
The notion of an Institution [5] is here taken as the precise formulation for the notion of a logical system. By using elementary tools from the core of category theory, we are able to reveal the underlying mathematical structures lying “behind” the logical formulation of the satisfaction condition, and hence to acquire a both suitable and deeper understanding of the institution concept. This allows us to systematically approach the problem of describing and analyzing relations between logical systems. Theorem 2.10 redesigns the notion of an institution to a purely categorical level, so that the satisfaction condition becomes a functorial (and natural) transformation from specifications to (subcategories of) models and vice versa. This systematic procedure is also applied to discuss and give a natural description for the notions of institution morphism and institution map. The last technical discussion is a careful and detailed analysis of two examples, which tries to outline how the new categorical insights could help in guiding the development of a unifying theory for relations between logical systems.
Research supported in part by a CNPq-grant 200529/94-3.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Arrais and J.L. Fiadeiro. Unifying theories in different institutions. In Proc. WADT11, Oslo, pages 81–101. Springer, LNCS 1130, 1996.
M. Cerioli and AMeseguer. May i borrow your logic? (transporting logical structures along maps). TCS, 173(2):311–347, 1997.
Maura Cerioli. Relationships between Logical Formalisms. PhD thesis, Università di Pisa-Genova-Udine, 1993. TD-4/93.
J. Goguen. A categorical manifesto. Mathematical Structures in Computer Science, 1(1):49–67, 1991.
J. A. Goguen and R. M. Burstall. Institutions: Abstract Model Theory for Specification and Programming. Journals of the ACM, 39(1):95–146, January 1992.
C. B. Jay. Extending properties to categories of partial maps. Technical Report LFCS 90–107, University of Edinburgh, LFCS, 1990.
J. Meseguer. General logics. In H.-D. Ebbinghaus et. al., editor, Logic colloquium '87, pages 275–329. Elsevier Science Publishers B. V., North Holland, 1989.
S. Salibra and G. Scollo. A soft stairway to institutions. In Recent Trends in Data Type Specification, pages 310–329. Springer, 1992. LNCS 655.
A. Tarlecki. Moving between logical systems. In Recent Trend's in Data Type Specification, pages 478–502. Springer, LNCS 1130, 1996.
A. Tarlecki, R.M. Burstall, and J.A. Goguen. Some fundamental algebraic tools for the semantics of computation. Part III: Indexed categories. TCS, 91:239–264, 1991.
U. Wolter. Institutional frames. In Recent Trends in Data Type Specification, pages 469–482. Springer, LNCS 906, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wolter, U., Martini, A. (1997). Shedding new light in the world of logical systems. In: Moggi, E., Rosolini, G. (eds) Category Theory and Computer Science. CTCS 1997. Lecture Notes in Computer Science, vol 1290. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0026987
Download citation
DOI: https://doi.org/10.1007/BFb0026987
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63455-3
Online ISBN: 978-3-540-69552-3
eBook Packages: Springer Book Archive