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

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?

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.

• May I inquire about the source for this? Mar 23 at 13:55
• See e.g. Chagrov and Zakharyaschev, Modal logic. Mar 23 at 17:59
• Thank you for your comment! Mar 24 at 7:38