Proof theory for linear lattices (Q1070254)

This paper deals with lattices representable as lattices of permuting equivalences (Type I according to Jónsson). Via Mal'cev correspondences it is easily seen that these form a recursively axiomatizable quasivariety, an explicit list of axioms has been given by \textit{B. Jónsson} [Trans. Am. Math. Soc. 92, 449-464 (1959; Zbl 0105.253)]. Gödel's completeness Theorem guarantees the existence of a complete calculus for the universal Horn theory of these lattices, the paper under review shows that the usual method of valuated graphs yields such a calculus. The achievement is to have explicitly formulated this calculus. Thus, proof theoretic results become possible. The author provides a normal form theorem concerning the order of the deductions and a duality theorem for ''planar'' proofs. The reviewer holds that the term ''linear lattices'' should be reserved for lattices of linear subspaces of vector spaces. That these form a class of definitely more special nature is best illustrated by the results of Gel'fand and Ponomarev mentioned in the introduction.