A 2-categorial Generalization of the Concept of Institution

Authors: Climent Vidal, J.1; Soliveres Tur, J.2

Source: Studia Logica, Volume 95, Number 3, August 2010 , pp. 301-344(44)

Publisher: Springer

Buy & download fulltext article:


Price: $47.00 plus tax (Refund Policy)


After defining, for each many-sorted signature Σ = (S, Σ), the category Ter(Σ), of generalized terms for Σ (which is the dual of the Kleisli category for $${\mathbb {T}_{\bf \Sigma}}$$ , the monad in Set S determined by the adjunction $${{\bf T}_{\bf \Sigma} \dashv {\rm G}_{\bf \Sigma}}$$ from Set S to Alg(Σ), the category of Σ-algebras), we assign, to a signature morphism d from Σ to Λ, the functor $${{\bf d}_\diamond}$$ from Ter(Σ) to Ter(Λ). Once defined the mappings that assign, respectively, to a many-sorted signature the corresponding category of generalized terms and to a signature morphism the functor between the associated categories of generalized terms, we state that both mappings are actually the components of a pseudo-functor Ter from Sig to the 2-category Cat. Next we prove that there is a functor TrΣ, of realization of generalized terms as term operations, from Alg(Σ) × Ter(Σ) to Set, that simultaneously formalizes the procedure of realization of generalized terms and its naturalness (by taking into account the variation of the algebras through the homomorphisms between them). We remark that from this fact we will get the invariance of the relation of satisfaction under signature change. Moreover, we prove that, for each signature morphism d from Σ to Λ, there exists a natural isomorphism d from the functor $${{{\rm Tr}^{\bf {\bf \Lambda}} \circ ({\rm Id} \times {\bf d}_\diamond)}}$$ to the functor $${{\rm Tr}^{\bf \Sigma} \circ ({\bf d}^* \times {\rm Id})}$$ , both from the category Alg(Λ) × Ter(Σ) to the category Set, where d* is the value at d of the arrow mapping of a contravariant functor Alg from Sig to Cat, that shows the invariant character of the procedure of realization of generalized terms under signature change. Finally, we construct the many-sorted term institution by combining adequately the above components (and, in a derived way, the many-sorted specification institution), but for a strict generalization of the standard notion of institution.

Keywords: 2-institution on a category; Kleisli construction; Many-sorted algebra; generalized term; institution on a category

Document Type: Research Article

DOI: http://dx.doi.org/10.1007/s11225-010-9268-0

Affiliations: 1: Departamento de Lógica y Filosofía de la Ciencia, Universidad de Valencia, E-46010, Valencia, Spain, Email: Juan.B.Climent@uv.es 2: Departamento de Lógica y Filosofía de la Ciencia, Universidad de Valencia, E-46010, Valencia, Spain, Email: Juan.Soliveres@uv.es

Publication date: August 1, 2010

Related content


Free Content
Free content
New Content
New content
Open Access Content
Open access content
Subscribed Content
Subscribed content
Free Trial Content
Free trial content

Text size:

A | A | A | A
Share this item with others: These icons link to social bookmarking sites where readers can share and discover new web pages. print icon Print this page