Heyting Algebras with Indiscernibility Relations

We introduce a class of algebraic structures, finite GBL-pairs, as pairs made of a finite Heyting algebra and a subgroup of its automorphism group. The group determines an equivalence relation on the Heyting algebra: we prove that the quotient, when endowed with suitable operations, is a GBL-algebra, and the operations can be interpreted as infima or suprema of equivalence classes. Conversely, we prove that every finite GBL-algebra can be represented as a GBL-pair. The motivation is to provide models for a fuzzy extension of intuitionistic propositional logic.