6533b839fe1ef96bd12a5997

RESEARCH PRODUCT

The parameterized local deduction theorem for quasivarieties of algebras and its application

subject

description

Let τ be an algebraic type. To each classK of τ-algebras a consequence relation ⊧ K defined on the set of τ-equations is assigned. Some weak forms of the deduction theorem for ⊧ K and their algebraic counterparts are investigated. The (relative) congruence extension property (CEP) and its variants are discussed.CEP is shown to be equivalent to a parameter-free form of the deduction theorem for the consequence ⊧ K .CEP has a strong impact on the structure ofK: for many quasivarietiesK,CEP implies thatK is actually a variety. This phenomenon is thoroughly discussed in Section 5. We also discuss first-order definability of relative principal congruences. This property is equivalent to the fact that the deduction theorem for ⊧ K is determined by a finite family of finite sets of equations. The following quasivarietal generalization of McKenzie's [26] finite basis theorem is proved: LetK be quasivariety of algebras of finite type in which the principalK-congruences are definable. ThenK is finitely axiomatizable iff either the classK FSI (of all relatively finitely subdirectly irreducible members ofK) or the class KSI (of all relatively subdirectly irreducible members ofK) is strictly elementary. Applications of the theory to Heyting, interior, Sugihara, and Łukasiewicz algebras are provided.