The word problem for \(Heyting^ *\) algebras (Q1095167)

A Heyting algebra with a unary operation \(a\mapsto a^*\) satisfying \(a\leq a^*\), \((a\cdot b)^*=a^*\cdot b^*\), and \((a\to b)^*\leq a+(a\to b)\) is called Heyting star algebra, or \(HA^*\) for short. Many properties of \(HA^*\)'s are inherited from their underlying Heyting algebras. For example, \(HA^*\) congruences coincide with Heyting algebra congruences, so that the HA* H is subdirectly irreducible if and only if it is subdirectly irreducible as a Heyting algebra. \textit{J. McKinsey} and \textit{A. Tarski} showed that every Heyting algebra has the finite embeddability property [Ann. Math., II. Ser. 47, 122-162 (1946; Zbl 0060.062)]. The principal result of this paper is that \(HA^*\)'s also have the finite embeddability property, from which it follows that the word problem for \(HA^*\)'s is solvable. The proof, which differs from the argument that is used for Heyting algebras, is based on a construction of subdirectly irreducible \(HA^*\)'s from an arbitrary \(HA^*\). The proof also shows that any finite \(HA^*\) can be embedded in the \(HA^*\) of open sets in some topological space with the operations \(M+N=M\cup N\), \(M\cdot N=M\cap N\), \(M\to N=int(N\cup M^ c)\), and \(M^*=((M^ c)')^ c\), where (') is the topological derivative.