Let $\Sigma$ be a (classic, single-sorted) signature. Denote by $\mathit{Mod}\_H(\Sigma)$ the category of $H$-valued models over $\Sigma$, where $H$ is a Heyting algebra. Then for any first-order sentence $\phi$ over $\Sigma$ and any model $M \in \mathit{Mod}\_H(\Sigma)$ the satisfaction relation $M \models \phi$ in defined in the obvious way. Denote by $\mathit{Log}\_H(\Sigma)$ the category of first-order sentences over $\Sigma$, and "proofs" induced by the relation $\models$, that is: $\phi \rightarrow \psi \Leftrightarrow \forall\_M M \models \phi \Rightarrow M \models \psi$. We shall call such a triple $\langle\mathit{Mod}\_H(\Sigma), \models, \mathit{Log}\_H(\Sigma)\rangle$ a logical system.<br>
A morphism from a logical system $\langle\mathit{Mod}\_H(\Sigma), \models, \mathit{Log}\_H(\Sigma)\rangle$ to a logical system $\langle \mathit{Mod}\_K(\Sigma), \models, \mathit{Log}\_K(\Sigma)\rangle$ consists of a pair of functors $F\_\mathit{mod} \colon \mathit{Mod}\_K(\Sigma) \rightarrow \mathit{Mod}\_H(\Sigma)$ and $F\_\mathit{log} \colon \mathit{Log}\_H(\Sigma) \rightarrow \mathit{Log}\_K(\Sigma)$ (note opposite directions) compatible with the satisfability relation: $M \models F_\mathit{log}(\phi) \Leftrightarrow F_\mathit{mod}(M) \models \phi$. A morphism transformation consists of an obvious pair of natural transformations (in the same direction).<br><br>

Is there any interesting adjunction between $\langle\mathit{Mod}_H(\Sigma), \models, \mathit{Log}_H(\Sigma)\rangle$ and $\langle\mathit{Mod}_2(\Sigma), \models, \mathit{Log}_2(\Sigma)\rangle$, where $2$ is two-valued boolean algebra? Note that the Kolmogorov transformation does not work here.<br><br>

Appendix<br>
The truth is that $\mathit{Mod}_H(-)$ are fibred and $\mathit{Log}_H(-)$ are op-fibred over the category of signatures. Such entities (i.e. a fibration, an opfibration and a collection of satisfaction relations) are called "institutions". What I am really looking for is an interesting adjunction between such institutions. But this (modulo the Beck-Chevalley condition, what, I guess, is not an issue here) reduces to the above case.