Institution (computer science)

<h2 id="definition">Definition</h2>
<p>The theory of institutions does not assume anything about the nature of the logical system. That is, <a href="/facts/Interpretation_(logic)/goPmjjQG">models</a> and <a href="/facts/Sentence_(mathematical_logic)/lnsLzvTx">sentences</a> may be arbitrary objects; the only assumption is that there is a satisfaction relation between models and sentences, telling whether a sentence holds in a model or not. Satisfaction is inspired by <a href="/facts/T-schema/zNkFFSHD">Tarski's truth definition</a>, but can in fact be any binary relation.
A crucial feature of institutions is that models, sentences, and their satisfaction, are always considered to live in some vocabulary or context (called <a href="/facts/Signature_(logic)/C0YQCuce">signature</a>) that defines the (non-logic) symbols that may be used in sentences and that need to be interpreted in models. Moreover, signature morphisms allow to extend signatures, change notation, and so on. Nothing is assumed about signatures and signature morphisms except that signature morphisms can be composed; this amounts to having a 
<a href="/facts/Category_(mathematics)/7WzxUThf">category</a> of signatures and morphisms. Finally, it is assumed that signature morphisms lead to translations of sentences and models in a way that satisfaction is preserved. While sentences are translated along with signature morphisms (think of symbols being replaced along the morphism), models are translated (or better: reduced) against signature morphisms. For example, in the case of a signature extension, a model of the (larger) target signature may be reduced to a model of the (smaller) source signature by just forgetting some components of the model.
</p><p>Let 
  
    
      
        
          
            C
            a
            t
          
          
            
              o
              p
            
          
        
      
    
    {\displaystyle \mathbf {Cat} ^{\mathrm {op} }}
  
 denote the <a href="/facts/Opposite_category/swDy8NrJ">opposite</a> of the <a href="/facts/Category_of_small_categories/BJt1bdM7">category of small categories</a>. An institution formally consists of
</p>
<ul><li>a <a href="/facts/Category_(mathematics)/7WzxUThf">category</a> 
  
    
      
        
          S
          i
          g
          n
        
      
    
    {\displaystyle \mathbf {Sign} }
  
 of signatures,</li>
<li>a <a href="/facts/Functor/l2u3rIBE">functor</a> 
  
    
      
        
          
            S
            e
            n
          
        
        :
        
          S
          i
          g
          n
        
        →
      
    
    {\displaystyle {\mathit {Sen}}\colon \mathbf {Sign} \to }
  
 <a href="/facts/Category_of_sets/LF5ykYl0">
  
    
      
        
          S
          e
          t
        
      
    
    {\displaystyle \mathbf {Set} }
  
</a> giving, for each signature 
  
    
      
        Σ
      
    
    {\displaystyle \Sigma }
  
, the set of sentences 
  
    
      
        
          
            S
            e
            n
          
        
        (
        Σ
        )
      
    
    {\displaystyle {\mathit {Sen}}(\Sigma )}
  
, and for each signature morphism 
  
    
      
        σ
        :
        Σ
        →
        
          Σ
          ′
        
      
    
    {\displaystyle \sigma \colon \Sigma \to \Sigma '}
  
, the sentence translation map 
  
    
      
        
          
            S
            e
            n
          
        
        (
        σ
        )
        :
        
          
            S
            e
            n
          
        
        (
        Σ
        )
        →
        
          
            S
            e
            n
          
        
        (
        
          Σ
          ′
        
        )
      
    
    {\displaystyle {\mathit {Sen}}(\sigma )\colon {\mathit {Sen}}(\Sigma )\to {\mathit {Sen}}(\Sigma ')}
  
, where often 
  
    
      
        
          
            S
            e
            n
          
        
        (
        σ
        )
        (
        φ
        )
      
    
    {\displaystyle {\mathit {Sen}}(\sigma )(\varphi )}
  
 is written as 
  
    
      
        σ
        (
        φ
        )
      
    
    {\displaystyle \sigma (\varphi )}
  
,</li>
<li>a <a href="/facts/Functor/l2u3rIBE">functor</a> 
  
    
      
        
          M
          o
          d
        
        :
        
          S
          i
          g
          n
        
        →
        
          
            C
            a
            t
          
          
            
              o
              p
            
          
        
      
    
    {\displaystyle \mathbf {Mod} \colon \mathbf {Sign} \to \mathbf {Cat} ^{\mathrm {op} }}
  
 giving, for each signature 
  
    
      
        Σ
      
    
    {\displaystyle \Sigma }
  
, the category of models 
  
    
      
        
          M
          o
          d
        
        (
        Σ
        )
      
    
    {\displaystyle \mathbf {Mod} (\Sigma )}
  
, and for each signature morphism 
  
    
      
        σ
        :
        Σ
        →
        
          Σ
          ′
        
      
    
    {\displaystyle \sigma \colon \Sigma \to \Sigma '}
  
, the reduct functor 
  
    
      
        
          M
          o
          d
        
        (
        σ
        )
        :
        
          M
          o
          d
        
        (
        
          Σ
          ′
        
        )
        →
        
          M
          o
          d
        
        (
        Σ
        )
      
    
    {\displaystyle \mathbf {Mod} (\sigma )\colon \mathbf {Mod} (\Sigma ')\to \mathbf {Mod} (\Sigma )}
  
, where often 
  
    
      
        
          M
          o
          d
        
        (
        σ
        )
        (
        
          M
          ′
        
        )
      
    
    {\displaystyle \mathbf {Mod} (\sigma )(M')}
  
 is written as 
  
    
      
        
          M
          ′
        
        
          
            |
          
          
            σ
          
        
      
    
    {\displaystyle M'|_{\sigma }}
  
,</li>
<li>a satisfaction <a href="/facts/Binary_relation/r9BwGgaK">relation</a> 
  
    
      
        
          
            ⊨
            
              Σ
            
          
        
        ⊆
        
          |
        
        
          
            M
            o
            d
          
          (
          Σ
          )
          
            |
          
          ×
          
            
              S
              e
              n
            
          
          (
          Σ
          )
        
      
    
    {\displaystyle {\models _{\Sigma }}\subseteq |{\mathbf {Mod} (\Sigma )|\times {\mathit {Sen}}(\Sigma )}}
  
 for each 
  
    
      
        Σ
        ∈
        
          S
          i
          g
          n
        
      
    
    {\displaystyle \Sigma \in \mathbf {Sign} }
  
,</li></ul>
<p>such that for each 
  
    
      
        σ
        :
        Σ
        →
        
          Σ
          ′
        
      
    
    {\displaystyle \sigma \colon \Sigma \to \Sigma '}
  
 in 
  
    
      
        
          S
          i
          g
          n
        
      
    
    {\displaystyle \mathbf {Sign} }
  
, the following satisfaction condition  holds:
</p><p>
  
    
      
        
          M
          ′
        
        
          ⊨
          
            
              Σ
              ′
            
          
        
        σ
        (
        φ
        )
        
        
          if and only if
        
        
        
          M
          ′
        
        
          
            |
          
          
            σ
          
        
        
          ⊨
          
            Σ
          
        
        φ
      
    
    {\displaystyle M'\models _{\Sigma '}\sigma (\varphi )\quad {\text{if and only if}}\quad M'|_{\sigma }\models _{\Sigma }\varphi }

</p><p>for each 
  
    
      
        
          M
          ′
        
        ∈
        
          M
          o
          d
        
        (
        
          Σ
          ′
        
        )
      
    
    {\displaystyle M'\in \mathbf {Mod} (\Sigma ')}
  
 and 
  
    
      
        φ
        ∈
        
          
            S
            e
            n
          
        
        (
        Σ
        )
      
    
    {\displaystyle \varphi \in {\mathit {Sen}}(\Sigma )}
  
.
</p><p>The satisfaction condition expresses that truth is invariant under change of notation 
(and also under enlargement or quotienting of context).
</p><p>Strictly speaking, the model functor ends in the "category" of all large categories.
</p>
<h2 id="examples-of-institutions">Examples of institutions</h2>
<ul><li><a href="/facts/Common_logic/U6FJjVaL">Common logic</a></li>
<li><a href="/facts/Common_Algebraic_Specification_Language/DzHEY8Uu">Common Algebraic Specification Language</a> (CASL)</li>
<li><a href="/facts/First-order_logic/lcISqWIg">First-order logic</a></li>
<li><a href="/facts/Higher-order_logic/hdUhry6m">Higher-order logic</a></li>
<li><a href="/facts/Intuitionistic_logic/zI7ulCnM">Intuitionistic logic</a></li>
<li><a href="/facts/Modal_logic/I7uXvYYT">Modal logic</a></li>
<li><a href="/facts/Propositional_logic/MNt5v31V">Propositional logic</a></li>
<li><a href="/facts/Temporal_logic/vANP39lc">Temporal logic</a></li>
<li><a href="/facts/Web_Ontology_Language/jkr0IGn8">Web Ontology Language</a> (OWL)</li></ul>
<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Abstract_model_theory/BsboNQT6">Abstract model theory</a></li>
<li><a href="/facts/Institutional_model_theory/md6KVcL3">Institutional model theory</a></li>
<li><a href="/facts/Universal_logic/SqsTNhgI">Universal logic</a></li></ul>

<h2 id="further-reading">Further reading</h2>
<ul><li>J. A. Goguen; R. M. Burstall (1984), "Introducing institutions", in E. Clarke; D. Kozen (eds.), <i>Logics of Programs: Proceedings of the Logics of Programming Workshop 1983</i>, Lecture Notes in Computer Science, vol. 164, Springer, Berlin, Germany, pp. 221–256, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2F3-540-12896-4_366">10.1007/3-540-12896-4_366</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-3-540-12896-0. This was the first publication on institution theory and the preliminary version of Goguen and Burstall (1992).</li>
<li>J. Meseguer (1989), "General logics", in H.-D. Ebbinghaus; J. Fernandez-Prida; M. Garrido; D. Lascar; M. Rodriquez Artalejo (eds.), <i>Logic Colloquium '87: Proceedings of the Colloquium held in Granada, Spain</i>, vol. 129, Elservier, pp. 274–307</li>
<li>J. A. Goguen; G. Rosu (2002), "Institution morphisms", <i>Formal Aspects of Computing</i>, 13 (3–5): 274–307, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2Fs001650200013">10.1007/s001650200013</a>, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:5687318">5687318</a></li>
<li>D. Sannella; A. Tarlecki (1988), "Specifications in an arbitrary institution", <i>Information and Computation</i>, 76 (2–3): 165–210, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2F0890-5401%2888%2990008-9">10.1016/0890-5401(88)90008-9</a></li>
<li>R. Diaconescu (2008), <a href="https://www.springer.com/birkhauser/mathematics/book/978-3-7643-8707-5"><i>Institution-independent Model Theory</i></a>, Birkhäuser, Basel</li></ul>
<h2 id="external-links">External links</h2>
<ul><li>Răzvan Diaconescu, <a href="https://iep.utm.edu/insti-th/">"Institution Theory"</a>, <i>Internet Encyclopedia of Philosophy</i>, retrieved January 31, 2021</li>
<li>Joseph Goguen (2006), <a href="http://www-cse.ucsd.edu/users/goguen/projs/inst.html"><i>Institutions</i></a>, University of California, San Diego, retrieved January 31, 2021</li>
<li><a href="http://www.informatik.uni-bremen.de/flirts/"><i>Formalism, Logic, Institution - Relating, Translating and Structuring</i></a>. Includes large bibliography.</li>
<li>Răzvan Diaconescu, <a href="http://www.imar.ro/~diacon/publications.html#Institutions__institution-independent"><i>Selected Publications</i></a>, Simion Stoilow Institute of Mathematics of the Romanian Academy, retrieved January 31, 2021. Contains recent work on institutional model theory.</li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1"><p>J. A. Goguen; R. M. Burstall (1992), "Institutions: Abstract model theory for specification and programming", Journal of the ACM, 39 (1): 95–146, doi:10.1145/147508.147524, S2CID 16856895 <a href="/wiki/Doi_(identifier)" target="_blank">/wiki/Doi_(identifier)</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li>
<li id="fn:2"><p>Razvan Diaconescu (2012), "Three decades of institution theory", in Jean-Yves Béziau (ed.), Universal Logic: An Anthology, Springer, pp. 309–322 <a href="https://www.springer.com/gp/book/9783034601443" target="_blank">https://www.springer.com/gp/book/9783034601443</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li>
<li id="fn:3"><p>T. Mossakowski; J. A. Goguen; R. Diaconescu; A. Tarlecki (2007), "What is a logic?: In memoriam Joseph Goguen", in Jean-Yves Beziau (ed.), Logica Universalis: Towards a General Theory of Logic (2nd ed.), Birkhäuser, Basel, pp. 113–133, doi:10.1007/978-3-7643-8354-1_7 <a href="/wiki/Doi_(identifier)" target="_blank">/wiki/Doi_(identifier)</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li>
</ol>

Institution (computer science) open-in-new

Institution (computer science)