Gödel (1932) showed that intuitionistic propositional logic (more precisely, any fragment with implication and disjunction) is not a finitely manyvalued logic. What about the pure implicational fragment?
2 Answers
The pure implicational fragment of intuitionistic propositional logic is not finitevalued.
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 nonfinitevaluedness for IPC itself already gives rise to such a disjunction.
We can turn this into a disjunctionfree 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.
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.


$\begingroup$ See e.g. Chagrov and Zakharyaschev, Modal logic. $\endgroup$ Mar 23 at 17:59
