Finite basis theorem for filter-distributive protoalgebraic deductive systems and strict universal Horn classes (Q1422452)

In the paper the following two main theorems are proved: (1) A finitely generated protoalgebraic strict universal Horn class that is filter-distributive is finitely based. (2) Every finitely generated axiomatic subclass of a filter-distributive, protoalgebraic strict universal Horn class is finitely based. The author gives three equivalent forms of these theorems, namely in terms of strict universal Horn classes, in terms of matrix-quasivarieties and in terms of \(\vec{k}\)-deductive systems. These theorems do not apply to sequent calculi. Also presented are many other related results, showing the new ones in a wider context. Thus the paper can be considered as a review of the results concerning filter-distributive protoalgebraic deductive systems and strict universal Horn classes.