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 sequenceof members of S and any subdirect product of, there is a covering C of the image ofsuch that, for each P ∈ , ∏ P is embeddable into . This condition (even with one‐element coverings) holds, for instance, when ℚ is discriminator or when ℚ has a set of binary terms satisfying semilattice identities while the direct product of any finite T ⊆ S is generated by corresponding semilattice zeros. We present several examples of quasivarieties which are equivalent to Gentzenstyle calculi for certain well‐known finitely‐valued logics with equality determinant, satisfy the latter sufficient condition of injectivity but are not congruence‐permutable, some of them having non‐simple relatively‐simple algebras. Moreover, we give an example of a quasivariety equivalent to Gentzen‐style calculi for some wellknown finitely‐valued logics with equality determinant, for which the first component of the Galois connection involved is not injective. We also apply our general elaboration to some discriminator quasivarieties, one of which is equivalent to no Gentzen‐style calculus associated with any finitely‐valued logic having an equality determinant while is equivalent to an extension of such a calculus (© 2010 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)