Algebraic semantics for universal Horn logic without equality. (English)
Universal algebra and quasigroup theory, Lect. Conf., Jadwisin/Pol. 1989, Res. Expo. Math. 19, 1-56 (1992).
Summary: [For the entire collection see Zbl 0745.00017.] An algebraic model theory for universal Horn logic (UHL) is developed that encompasses both strict UHL with equality, in particular quasi- equational logic, and sentential logic, which can be naturally viewed as UHL without equality and with a single, unary predicate. The underlying formal mechanism is the $k$-deductive system; its propositions are $k$- tuples of sentences and its models are algebras with a designated set of “true” $k$-tuples called a filter. Inherent in every $k$-deductive system, in fact in every universal Horn theory, is a notion of equality in the sense of Leibniz that may have no representation in the formal language. It determines the Leibniz operator, a mapping between the lattices of filters and congruences of an algebra, in terms of which a hierarchy of $k$-deductive systems can be defined. Monotone Leibniz operators give rise to protoalgebraic $k$-deductive systems. They form the widest class of $k$-deductive systems with a reasonable algebraic semantics; a major part of the paper is devoted to their study. Two of the main results of the paper: (1) a metamathematical characterization of protoalgebraic $k$-deductive systems in the spirit of Mal’cev’s characterization of congruence-permutable equational theories; (2) an algebraic characterization of the reduced model classes of $k$- deductive systems analogous to Birkhoff’s well-known characterization of varieties. Similar characterizations are obtained for other classes of $k$-deductive systems arising from the Leibniz operator. Some applications to computer science and formal language theory are given.