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?


2 Answers 2


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.


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$ May I inquire about the source for this? $\endgroup$ Mar 23 at 13:55
  • $\begingroup$ See e.g. Chagrov and Zakharyaschev, Modal logic. $\endgroup$ Mar 23 at 17:59
  • $\begingroup$ Thank you for your comment! $\endgroup$ Mar 24 at 7:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.