The notion of institution has been created by Joseph Goguen and Rod Burstall in the early 1980's in order to deal with the "population explosion among the logical systems used in computer science". The notion tries to capture the essence of what a logical system is. With this, it is possible to develop concepts of specification languages (like structuring of specifications, parameterization, implementation, refinement, development), proof calculi and even tools in a way completely independent of the underlying logical system. There are also morphisms that allow to relate and translate logical systems. Important applications of this are re-use of logical structure (also called borrowing), heterogeneous specification and combination of logics. {vfd} Joseph Goguen - an independent thinker. ... Wikibooks Wikiversity has more about this subject: School of Computer Science Open Directory Project: Computer Science Collection of Computer Science Bibliographies Belief that title science in computer science is inappropriate Categories: Computer science | Academic disciplines ... Mathematical logic is a discipline within mathematics, studying formal systems in relation to the way they encode intuitive concepts of proof and computation as part of the foundations of mathematics. ... A specification language is a formal language used in computer science. ... Informally, we may say that a proof calculus determines a family of formal systems which specify inference rules that characterise a logical system. ... Modern hammer A tool is, among other things, a device that provides a mechanical or mental advantage in accomplishing a task. ...

Definition

An institution consists of

• a category Sign of signatures,
• a functor Set giving, for each signature Σ, the set of sentences sen(Σ), and for each signature morphism , the sentence translation map , where often is written as ,
• a functor Cat giving, for each signature Σ, the category of models Mod(Σ), and for each signature morphism , the reduct functor , where often Mod(σ)(M') is written as M' | _σ,
• a satisfaction relation for each ,

such that for each in Sign the following satisfaction condition holds: In mathematics, categories allow one to formalize notions involving abstract structure and processes which preserve structure. ... In category theory, a functor is a special type of mapping between categories. ... In mathematics, the category of sets is the category whose objects are all sets and whose morphisms are all functions. ... In category theory, a functor is a special type of mapping between categories. ... In mathematics, specifically in category theory, the 2-category of small categories is the 2-category whose objects are small categories, whose arrows are functors and whose 2-arrows are natural transformations. ... In mathematics, the concept of binary relation is exemplified by such ideas as is greater than and is equal to in arithmetic, or is congruent to in geometry, or is an element of or is a subset of in set theory. ...

iff

for each and .

The satisfaction condition expresses that truth is invariant under change of notation (and also under enlargement or quotienting of context).

Strictly speaking, the model functor ends in the quasi-category of all large categories.

Examples of Institutions

• First-order logic
• Higher-order logic
• Modal logic
• Temporal logic
• CASL

First-order predicate calculus or first-order logic (FOL) permits the formulation of quantified statements such as there exists an x such that. ... In mathematics, higher-order logic is distinguished from first-order logic in a number of ways. ... Modal logic, or (less commonly) intensional logic is the branch of logic that deals with sentences that are qualified by modalities such as can, could, might, may, must, possibly, and necessarily, and others. ... In logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. ...

Papers

• J. A. Goguen and R. M. Burstall, Introducing Institutions, Lecture Notes in Computer Science 164, pp. 221-256, 1984.
• J. A. Goguen and R. M. Burstall, Institutions: Abstract Model Theory for Specification and Programming, Journal of the Association for Computing Machinery 39, pp. 95-146, 1992.
• J. Meseguer, General Logics, Logic Colloquium 87, pp. 275-329, North Holland, 1989.
• J. A. Goguen and G. Rosu, Institution morphisms, Formal aspects of computing 13, pp. 274-307, 2002.
• D. Sannella and A. Tarlecki, Specifications in an arbitrary institution, Information and Computation 76, pp. 165-210, 1988
• T. Mossakowski, J. A. Goguen, R. Diaconescu, A. Tarlecki. What is a Logic?. In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113–133. Birkhäuser 2005.

External Links

• Institutions by Joseph Goguen
• Formalism, Logic, Institution - Relating, Translating and Structuring*

See also

• Entailment system
• Abstract model theory