Equational Consequence
Alex Citkin, Alexei Yu. Muravitsky · 2022
Abstract This chapter develops a theory of the consequence relation for a schematic language of terms with equality. This consequence relation, called the equational consequence, is determined in a semantic way by means of E-matrices, as well as syntactically by inference rules, and their equivalence is established as a completeness theorem. We also define the concept of the Lindenbaum-Tarski matrix and the concept of the Mal'cev matrix for the equational consequence. Further, we prove an analog of the Mal'cev first and second theorems, as well as analogs of the Dick and Tietze theorems for the equational consequence. The equational consequence based on implication logic is illustrated by two examples: the class of Boolean algebras with equality and the class of Heyting algebras with equality.