Abstract

The main result of the present paper is equivalence of the following conditions, for any k-dimensional logic L : L has a full-replacement implication system, i.e., a finite set of k-dimensional formulas with 2k variables that in a natural way adopts the Identity axiom and the Modus Ponens rule for the ordinary implication connective; L has an unary-replacement implication system, i.e., a finite set of k-dimensional formulas with k+1 variables that in a different way adopts the Identity axiom and the Modus Ponens rule for the ordinary implication connective; L has a parameterized local deduction theorem ; L has the syntactic correspondence property that is essentially the restriction of the filter correspondence property to deductive L-filters over the formula algebra alone; L is protoalgebraic in the sense that the Leibniz operator is monotonic on the set of deductive L -filters over every algebra; L has a system of equivalence formulas with parameters that defines the Leibniz operator on deductive L -filters over every algebra.We also present a family of specific examples which collectively show that the above metaequivalence doesn't remain true when in ``2k'' ``k+1'') is replaced by ``2k-1''. This, in particular, disproves the statement of [4], Theorem 13.2.