On some compatible operations on Heyting algebras (Q763330)

The authors study certain operations on Heyting algebras that correspond to new connectives in intuitionistic logic. In this sense, the authors are interested in examining the operations that may be defined using the minimum operator. This motivation comes from the fact that already known compatible operations, such as the successor by Kuznetsov, the minimum dense by Smetanich and the operation \(G\) by Gabbay, may be defined in this way, though almost never explicitly noted in the literature, and that defining operations in this way is equivalent, from a logical point of view, to two clauses, one corresponding to an introduction rule and the other to an elimination rule, thus providing a manageable way to deal with these operations. One aim of this paper is to show that any operation defined by means of certain minimization scheme may be defined using the successor. A second aim is to extend Priestly duality between bounded distributive lattices and topological spaces to Heyting algebras with new operations.