Let V be a s.f.b. (strongly finitely based, see below) variety of algebras. The central result is Theorem 2 saying that the logic defined by all matrices (A, d) with d A V is finitely based iff the A V have 1st order definable cosets for their congruences. Theorem 3 states a similar axiomatization criterion for the logic determined by all matrices (A, A), A V, a term which is constant in V. Applications are given in a series of examples.

After some motivating remarks in Section 1, in Section 2 we show how to replace an axiomatic basis for any one of a broad range of sentential logics having finitely many axiom schemes and Modus Ponens as the sole proper rule, by a basis with the same axiom schemes and finitely many one-premiss rules. Section 3 mentions some questions arising from this replacement procedure , explores another such procedure, and discusses some aspects of the consequence relations associated with the different (...) axiomatizations in play. Several open problems are mentioned. An appendix briefly treats the issue of a similar ‘at most one-premiss rules’ reformulation of proof systems with sequent-to-sequent rules. (shrink)

We define a property for varieties V, the f.r.p. . If it applies to a finitely based V then V is strongly finitely based in the sense of [14], see Theorem 2. Moreover, we obtain finite axiomatizability results for certain propositional logics associated with V, in its generality comparable to well-known finite base results from equational logic. Theorem 3 states that each variety generated by a 2-element algebra has the f.r.p. Essentially this implies finite axiomatizability of a 2-valued logic in (...) any finite language. (shrink)