Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: What are Horn theories?

Evan Washington (Apr 16 2024 at 02:38):

Intermediate between finite-product theories (Lawvere theories, algebraic theories) and finite-limit theories (essentially algebraic theories) are equational Horn theories. (Partial Horn theories, though, are equivalent to finite-limit theories.) Whereas algebraic theories have axioms of the form $\vdash s = t$ equational Horn theories have axioms of the form $s_1 = t_1, \dots, s_n = t_n \vdash s = t$ so conditional equations or quasi-identities replace the unconditional equations. The class of models of a Horn theory form a quasi-variety, while the models of an algebraic theory form a variety.

I can't seem to find an answer to this in the usual places (like the Elephant or nLab). What property characterizes the Horn theories, in the same way having finite products characterizes (many-sorted) algebraic theories? It must be something intermediate in strength between having finite products and having finite limits.

Ryan Wisnesky (Apr 16 2024 at 03:01):

this paper: https://coalg.org/calco15/ei/hino.pdf gives a few characterizations in table 1

Evan Washington (Apr 16 2024 at 03:10):

That paper seems to say what the category of models is like (i.e. that the models of a Horn theory must be what is sometimes called an "algebraic category"), but not what the "classifying model" is like

Ralph Sarkis (Apr 16 2024 at 04:14):

What you want is probably Theorem 25 and 27 in Section 3.3 of Wechler's Universal Algebra for Computer Scientists. They give the following corollary (this section has three variants of what kind of implications they allow, infinitely many variables, finitely many variables, and finitely many premises, Horn clauses being those with finitely many premises):
e8c0583f-3493-42ba-af02-9cc8a1b6d080.jpg

Ralph Sarkis (Apr 16 2024 at 04:21):

Wait, I gave the same answer as Ryan...

Morgan Rogers (he/him) (Apr 16 2024 at 07:54):

See also Frey's work on clans as a way of characterising intermediate theories between finite product and finite limit