Is there published work about universal anti-Horn classes?
Anti-Horn formulas are also sometimes known as dual Horn. See also related question Is there any research of universal algebras axiomatized by non-Horn clauses? asking about universal classes more generally.
A universal class is definable by the conjunction of a set of universal sentences, which here are formulas with universal quantification. The underlying language allows relational symbols and an equality symbol $\approx$; terms are built from variables, constants, and functional symbols; and atoms are either relational expressions $R(\mathbf{t})$ or identities $s \approx t,$ where $s$ and $t$ are terms and $\mathbf{t}$ is a sequence of terms. Quantification is first-order.
Because propositional formulas are equivalent to formulas in conjunctive normal form, universal sentences can be considered to be disjunctions of atoms or negated atoms. Each universal sentence can then be classified by how many atoms and negated atoms it contains in the disjunction. A Horn formula is a disjunction of atoms or negated atoms, with at most one atom that is not negated; the remaining atoms are all negated. An anti-Horn or dual Horn formula has at most one atom that is negated.
First, consider Horn classes. Varieties are universal classes definable by identities. Denote a list of variables by $\mathbf{x}$. Quasivarieties are universal classes definable by quasi-identities of the form $\alpha_1(\mathbf{x})\land\dots\land\alpha_k(\mathbf{x}) \to \alpha_0(\mathbf{x}),$ where each $\alpha_i$ is either an identity or a relational atom $R(\mathbf{x}).$ If in a quasi-identity $k=1$ and $\alpha_1$ is allowed to be the special symbol $\top$, denoting a relation with arity 0 that is always interpreted as true, then quasi-identities subsume identities. If in a quasi-identity $\alpha_0$ is the special symbol $\bot$, interpreted as false, then such a quasi-identity is known as an anti-identity. Anti-identities define anti-varieties. A universal Horn sentence is then either an identity, anti-identity, or a quasi-identity; and a universal Horn class is a class definable by universal Horn sentences. (These definitions are essentially those of Gorbunov.)
The theory of universal Horn classes is therefore rather general, encompassing all of classical universal algebra.
However, to characterize some classes of structures one sometimes requires sentences that are universal anti-Horn, i.e. of the form $$\forall \mathbf{x}\; \alpha_0(\mathbf{x}) \to \alpha_1(\mathbf{x})\lor\dots\lor\alpha_k(\mathbf{x}),$$ or equivalently disjunctions with at most one negated atom.
Anti-Horn sentences capture fixed finite cardinality of a structure, and other desirable properties that are not closed under products (recall a result by Keisler-Galvin-Shelah that first-order formulas preserved by reduced products are precisely those that are equivalent to a Horn formula). Throwing out products means losing all the nice tools in chapter 9 of Hodges or chapter 6 of Chang & Keisler. Compactness also fails for classes of such structures. Finite model theory considers classes of finite structures, i.e. models of infinite disjunctions of universal anti-Horn sentences of a special form, but its focus is often beyond first-order logic and existential quantification is rather important for the core machinery of Ehrenfeucht–Fraïssé games. One obviously cannot expect universal anti-Horn classes to have the same nice structure theory that exists for varieties, and to a lesser extent for quasi-varieties and universal Horn classes, nor can one expect to be able to use the tools of finite model theory, but there should be some basic theory.
I've found a few of the later papers by Mal'tsev that start sketching a theory of universal classes, but he died before getting far. If such work has been done it is therefore possibly quite old and difficult to find in English, so I am hoping to find pointers to such theory. I intend to apply it to classes defined by means of both universal Horn and universal anti-Horn sentences, arising naturally in constraint satisfaction.
This question seems extremely basic, but also missing from standard textbooks, so perhaps I am missing an extremely basic insight about why universal anti-Horn classes are mathematically uninteresting—if so, a hint would be appreciated.
- Viktor A. Gorbunov, Algebraic theory of quasivarieties, Plenum, 1998. (ISBN 0-306-11063-6)
- A. I. Mal'tsev, Universally axiomatizable subclasses of locally finite classes of models, Siberian Mathematical Journal 8(5), 1967, pp.764–770. (doi:10.1007/BF01040652)
Edit 2015-04-20: as suggested in comments here and at the linked question, I'm now investigating multiple-conclusion rules, preservation theorems relating to coproducts and the "arrows reversed" notion corresponding to reducts, discriminator terms, pseudoidentities, and also considering the term "dual Horn" instead of "anti-Horn".
Additional references 2015-04-23:
- A. I. Mal'cev, Algebraic Systems, Springer, 1973. (ISBN 0-387-05792-7) See Section 7.
- D. J. Shoesmith and T. J. Smiley, Multiple-conclusion Logic, Cambridge University Press, 1978.
