This is a summary of a talk delivered at the Winter School of Logic held in Rabka, 24.02 – 04.03.1986 by the Department of Logic of the Jagiellonian University. We wish to announce here several results on embeddability of quotient algebras of certain kind into algebras of some varieties related to the class of Heyting algebras. A “by product” is the deduction theorem for a large family of intermediate consequence operations.

The intuitionistic consequence operation restricted to the language with (equivalence) and (negation) as the only connectives is axiomatized by means of a finite set of sequential rules of inference.

In this paper we dene a concept of depth of a consequence operation which seems to have a few useful properties. To make our denition worth- while we shall show that the concept of depth leads to a strengthening of the well-known theorem of R. Wojcicki [4]. For unexplained terminology and notations we refer the reader to R. Wojcicki [5]. Algebras and matrices con- sidered in this paper are of the same similarity type indicating a sequence of nitary operations.

The equivalence connective in ukasiewicz logic has its algebraic counterpart which is the distance function d(x,y) =|x–y| of a positive cone of a commutative -group. We make some observations on logically motivated algebraic structures involving the distance function.