Characterization of Strong Day Implication Systems

The notion of a Day implication system was introduced by Janusz Czelakowski as adaptation of Day terms for studying congruence-modularity in quasivarieties. We consider a strengthening of this notion that plays in equational-style deductive systems a role similar to that of multiterm implication systems. In particular, it means that an equational-style version of Deduction-Detachment Theorem holds. Further, by the methods of Abstract Algebraic Logic, we show that existence of a strong Day implication system is equivalent to the existence of a special Gentzen-style system over an equational-style deductive system.