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 intuitionistic 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.

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.

The 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 intuitionistic 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.

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 intuitionistic 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.