Universal Logic

Institution theory is a major model theoretic trend of universal logic that formalizes within category theory the intuitive notion of a logical system, including syntax, semantics, and the satisfaction relation between them.
It arose within computing science, especially specification theory[1], as a response to the population explosion of logics there and where it has become the most important foundational theory Later on institution theory has been succesfully used in pure logic studies in the spirit of universal logic.
This means the development of model and proof theory in the very abstract setting of arbitrary institutions, free of commitement to a particular logical system [2].
In this way we gain freedom to live without concrete models, sentences satisfaction, and so on, we gain another level of abstraction and generality and a deeper understanding of model theoretic phenomena not hindered by the largely irrelevant details of a particular logical system, but guided by structurally clean causality.
The latter aspect is based upon the fact that concepts come naturally as presumed features that a ``logic'' might exhibit or not and are defined at the most appropriate level of abstraction; hypotheses are kept as general as possible and introduced on a by-need basis, and thus results and proofs are modular and easy to track down regardless of their depth.
The continuous interplay between the specific and the general in institution theory brings a large array of new results for particular non-conventional, unifies several known results, produces new results in well-studied conventional areas, reveals previously unknown causality relations, and dismantles some which are usually assumed as natural. Access to highly non-trivial results is also considerably facilitated.
The dynamic role played by institution theory within the wider universal logic project is illustrated by the fact that institution theory papers have come second and first, respectively, in the contests of the Montreux (2005) and Xi'and (2007) UNILOG, respectively.



	Theory of Institutions Razvan Diaconescu Institute of Mathematics "Simion Stoilow" Bucharest, Romania
Institution theory is a major model theoretic trend of universal logic that formalizes within category theory the intuitive notion of a logical system, including syntax, semantics, and the satisfaction relation between them. It arose within computing science, especially specification theory[1], as a response to the population explosion of logics there and where it has become the most important foundational theory Later on institution theory has been succesfully used in pure logic studies in the spirit of universal logic. This means the development of model and proof theory in the very abstract setting of arbitrary institutions, free of commitement to a particular logical system [2]. In this way we gain freedom to live without concrete models, sentences satisfaction, and so on, we gain another level of abstraction and generality and a deeper understanding of model theoretic phenomena not hindered by the largely irrelevant details of a particular logical system, but guided by structurally clean causality. The latter aspect is based upon the fact that concepts come naturally as presumed features that a ``logic'' might exhibit or not and are defined at the most appropriate level of abstraction; hypotheses are kept as general as possible and introduced on a by-need basis, and thus results and proofs are modular and easy to track down regardless of their depth. The continuous interplay between the specific and the general in institution theory brings a large array of new results for particular non-conventional, unifies several known results, produces new results in well-studied conventional areas, reveals previously unknown causality relations, and dismantles some which are usually assumed as natural. Access to highly non-trivial results is also considerably facilitated. The dynamic role played by institution theory within the wider universal logic project is illustrated by the fact that institution theory papers have come second and first, respectively, in the contests of the Montreux (2005) and Xi'and (2007) UNILOG, respectively.
		In this tutorial we will start with a brief explanation of the historical and philosophical origins of institution theory, followed by a presentation of its basic mathematical concepts. We will also have a trip through the rather rich body of methods and results of the institution theoretic approach to logic and model theory. Although institution theory is primarily a model theoretic approach we will also discuss recent proof theoretic developments in the area. However our real emphasis will be not on the actual mathematical developments but on the non-substantialist way of thinking and the top-down methodologies promoted by institution theory, that contrast sharply the substantialist view and the bottom-up methodologies that pervade and underly conventional logic, this being the most profound message of institution theory as a universal logic trend. References: [1] J. Goguen, R. Burstall, Institutions: Abstract Model Theory for Specification and Programming, J.ACM 39(1) 95-146, 1992. [2] R. Diaconescu, Institution-independent Model Theory, Birkhauser, 2008.