# Adjunction between classic and intuitionistic logic

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.

-
It seems that there is a problem with latex, and I am unable to fix it (I tried the same text on my local latex processor and everything was fine). Is it a bug in the web-site? –  Michal R. Przybylek Mar 16 '11 at 20:23
If there are LaTeX problems, usually it is caused by special characters being interpreted as markdown commands - the two solutions are either to put backslashes in front of the offending symbols, or to enclose the math dollar signs with backticks (see mathoverflow.net/faq#latex). I surmise that, since the dollar sign is not a markdown special character, the backslash won't be removed when it is escaped, and that this is why the example given in the FAQ looks like '\$...\$'. –  Zev Chonoles Mar 16 '11 at 21:04
Thank you for the comment and for fixing my text. –  Michal R. Przybylek Mar 16 '11 at 22:08
What are the morphisms of $\mathit{Mod}_H(\Sigma)$? –  Emil Jeřábek Mar 17 '11 at 12:18
The usual homomorphisms of algebras, which are monotonic on logical values (i.e. if r is a relation symbol then r(h(x_1), ..., h(x_n)) >= r(x_1, ..., x_n)). –  Michal R. Przybylek Mar 17 '11 at 13:02