Subquasivarieties of implicative locally‐finite quasivarieties

A quasivariety is said to be implicative if it is generated by a class of algebras with equationally‐definable implication of equalities. Implicative finitely‐generated quasivarieties appear naturally within logic, for instance, as equivalent quasivarieties of Gentzen‐style calculi for finitely‐valued propositional logics with equality determinant (cf. [17], [18, Subsection 7.5] and Section A). Furthermore, any discriminator quasivariety is implicative. We prove that, for any implicative locally‐finite quasivariety ? and any skeleton S of the class of all finite ?‐simple members of ?, the image of the first component of a natural Galois connection between the dual poset of subquasivarieties of ? and the poset of all sets of finite subsets of S is the closure system of all U_S‐ideals of the poset 〈S, ?〉, where ? is the embeddability relation and U_S is the up‐set on S constituted by all members of S having a one‐element subalgebra, with closure basis determined by the sets of all principal and non‐empty finitely‐generated up‐sets on S. It is also shown that the first component of the Galois connection under consideration is injective if and only if, for each finite sequence