A b s t r a c t.
The main result of the present paper is
equivalence of the following conditions,
for any k-dimensional logic L :
(i) 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;
(ii)
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;
(iii)
L has a parameterized local deduction theorem ;
(iv)
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;
(v)
L is protoalgebraic in the sense that
the Leibniz operator is monotonic on
the set of deductive L -filters over every algebra;
(vi)
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 (i) ``2k'' (resp., in (ii) ``k+1'') is replaced by ``2k-1'' (resp., by ``k''). This, in particular, disproves the statement of [4], Theorem 13.2.