3
$\begingroup$

TL;DR: "It is also fundamental that sentences translate in the same direction as the change of notation, whereas models translate in the opposite direction." (Goguen, Institutions: Abstract model theory for specification and programming, p. 101). Why?

Institutions are typically defined as 4-tuples $I = (\mathbf{Sign},\textit{sen},\mathbf{Mod},\models)$ (see e.g. Goguen, Diaconescu, or Meseguer, which is the one I'm spending the most time on), where in particular $\mathbf{Mod}$ is a functor $\mathbf{Mod} : \mathbf{Sign}^{\textit{op}} \to \mathbf{Cat}$ (or also sometimes defined as $\mathbf{Mod}$ is a functor $\mathbf{Mod} : \mathbf{Sign} \to \mathbf{Cat}^{\textit{op}}$).

I cannot for the life of me figure out how it works, and why we're working with duals (a.k.a. opposites).

My thinking thus far has been: We two signatures, $\Sigma$ and $\Sigma'$, a signature morphism $H:\Sigma\to\Sigma'$, and... a $\Sigma'$-Model $M'$? Why not a $\Sigma$-Model $M$? But ignoring that question for now, say $M' = (\{a,b,c,abc,baca\},\{f^{\mathcal{A}'},g^{\mathcal{A}'}\})$ ($a$ through $c$ being constant symbols and f and g function symbols, with the superscript ($\mathcal{A}'=\{a,b,c,abc,baca\}$ Edit: This is not what underlying sets look like, and this faulty assumption is what caused my confusion.) referring to their particular interpretations). How do we transform this into a $\Sigma$-model $M$? We can't translate $\mathcal{A}'$ into $\mathcal{A} = \{1,2,3,123,2131\}$, because our signature morphism is in the wrong direction, and the same goes for the function symbols. We can, yes, if we already knew the corresponding function symbols in $\Sigma$ (say $6$ and $7$) associate to them the interpretation associated with $\textit{sen}(H)(6) = f$ and $\textit{sen}(H)(7) = g$, respectively (though I'm also not sure how that works), but aside from that I'm incredibly confused, and been so for many hours. I love the generality of it all but apparently my brain / zero mathematical maturity can't handle it.

Any help would be much appreciated.

Thanks and happy holidays!

Diaconescu, Răzvan, Institution-independent model theory, Studies in Universal Logic. Basel: Birkhäuser (ISBN 978-3-7643-8707-5/pbk). xi, 376 p. (2008). ZBL1144.03001.

Goguen, Joseph A.; Burstall, Rod M., Institutions: Abstract model theory for specification and programming, J. Assoc. Comput. Mach. 39, No. 1, 95-146 (1992). ZBL0799.68134.

Goguen, J. A.; Burstall, R. M., Introducing institutions, Logics of programs, Workshop, Pittsburgh/PA 1983, Lect. Notes Comput. Sci. 164, 221-256 (1984). ZBL0543.68021.

Meseguer, José, General logics, Logic colloq. ’87, Proc. Colloq., Granada/Spain 1987, Stud. Logic Found. Math. 129, 275-329 (1989). ZBL0691.03001.

$\endgroup$
  • $\begingroup$ In the usual model theory, signatures are languages. Sentences are expression of the language (without free variables). Models are mathematical objects (structures) used to interpret the language and $\vDash$ is the satisfaction relation between a model $M$ and a sentence $\varphi$ such that $M \vDash \varphi$ iff the sentence holds (is TRUE) in the structure $M$. $\endgroup$ – Mauro ALLEGRANZA Dec 19 '19 at 14:31
  • $\begingroup$ In Diaconescu's approach they are expressed in category theory language. $\endgroup$ – Mauro ALLEGRANZA Dec 19 '19 at 14:33
  • $\begingroup$ The functor $\text {Mod}^I$ is a functor that maps every signature $\Sigma$ (an object in $\text {Sig}^I$ is a signature) into the category whose objects are the models of $\Sigma$. $\endgroup$ – Mauro ALLEGRANZA Dec 19 '19 at 14:36
  • $\begingroup$ Yes, that part I understand (third comment), but it's $\text{Mod}^I$ mapping signature morphisms that confuses me $\endgroup$ – BlondCafé Dec 19 '19 at 14:39
4
$\begingroup$

Suppose you have a signature morphism $H:\Sigma\to \Sigma'$ and $M$ is a $\Sigma'$-model. Then you can define a $\Sigma$-model $H^*M$ with the same underlying set as $M$, where for each $\sigma\in\Sigma$ the function or relation $\sigma_{H^*M}$ is defined to be $H(\sigma)_M$. In other words, to interpret a symbol $\sigma$ in $\Sigma$ on $M$, you just use the interpretation of $H(\sigma)$, and in this way $M$ turns into a $\Sigma$-model.

In this way, a morphism $H:\Sigma\to\Sigma'$ gives a way of turning $\Sigma'$-models into $\Sigma$-models, and it is easy to check that this also turns $\Sigma'$-homomorphisms into $\Sigma$-homomorphisms and thus induces a functor $\mathbf{Mod}(\Sigma')\to\mathbf{Mod}(\Sigma)$. This makes $\mathbf{Mod}$ a functor $\mathbf{Sign}\to\mathbf{Cat}^{op}$: it sends an object $\Sigma$ to the category $\mathbf{Mod}(\Sigma)$, and a morphism $H:\Sigma\to\Sigma'$ to a functor $\mathbf{Mod}(\Sigma')\to\mathbf{Mod}(\Sigma)$ and you can check that this preserves identities and composition.

(To be clear, here I am assuming you are working with the "standard" institution of classical model theory. The point of institutions is to make an abstract definition which captures similar formal behavior to classical and other model theories. So in a general institution, "models" don't have to be anything like models in classical model theory as I described here; they just have to (together with the rest of the 4-tuple) satisfy the definition of an institution. The story above is motivation for why instutitions are defined they way they are, with $\mathbf{Mod}$ being contravariant.)

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ It seems like I had the (apparently faulty) assumption that the underlying set is dependent upon the signature. So... that's not the case? $\endgroup$ – BlondCafé Dec 19 '19 at 15:25
  • $\begingroup$ I don't even know what that means. A model can have any underlying set at all, as long as you also provide interpretations of everything in the signature for that set. $\endgroup$ – Eric Wofsey Dec 19 '19 at 15:26
  • $\begingroup$ Well I thought the underlying set of a $\Sigma$-model would always have to be a subset of $\textit{sen}(\Sigma)$. So, to reiterate, that's not true? $\endgroup$ – BlondCafé Dec 19 '19 at 15:28
  • 1
    $\begingroup$ Correct, that is not true. The elements of a $\Sigma$-model typically have nothing to do with sentences. $\endgroup$ – Eric Wofsey Dec 19 '19 at 15:30
  • $\begingroup$ Okay that changes everything. It makes sense now. Thank you so much! $\endgroup$ – BlondCafé Dec 19 '19 at 15:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.