Whether the pure implicational fragment of intuitionistic propositional logic is a finitely-many valued logic

Question

Gödel (1932) showed that intuitionistic propositional logic (more precisely, any fragment with implication and disjunction) is not a finitely many-valued logic. What about the pure implicational fragment?

Answer 1

The pure implicational fragment of intuitionistic propositional logic is not finite-valued.

Take your favorite $k \in \mathbb{N}$. It's easy to find a disjunction $t_1 \vee t_2 \vee \dots \vee t_n$ of Heyting algebra terms so that each term in $t_1,t_2,\dots,t_n$ consists only of variables and implications, and the universal closure of $t_1 \vee t_2 \vee \dots \vee t_n = \top$ holds in every finite Heyting algebra $(H, \wedge, \vee, \rightarrow, \bot, \top)$ with $|H| = k$, but fails in some Heyting algebra with $|H| > k$. The usual proof of non-finite-valuedness for IPC itself already gives rise to such a disjunction.

We can turn this into a disjunction-free formula with similar properties using the intuitionistic tautology $(A \vee B) \rightarrow ((A \rightarrow C) \rightarrow (B \rightarrow C) \rightarrow C)$.

If we pick a variable $z$ which does not occur in the terms $t_1,\dots,t_n$, then the universal closure of the equality $$(t_1 \rightarrow z) \rightarrow (t_2 \rightarrow z) \rightarrow \dots \rightarrow (t_n \rightarrow z) \rightarrow z = \top$$ holds in the implicational reduct $(H, \rightarrow, \bot, \top)$ of any Heyting algebra with $|H| = k$, by the tautology above. But by construction, the left hand side of this equality belongs to the implicational fragment, and is certainly not an intuitionistic tautology.

Every finite structure $(H, \rightarrow, \bot, \top)$ which obeys the implicational fragment of intuitionistic logic in the sense that the universal closure of $t=\top$ holds if the term $t$ is a tautology of this fragment, arises as a reduct of some Heyting algebra: the solutions to $x \rightarrow y = \top$ uniquely determine the order, and the order induces the structure of a distributive lattice $(H, \wedge, \vee)$.

Thus, no finite $(H, \rightarrow, \bot, \top)$ provides a complete semantics for the implicational fragment of intuitionistic propositional logic.

Answer 2

A related property in which the implicational fragment differs from full intuitionistic logic is that the former is locally finite: for every finite $n$, there are only finitely many inequivalent formulas in $n$ variables. As a consequence, the $n$-variable implicational fragment is determined by a single finite Kripke frame (whose size depends on $n$); as another consequence, the implicational fragment of every superintuitionistic logic has the finite model property. More generally, all this holds also for the $\{\to,\land,\bot\}$-fragment. This is known as Diego's theorem.