On finite-dimensional superintuitionistic logics

A pseudoboolean algebra $\mathfrak M$ is called $n$-dimensional if the lattice $(Z_2)^{n+1}$ is not embeddable in $\mathfrak M$ as a lattice, where $Z_2$ is the two-element lattice. A superintuitionistic logic is said to be $n$-dimensional if the formula $E_n(x_1,\dots,x_n)\leftrightharpoons\bigvee_{i=1}^{n+1}(x_i=\bigvee_{j\ne i}x_j)$ belongs to it. A logic is $n$-dimensional if and only if it is approximable by $n$-dimensional algebras. All finite-dimensional logics are complete relative to Kripke semantics. An example is given of a formula that generates a logic not approximable by finite-dimensional algebras. It is proved that for every $n$, every finitely axiomatizable $n$-dimensional logic containing the formula $H(x,y)\leftrightharpoons(((x\to y)\to x)\to x)\vee (((y\to x)\to y)\to y)$ is decidable (already for $n=2$ there exist among such logics non-finitely-approximable ones). The proof uses the theory of finite automata on $\omega$-sequences.
Bibliography: 10 titles.