Intermediate logics and strong algebraic completeness

Question

As a setup, suppose that you have a usual propositional language $\mathcal L$ over a set of propositional variables $Var$ and with symbols $\land,\lor,\rightarrow,\bot$ in the usual way. Let $L$ be an intermediate logic over $\mathcal L$, that is a set of $\mathcal L$-formulas containing intuitionistic propositional logic $IPC$, being contained in classical propositional logic $CPC$ and being closed under modus ponens and substitution of propositional variables.

A common semantics for intermediate logic is through Heyting algebras $\mathbf A$ and accompanying evaluations $f:Var\to\mathbf A$ which extend to the whole propositional language using the operations of the Heyting algebra. I write $(\mathbf A,f)\models\phi$ for $\phi\in\mathcal L$ if the value of $\phi$ under this extension of $f$ in $\mathbf A$ is the top-element of the Heyting algebra. Also, I write $(\mathbf A,f)\models\Gamma$ for $\Gamma\subseteq\mathcal L$ if $(\mathbf A,f)\models\gamma$ for all $\gamma\in\Gamma$.

My question is wether every intermediate logic $L$ has a strong algebraic completeness theorem, with respect to some class of Heyting algebras, in the sense of the following: does there exists a class of Heyting algebras $\mathsf C$ (relative to $L$) such that

$$\Gamma\vdash_L\phi\text{ iff }\forall\mathbf A\in\mathsf C\forall f:Var\to\mathbf A:(\mathbf A,f)\models\Gamma\Rightarrow (\mathbf A,f)\models\phi?$$

Answer 1

Yes, we can do this, and even in a beautifully precise way. This is a well-known result, but for some reason I do not directly know a good reference for this (anyone?). So it might be good to have this written out.

---

Most of our tools and definitions come from the realm of universal algebra, but we will just be interested in the bit about Heyting algebras.

Definition. A variety is a class of algebras satisfying a fixed set of equations.

In particular, for the language of Heyting algebras, this is a set of expressions of the form $\varphi = \psi$. Where $\varphi$ and $\psi$ are propositional formulas and this expression should be interpreted as "when we assign elements of our (Heyting) algebra to the propositional variables, then $\varphi$ and $\psi$ must evaluate to the same element in our (Heyting) algebra". If every algebra in the variety is a Heyting algebra, then $\varphi = \psi$ is equivalent to $\varphi \leftrightarrow \psi = \top$. So we may assume the equations to be of the latter form.

The class of Heyting algebras is a variety: it is precisely the class of algebras satsifying $IPC$.

Definition. Let $\mathsf{HA}$ denote the variety of Heyting algebras. For a Heyting algebra $A$, write $A \models \varphi$ if $\varphi$ evualates to the top element for every evaluation on $A$.

For a subvariety $V \subseteq \mathsf{HA}$ and a propositional formula $\varphi$ we write $V \models \varphi$ if $A \models \varphi$ for every $A \in V$. We define $$ L_V = \{\varphi \in \mathcal{L} : V \models \varphi \}. $$

Since $V \subseteq \mathsf{HA}$, one easily checks that $L_V$ is an intermediate logic.

Definition. Given an intermediate logic $L$ we let $V_L$ be the variety corresponding to the set of equations $\{ \varphi = \top : \varphi \in L \}$.

By construction $V_L \models L$ and $V_L \subseteq \mathsf{HA}$. Furthermore, it should be clear that for $V \subseteq V'$ we have $L_V \supseteq L_{V'}$. And for $L \supseteq L'$, we have $V_L \subseteq V_{L'}$.

Theorem. The operations $L \mapsto V_L$ and $V \mapsto L_V$ are inverses to each other.

In particular if we let $\mathcal{H}$ be the collection of all subvarietes of $\mathsf{HA}$ and we let $\mathcal{I}$ be the collection of intermediate logics. Then the partial orders $(\mathcal{H}, \subseteq)$ and $(\mathcal{I}, \supseteq)$ are isomorphic.

The following will be useful in the proof of the theorem.

Definition. For an intermediate logic $L$, let $A_L$ be the Heyting algebra defined as follows. Its elements are equivalence classes of propositional formulas, where formulas $\varphi$ and $\psi$ are equivalent if $\varphi \leftrightarrow \psi \in L$. Denote by $[\varphi] \in A_L$ the equivalence class of $\varphi$. The order on $A_L$ is given by $[\varphi] \leq [\psi]$ iff $\varphi \to \psi \in L$. We call $A_L$ the Lindenbaum-Tarski algebra for $L$.

Note that $A_L \models L$, so in particular $A_L \in V_L$.

Proof of theorem. We first prove $L = L_{V_L}$. Since $V_L \models L$ we have $L \subseteq L_{V_L}$. For $\varphi \in L_{V_L}$ we must have $V_L \models \varphi$, and thus in particular $A_L \models \varphi$. So $[\varphi] = [\top]$ in $A_L$, and hence $\varphi \in L$.

Now we prove $V = V_{L_V}$. Let $A \in V$, then $A \models L_V$ hence $A \in V_{L_V}$. For the other inclusion, let $\Sigma$ be a set of equations such that $V$ consists of all those algebras satisfying $\Sigma$. Then $\Sigma \subseteq L_V$. Hence for $A \in V_{L_V}$ we have $A \models \Sigma$ and thus $A \in V$. This completes the proof.

Note. I did not exclude the trivial variety containing the degenerate algebra (consisting of just one point). This corresponds to the inconsistent logic. If you want to only consider consistent logics (i.e. logics contained in $CPC$), then on the other side we have to restrict to all varietes containing the variety of Boolean algebras.

---

In your original question there does also appear a $\Gamma$. However, this is not really doing anything. For an intermediate logic $L$, let $\langle L, \Gamma \rangle$ be the intermediate logic generated by $L$ and $\Gamma$ (i.e. the intersection of all intermediate logics containing both $L$ and $\Gamma$). Then we have $\Gamma \vdash_L \varphi$ iff $\emptyset \vdash_{\langle L, \Gamma \rangle} \varphi$. So the class you are interested in is the variety $V_{\langle L, \Gamma \rangle}$.