Almost structural completeness; an algebraic approach

A deductive system is structurally complete if all of its admissible inference rules are derivable. For several important systems, like the modal logic S5, failure of structural completeness is caused only by the underivability of a passive rule, i.e., a rule whose premise is not unifiable by any substitution. Neglecting passive rules leads to the notion of almost structural completeness, that means, to the derivability of admissible non-passive rules. We investigate almost structural completeness for quasivarieties and varieties of general algebras. The results apply to all algebraizable deductive systems.Firstly, various characterizations of almost structurally complete quasivarieties are presented. Two of them are general: the one expressed with finitely presented algebras, and the one expressed with subdirectly irreducible algebras. The next one is restricted to quasivarieties with the finite model property and equationally definable principal relative congruences, where the condition is verifiable on finite subdirectly irreducible algebras. Some connections with exact and projective unification are included.Secondly, examples of almost structurally complete varieties are provided. Particular emphasis is put on varieties of closure algebras, that are known to constitute adequate semantics for normal extensions of the modal logic S4. A certain infinite family of such almost structurally complete, but not structurally complete, varieties is constructed. Every variety from this family has a finitely presented unifiable algebra which does not embed into any free algebra for this variety. Hence unification is not unitary there. This shows that almost structural completeness is strictly weaker than projective unification for varieties of closure algebras.