Confusion about Mod functor in Institutions

78 Views Asked by At

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.

1

There are 1 best solutions below

5
On BEST ANSWER

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.)