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

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.

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

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 complete 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 (i.e. the semantics of $\phi$ in $M$ is the top element of $H$). 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.
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 satisfiability relation: $M \models F_\mathit{log}(\phi) \Leftrightarrow F_\mathit{mod}(M) \models \phi$.
A morphism transformation $\alpha \colon F \rightarrow G$ consists of a pair of natural transformations $\langle \alpha\_\mathit{mod} \colon F\_\mathit{mod} \rightarrow G\_\mathit{mod}, \alpha\_\mathit{log} \colon F\_\mathit{log} \rightarrow G\_\mathit{log}\rangle$.

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 the two-valued boolean algebra? Note that the Kolmogorov transformation does not work here.

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

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

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.

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

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

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.

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