Take the tour ×  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 func