The finite model property for the variety of Heyting algebras with successor

Abstract

The finite model property of the variety of S-algebras was proved by X. Caicedo using Kripke model techniques of the associated calculus. A more algebraic proof, but still strongly based on Kripke model ideas, was given by Muravitskii. In this article we give a purely algebraic proof for the finite model property which is strongly based on the fact that for every element x in a S-algebra the interval [x, S(x)] is a Boolean lattice.